----- Jean-Marc Desperrier <[email protected]> wrote: > I'm not sure autoinfering is always the good solution :-) > > When you add the" __postcondition(return <= amount)" annotation to > PR_Read, you are actually changing an implicit, "must read some text" > part of the contract the PR_Read function has with the rest of the world > to something that's explicitly described. This is a very good thing. > It infering has the consequence you don't do it anymore, it's not > actually positive.
Hi, I agree that making the contracts explicit is good. Mozilla has a lot of code though, and anything which reduces the annotation burden for that code I view as good. Your idea of having the inference export annotations which could be added to the code is a great meet-in-the-middle solution, definitely worth investigating. > In fact, I don't know if it's not there already, the best would be to > take the __postcondition annotations as input and check that the > function really respect them. Yes, each __postcondition will be checked and a report generated if it might not hold at exit from the function. There is an alternate __postcondition_assume which will *not* be checked; the tool just assumes it holds after each call. Brian _______________________________________________ dev-static-analysis mailing list [email protected] https://lists.mozilla.org/listinfo/dev-static-analysis
