walkero
/
cppcheck
1
0
Fork 0
Code Issues Pull Requests Projects Releases 1 Wiki Activity

ExprEngine: Handle variable annotations better

This commit is contained in:
Daniel Marjamäki 2020-01-21 18:55:07 +01:00
parent b6db5116c3
commit 4235a29501
2 changed files with 21 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
lib/exprengine.cpp
View File

@ -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;

22
test/testexprengine.cpp
View File

@ -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, ">"));
}