3 ms·
I think the most significant are the SAL version 2 annotations. This is a nice introduction : https://www.cs.cmu.edu/~fp/courses/15122-f10/lectures/25-sal.pdf h
by ekr 11y ago
I think the most significant are the SAL version 2 annotations. This is a nice introduction : https://www.cs.cmu.edu/~fp/courses/15122-f10/lectures/25-sal.pdf https://www.cs.cmu.edu/~fp/courses/15122-f10/lectures/25-sal....
Basically, there's an additional step after compilation, called code analysis, which runs this static verification. I think it's implemented on top of the Z3 theorem prover.
- cpeterso 11y agoHere's a list of the driver code analysis warnings. I wonder how many of these could be codified as compile-time checks in the winapi-kmd-rs library. For example, the KIRQL type is a u8 in winapi-kmd-rs, but the code analysis warnings the valid IRQL range is 0–31. https://msdn.microsoft.com/en-us/library/windows/hardware/ff550572(v=vs.85).aspx https://msdn.microsoft.com/en-us/library/windows/hardware/ff...