On Feb 8, 2012, at 3:50 PM, Ted Kremenek wrote: > 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). > Makes sense.
> 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. So when a function is inlined, the checker is going to see something like this : check::PreStmt<CallExpr> // All the callbacks corresponding to the inlined body evaluation: check::PreStmt<Stmt> ... check::PostStmt<CallExpr> When the function is not inlined: check::PreStmt<CallExpr> // The special summary callback or EscapedSymbol callback for every parameter. check::CallSummary ... check::PostStmt<CallExpr> Anna.
_______________________________________________ cfe-commits mailing list [email protected] http://lists.cs.uiuc.edu/mailman/listinfo/cfe-commits
