Brian William Hackett wrote:
improvements to the tool's inference will reduce the need for annotations.
In both the above cases it would not be too hard to work on the tool to infer
these and similar postconditions.
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.
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.
I think inference would more useful as an help tool to let programmers
see what kind of __postcondition annotation could be put on the
function, but that it better be their choice to add them or not.
Of course, when the function is only used locally, inferring
automatically makes writing the code easier.
_______________________________________________
dev-static-analysis mailing list
[email protected]
https://lists.mozilla.org/listinfo/dev-static-analysis
