ExprEngine: Handling cases when for condition is always false (danmar#2984)

jubnzv · web-flow · commit 1c12b4fd78c3 · 2020-12-26T21:29:50.000+01:00
diff --git a/lib/exprengine.cpp b/lib/exprengine.cpp
@@ -2669,6 +2669,10 @@ static std::string execute(const Token *start, const Token *end, Data &data)
                 data.assignValue(tok, varid, loopValues);
                 tok = tok->linkAt(1);
                 loopValues->loopScope = tok->next()->scope();
+                // Check whether the condition expression is always false
+                if (tok->next() && (initValue > lastValue)) {
+                    tok = tok->next()->link();
+                }
                 continue;
             }
         }
diff --git a/test/testexprengine.cpp b/test/testexprengine.cpp
@@ -79,6 +79,7 @@ class TestExprEngine : public TestFixture {
         TEST_CASE(switch2);
 
         TEST_CASE(for1);
+        TEST_CASE(forAlwaysFalse1);
 
         TEST_CASE(while1);
         TEST_CASE(while2);
@@ -660,6 +661,22 @@ class TestExprEngine : public TestFixture {
                       expr(code, "=="));
     }
 
+    void forAlwaysFalse1() {
+        const char code[] = "int f() {\n"
+                            "  int a = 19;\n"
+                            "  for (int i = 0; i < 0; i++)\n"
+                            "    a += 8;\n"
+                            "  for (int i = 0; i < 1; i++)\n"
+                            "    a += 23;\n"
+                            "  for (int i = 100; i >= 1; i--)\n"
+                            "    a += 23;\n"
+                            "  return a == 42;\n"
+                            "}";
+        const char expected[] = "(and (>= $4 (- 2147483648)) (<= $4 2147483647))\n"
+                                "(= (+ $4 23) 42)\n"
+                                "z3::sat\n";
+        ASSERT_EQUALS(expected, expr(code, "=="));
+    }
 
     void while1() {
         const char code[] = "void f(int y) {\n"

Original file line number	Diff line number	Diff line change
`@@ -2669,6 +2669,10 @@ static std::string execute(const Token start, const Token end, Data &data)`
`2669`	`2669`	`data.assignValue(tok, varid, loopValues);`
`2670`	`2670`	`tok = tok->linkAt(1);`
`2671`	`2671`	`loopValues->loopScope = tok->next()->scope();`
	`2672`	`+ // Check whether the condition expression is always false`
	`2673`	`+ if (tok->next() && (initValue > lastValue)) {`
	`2674`	`+ tok = tok->next()->link();`
	`2675`	`+ }`
`2672`	`2676`	`continue;`
`2673`	`2677`	`}`
`2674`	`2678`	`}`