Function execution context correctness is one of the most easily violated critical properties by OS (operation system) kernel programs while it is non-trivial to be checked out. The existing solutions suffer some difficulty and limitation. This paper presents a framework PRPF to check the correctness of function execution context, as well as the modeling process and algorithms in detail. The PRPF has the advantages, such as direct checking source code, no need writing formal specifications, low time and space costs, and perfect scalability, etc., over the existing techniques. The technique has been applied in checking the Linux kernel source 2.4.20. The experimental results show that PRPF can check the correctness of function execution context as expected by automatically exploring all paths in the sources. As a result, 23 errors and 5 false positives are found in the ‘drivers/net’ source directory. The technique is very helpful in improving the quality of OS kernel codes.