@@ -2820,18 +2820,20 @@ void ExprEngine::processBranch(
28202820 ProgramStateRef PrevState = PredN->getState ();
28212821
28222822 ProgramStateRef StTrue, StFalse;
2823- if (const auto KnownCondValueAssumption = assumeCondition (Condition, PredN))
2823+ StTrue = StFalse = PrevState;
2824+
2825+ if (const auto KnownCondValueAssumption = assumeCondition (Condition, PredN)) {
28242826 std::tie (StTrue, StFalse) = *KnownCondValueAssumption;
2825- else {
2826- assert (!isa<ObjCForCollectionStmt>(Condition));
2827- // TODO: instead of this shortcut perhaps it would be better to "rejoin"
2828- // the common execution path with
2829- // StTrue = StFalse = PrevState;
2830- builder.generateNode (PrevState, true , PredN);
2831- builder.generateNode (PrevState, false , PredN);
2832- continue ;
2827+
2828+ if (!StTrue)
2829+ builder.markInfeasible (true );
2830+
2831+ if (!StFalse)
2832+ builder.markInfeasible (false );
28332833 }
2834- if (StTrue && StFalse)
2834+ bool BothFeasible = builder.isFeasible (true ) && builder.isFeasible (false );
2835+
2836+ if (BothFeasible)
28352837 assert (!isa<ObjCForCollectionStmt>(Condition));
28362838
28372839 const Expr *EagerlyAssumeExpr =
@@ -2844,49 +2846,39 @@ void ExprEngine::processBranch(
28442846 ConditionExpr = ConditionExpr->IgnoreParenCasts ();
28452847 }
28462848 bool DidEagerlyAssume = EagerlyAssumeExpr == ConditionExpr;
2847- bool BothFeasible = (DidEagerlyAssume || (StTrue && StFalse)) &&
2848- builder.isFeasible (true ) && builder.isFeasible (false );
28492849
28502850 // Process the true branch.
28512851 if (builder.isFeasible (true )) {
2852- if (StTrue) {
2853- if (BothFeasible && IterationsFinishedInLoop &&
2854- *IterationsFinishedInLoop >= 2 ) {
2855- // When programmers write a loop, they imply that at least two
2856- // iterations are possible (otherwise they would just write an `if`),
2857- // but the third iteration is not implied: there are situations where
2858- // the programmer knows that there won't be a third iteration, but
2859- // this is not marked in the source code. (For example, the ffmpeg
2860- // project has 2-element arrays which are accessed from loops where
2861- // the number of steps is opaque and the analyzer cannot deduce that
2862- // there are <= 2 iterations.)
2863- // Checkers may use this heuristic mark to discard results found on
2864- // branches that contain this "weak" assumption.
2865- StTrue = recordWeakLoopAssumption (StTrue);
2866- }
2867- builder.generateNode (StTrue, true , PredN);
2868- } else {
2869- builder.markInfeasible (true );
2852+ if ((BothFeasible || DidEagerlyAssume) && IterationsFinishedInLoop &&
2853+ *IterationsFinishedInLoop >= 2 ) {
2854+ // When programmers write a loop, they imply that at least two
2855+ // iterations are possible (otherwise they would just write an `if`),
2856+ // but the third iteration is not implied: there are situations where
2857+ // the programmer knows that there won't be a third iteration, but
2858+ // this is not marked in the source code. (For example, the ffmpeg
2859+ // project has 2-element arrays which are accessed from loops where
2860+ // the number of steps is opaque and the analyzer cannot deduce that
2861+ // there are <= 2 iterations.)
2862+ // Checkers may use this heuristic mark to discard results found on
2863+ // branches that contain this "weak" assumption.
2864+ StTrue = recordWeakLoopAssumption (StTrue);
28702865 }
2866+ builder.generateNode (StTrue, true , PredN);
28712867 }
28722868
28732869 // Process the false branch.
28742870 if (builder.isFeasible (false )) {
2875- if (StFalse) {
2876- if (BothFeasible && IterationsFinishedInLoop &&
2877- *IterationsFinishedInLoop == 0 ) {
2878- // There are many situations where the programmers know that there
2879- // will be at least one iteration in a loop (e.g. a structure is not
2880- // empty) but the analyzer cannot deduce this and reports false
2881- // positives after skipping the loop.
2882- // Checkers may use this heuristic mark to discard results found on
2883- // branches that contain this "weak" assumption.
2884- StFalse = recordWeakLoopAssumption (StFalse);
2885- }
2886- builder.generateNode (StFalse, false , PredN);
2887- } else {
2888- builder.markInfeasible (false );
2871+ if ((BothFeasible || DidEagerlyAssume) && IterationsFinishedInLoop &&
2872+ *IterationsFinishedInLoop == 0 ) {
2873+ // There are many situations where the programmers know that there
2874+ // will be at least one iteration in a loop (e.g. a structure is not
2875+ // empty) but the analyzer cannot deduce this and reports false
2876+ // positives after skipping the loop.
2877+ // Checkers may use this heuristic mark to discard results found on
2878+ // branches that contain this "weak" assumption.
2879+ StFalse = recordWeakLoopAssumption (StFalse);
28892880 }
2881+ builder.generateNode (StFalse, false , PredN);
28902882 }
28912883 }
28922884 currBldrCtx = nullptr ;
0 commit comments