3 ms·
Prior art from Microsoft which leverages similar idea, but using macros: https://docs.microsoft.com/en-us/cpp/code-quality/best-practices-and-examples-sal?view=
by bialpio 6y ago
Prior art from Microsoft which leverages similar idea, but using macros:
https://docs.microsoft.com/en-us/cpp/code-quality/best-practices-and-examples-sal?view=msvc-160 https://docs.microsoft.com/en-us/cpp/code-quality/best-pract...
They also have SAL annotations for "what locks it?".
- Animats 6y agoThat's been a problem with verification systems. If the annotations are not well integrated into the language, they're viewed as a nuisance. Especially if the compiler neither enforces them or uses them to help optimization.
- bialpio 6y agoThe enforcement does not necessarily need to come from the compiler - it's not uncommon to introduce additional required processes / checks that new code needs to pass (ex. "tests need to pass", "at least one reviewer must approve a change"). The compiler probably won't be able to leverage those annotations since there's always a potential for mismatch between annotations and code (but the verification system should be able to catch it) - I agree that integration into the language would be needed here, but that's not likely going to happen with C/C++ so I'm open to using a solution that's not perfect. :-)