Ahead of time static analysis for automatic generation of debugging interfaces to the Linux kernel