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

Bug hunting; Fix for '*x=y'

This commit is contained in:
Daniel Marjamäki 2020-12-13 19:53:29 +01:00
parent ffde6278de
commit bf951ea5e6
2 changed files with 17 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
lib/exprengine.cpp
View File

@ -1787,6 +1787,10 @@ static void assignExprValue(const Token *expr, ExprEngine::ValuePtr value, Data
auto val = std::dynamic_pointer_cast<ExprEngine::AddressOfValue>(pval); auto val = std::dynamic_pointer_cast<ExprEngine::AddressOfValue>(pval);
if (val) if (val)
data.assignValue(expr, val->varId, value); data.assignValue(expr, val->varId, value);
} else if (pval && pval->type == ExprEngine::ValueType::ArrayValue) {
auto arrayValue = std::dynamic_pointer_cast<ExprEngine::ArrayValue>(pval);
auto indexValue = std::make_shared<ExprEngine::IntRange>("0", 0, 0);
arrayValue->assign(indexValue, value);
} else if (pval && pval->type == ExprEngine::ValueType::BinOpResult) { } else if (pval && pval->type == ExprEngine::ValueType::BinOpResult) {
auto b = std::dynamic_pointer_cast<ExprEngine::BinOpResult>(pval); auto b = std::dynamic_pointer_cast<ExprEngine::BinOpResult>(pval);
if (b && b->binop == "+") { if (b && b->binop == "+") {

15
test/testexprengine.cpp
View File

@ -84,6 +84,7 @@ private:
TEST_CASE(array3); TEST_CASE(array3);
TEST_CASE(array4); TEST_CASE(array4);
TEST_CASE(array5); TEST_CASE(array5);
TEST_CASE(array6);
TEST_CASE(arrayInit1); TEST_CASE(arrayInit1);
TEST_CASE(arrayInit2); TEST_CASE(arrayInit2);
TEST_CASE(arrayUninit); TEST_CASE(arrayUninit);
@ -593,8 +594,8 @@ private:
" *len = 0;\n" " *len = 0;\n"
" *len == 0;\n" " *len == 0;\n"
"}"; "}";
// Currently the *len gets a BailoutValue in the loop ASSERT_EQUALS("(= 0 0)\n"
ASSERT_EQUALS("", expr(code, "==")); "z3::sat\n", expr(code, "=="));
} }
void while5() { void while5() {
@ -652,6 +653,16 @@ private:
trackExecution(code)); trackExecution(code));
} }
void array6() {
const char code[] = "void foo(int *x) {\n"
" *x = 2;\n"
" if (*x == 21) {}"
"}";
ASSERT_EQUALS("(= 2 21)\n"
"z3::unsat\n",
expr(code, "=="));
}
void arrayInit1() { void arrayInit1() {
ASSERT_EQUALS("0", getRange("inf f() { char arr[10] = \"\"; return arr[4]; }", "arr[4]")); ASSERT_EQUALS("0", getRange("inf f() { char arr[10] = \"\"; return arr[4]; }", "arr[4]"));
} }