From 4235a295011ab3214c9c49bb74767cbd7523c404 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Daniel=20Marjam=C3=A4ki?= <daniel.marjamaki@gmail.com>
Date: Tue, 21 Jan 2020 18:55:07 +0100
Subject: [PATCH] ExprEngine: Handle variable annotations better

---
 lib/exprengine.cpp      |  2 ++
 test/testexprengine.cpp | 22 +++++++++++++++++++---
 2 files changed, 21 insertions(+), 3 deletions(-)

diff --git a/lib/exprengine.cpp b/lib/exprengine.cpp
index 947b87b7a..fa9dbdfa4 100644
--- a/lib/exprengine.cpp
+++ b/lib/exprengine.cpp
@@ -234,6 +234,8 @@ namespace {
                 return ExprEngine::ValuePtr();
             ExprEngine::ValuePtr value = getValueRangeFromValueType(getNewSymbolName(), valueType, *settings);
             if (value) {
+                if (tok->variable() && tok->variable()->nameToken())
+                    addConstraints(value, tok->variable()->nameToken());
                 assignValue(tok, varId, value);
             }
             return value;
diff --git a/test/testexprengine.cpp b/test/testexprengine.cpp
index 1688814e8..be400774c 100644
--- a/test/testexprengine.cpp
+++ b/test/testexprengine.cpp
@@ -34,6 +34,7 @@ private:
     void run() OVERRIDE {
 #ifdef USE_Z3
         TEST_CASE(annotation1);
+        TEST_CASE(annotation2);
 
         TEST_CASE(expr1);
         TEST_CASE(expr2);
@@ -165,6 +166,21 @@ private:
         ASSERT_EQUALS(expected, expr(code, "<"));
     }
 
+    void annotation2() {
+        const char code[] = "__cppcheck_low__(100) short x;\n"
+                            " void f() {\n"
+                            "    return x < 10;\n"
+                            "}";
+
+        const char expected[] = "(declare-fun $1 () Int)\n"
+                                "(assert (>= $1 100))\n" // <- annotation
+                                "(assert (and (>= $1 (- 32768)) (<= $1 32767)))\n"
+                                "(assert (< $1 10))\n"
+                                "z3::unsat";
+
+        ASSERT_EQUALS(expected, expr(code, "<"));
+    }
+
     void expr1() {
         ASSERT_EQUALS("-32768:32767", getRange("void f(short x) { a = x; }", "x"));
     }
@@ -409,9 +425,9 @@ private:
 
     void floatValue3() {
         const char code[] = "void foo(float f) { return f > 12.0; }";
-        const char expected[] = "(declare-fun |12.0| () (_ FloatingPoint 11 53))\n"
-                                "(declare-fun $1 () (_ FloatingPoint 11 53))\n"
-                                "(assert (fp.gt $1 |12.0|))\n"
+        const char expected[] = "(declare-fun |12.0| () Real)\n"
+                                "(declare-fun $1 () Real)\n"
+                                "(assert (> $1 |12.0|))\n"
                                 "z3::sat";
         ASSERT_EQUALS(expected, expr(code, ">"));
     }