ProcessAssume should already be correct -- though it doesn't count the checkers, the early end condition results in a return, not a break.
Looking at the checkers, there are roughly three kinds of callbacks: 1. Full visits. Every checker gets a turn, and they can create multiple ExplodedNodes. (Ex: _PreVisit, VisitBranchCondition) 2. Evaluations. First checker to claim the statement wins, and it can create multiple ExplodedNodes. (Ex: EvalCallExpr, EvalNilReceiver) 3. Filters: Every checker gets a turn, but they can't bifurcate the state. (Ex: ProcessAssume, proposed ProcessRegionChange) These require three different loops, whether or not we're caching. The problem is that each callback takes completely different arguments, and I'm not sure how to parameterize a loop to make calls with different signatures. Which doesn't make it impossible, just annoying. This definitely ought to be cleaner. On Thu, 5 Aug 2010 21:10:43 -0700, Ted Kremenek <[email protected]> wrote: > Looks great Zhongxing. > > We should also update the corresponding logic in ProcessAssume to also do > the right checking to make sure that all checkers were evaluated. Down the > line we should also consider if we can merge this logic, instead of having > separate copies. > > On Aug 5, 2010, at 5:16 PM, Zhongxing Xu wrote: > >> I see. How about this patch to make the check functional. >> >> Index: lib/Checker/GRExprEngine.cpp >> =================================================================== >> --- lib/Checker/GRExprEngine.cpp (版本 110392) >> +++ lib/Checker/GRExprEngine.cpp (工作副本) >> @@ -206,6 +206,8 @@ >> unsigned checkersEvaluated = 0; >> >> for (CheckersOrdered::iterator I=CO->begin(), E=CO->end(); I!=E; ++I){ >> + if (PrevSet->empty()) >> + break; >> ExplodedNodeSet *CurrSet = 0; >> if (I+1 == E) >> CurrSet = &Dst; _______________________________________________ cfe-commits mailing list [email protected] http://lists.cs.uiuc.edu/mailman/listinfo/cfe-commits
