@@ -121,19 +121,28 @@ struct EvalCallOptions {
121121 EvalCallOptions () {}
122122};
123123
124- // / Simple control flow statements like `if` only produce a single state split,
125- // / so the fact that they are included in the source code implies that both
126- // / branches are possible (at least under some conditions) and the analyzer can
127- // / freely assume either of them. (This is not entirely true, because there may
128- // / be unmarked logical correlations between `if` statements, but is a good
129- // / enough heuristic and the analyzer strongly relies on it.)
130- // / On the other hand, in a loop the state may be split repeatedly at each
131- // / evaluation of the loop condition, and this can lead to following "weak"
132- // / assumptions even though the code does not imply that they're valid and the
133- // / programmer intended to cover them.
134- // / This function is called to mark the `State` when the engine makes an
135- // / assumption which is weak. Checkers may use this heuristical mark to discard
136- // / result and reduce the amount of false positives.
124+ // / Simple control flow statements like `if` can only produce a single two-way
125+ // / state split, so when the analyzer cannot determine the value of the
126+ // / condition, it can assume either of the two options, because the fact that
127+ // / they are in the source code implies that the programmer thought that they
128+ // / are possible (at least under some conditions).
129+ // / (Note that this heuristic is not entirely correct when there are _several_
130+ // / `if` statements with unmarked logical connections between them, but it's
131+ // / still good enough and the analyzer heavily relies on it.)
132+ // / In contrast with this, a single loop statement can produce multiple state
133+ // / splits, and we cannot always single out safe assumptions where we can say
134+ // / that "the programmer included this loop in the source code, so they clearly
135+ // / thought that this execution path is possible".
136+ // / However, the analyzer wants to explore the code in and after the loop, so
137+ // / it makes assumptions about the loop condition (to get a concrete execution
138+ // / path) even when they are not justified.
139+ // / This function is called by the engine to mark the `State` when it makes an
140+ // / assumption which is "weak". Checkers may use this heuristical mark to
141+ // / discard the result and reduce the amount of false positives.
142+ // / TODO: Instead of just marking these branches for checker-specific handling,
143+ // / we could discard them completely. I suspect that this could eliminate some
144+ // / false positives without suppressing too many true positives, but I didn't
145+ // / have time to measure its effects.
137146ProgramStateRef recordWeakLoopAssumption (ProgramStateRef State);
138147
139148// / Returns true if `recordWeakLoopAssumption()` was called on the execution
@@ -341,9 +350,9 @@ class ExprEngine {
341350 ExplodedNode *Pred);
342351
343352 // / ProcessBranch - Called by CoreEngine. Used to generate successor
344- // / nodes by processing the 'effects' of a branch condition.
353+ // / nodes by processing the 'effects' of a branch condition.
345354 // / If the branch condition is a loop condition, IterationsFinishedInLoop is
346- // / the number of already finished iterations (0, 1, 2...); otherwise it's
355+ // / the number of already finished iterations (0, 1, 2, ...); otherwise it's
347356 // / std::nullopt.
348357 void processBranch (const Stmt *Condition, NodeBuilderContext &BuilderCtx,
349358 ExplodedNode *Pred, ExplodedNodeSet &Dst,
0 commit comments