On Feb 8, 2012, at 3:40 PM, Ted Kremenek <[email protected]> wrote: >> Ex: Should the checkers receive the post/pre visit callbacks on a CallExpr >> if it's being inlined? > > Absolutely. The pre- and post- visit checks are for checking preconditions > and postconditions, which is orthogonal to how the actual function call gets > evaluated. > > This is probably worth some design discussion.
Put another way, what you have here is essentially a typestate checker. Suppose we had a typestate checker for analyzing lock() is paired with unlock(). We want that checker to work irrespective of how lock() and unlock() are implemented, and how much of that implementation is exposed to the user. If we know the user thinks in terms of lock() and unlock(), then the checker needs to operate at that level as well. We can use the post-condition checking to validate the implementation of these functions (if it is available). What we may wish to do is add another Checker callback, that indicates the "conservative" summary was used for a function, and allow checkers to decide what is the effects they want to apply to the ProgramState. This could be independent of postVisit(). This would allow a clean way for checkers to drop checker state without muddling their post-condition checking.
_______________________________________________ cfe-commits mailing list [email protected] http://lists.cs.uiuc.edu/mailman/listinfo/cfe-commits
