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

ExprEngine: Added ifIntRangeAlwaysFalse and ifIntRangeAlwaysTrue tests

This commit is contained in:
Daniel Marjamäki 2020-12-20 19:04:46 +01:00
parent 229e39e7de
commit 5701f6d368
2 changed files with 39 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
lib/exprengine.cpp
View File

@ -2504,6 +2504,9 @@ static std::string execute(const Token *start, const Token *end, Data &data)
if (auto b = std::dynamic_pointer_cast<ExprEngine::BinOpResult>(condValue)) {
canBeFalse = b->isEqual(&data, 0);
canBeTrue = b->isTrue(&data);
} else if (auto i = std::dynamic_pointer_cast<ExprEngine::IntRange>(condValue)) {
canBeFalse = i->isEqual(&data, 0);
canBeTrue = ExprEngine::BinOpResult("!=", i, std::make_shared<ExprEngine::IntRange>("0", 0, 0)).isTrue(&data);
}
Data &thenData(data);

36
test/testexprengine.cpp
View File

@ -65,6 +65,8 @@ private:
TEST_CASE(ifelse1);
TEST_CASE(ifif);
TEST_CASE(ifreturn);
TEST_CASE(ifIntRangeAlwaysFalse);
TEST_CASE(ifIntRangeAlwaysTrue);
TEST_CASE(istream);
@ -487,6 +489,40 @@ private:
expr(code, "=="));
}
void ifIntRangeAlwaysFalse() {
const char code[] = "void foo(unsigned char x) {\n"
" if (x > 0)\n"
" return;\n"
" if (x) {\n" // <-- condition should be "always false".
" x++;\n"
" }\n"
" return x == 0;\n" // <- sat
"}";
ASSERT_EQUALS("(<= $1 0)\n"
"(= $1 0)\n"
"(and (>= $1 0) (<= $1 255))\n"
"(= $1 0)\n"
"z3::sat\n",
expr(code, "=="));
}
void ifIntRangeAlwaysTrue() {
const char code[] = "void foo(unsigned char x) {\n"
" if (x < 1)\n"
" return;\n"
" if (x) {\n" // <-- condition should be "always true".
" x++;\n"
" }\n"
" return x == 0;\n" // <- unsat
"}";
ASSERT_EQUALS("(>= $1 1)\n"
"(distinct $1 0)\n"
"(and (>= $1 0) (<= $1 255))\n"
"(= (+ $1 1) 0)\n"
"z3::unsat\n",
expr(code, "=="));
}
void istream() {
const char code[] = "void foo(const std::string& in) {\n"
" std::istringstream istr(in);\n"