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

ExprEngine; Try to handle assignments better

This commit is contained in:
Daniel Marjamäki 2020-04-30 21:05:34 +02:00
parent 5a9e81897a
commit b97250e0fa
2 changed files with 51 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

29
lib/exprengine.cpp
View File

@ -1294,11 +1294,19 @@ static ExprEngine::ValuePtr executeAssign(const Token *tok, Data &data)
{
ExprEngine::ValuePtr rhsValue = executeExpression(tok->astOperand2(), data);
if (!rhsValue && tok->astOperand2()->valueType() && tok->astOperand2()->valueType()->container && tok->astOperand2()->valueType()->container->stdStringLike) {
auto size = std::make_shared<ExprEngine::IntRange>(data.getNewSymbolName(), 0, ~0ULL);
auto value = std::make_shared<ExprEngine::IntRange>(data.getNewSymbolName(), -128, 127);
rhsValue = std::make_shared<ExprEngine::ArrayValue>(data.getNewSymbolName(), size, value, false, false, false);
call(data.callbacks, tok->astOperand2(), rhsValue, &data);
if (!rhsValue) {
const ValueType *vt = tok->astOperand1() ? tok->astOperand1()->valueType() : nullptr;
if (vt && vt->pointer == 0 && vt->isIntegral())
rhsValue = getValueRangeFromValueType(data.getNewSymbolName(), vt, *data.settings);
else {
vt = tok->astOperand2() ? tok->astOperand2()->valueType() : nullptr;
if (vt && vt->container && vt->container->stdStringLike) {
auto size = std::make_shared<ExprEngine::IntRange>(data.getNewSymbolName(), 0, ~0ULL);
auto value = std::make_shared<ExprEngine::IntRange>(data.getNewSymbolName(), -128, 127);
rhsValue = std::make_shared<ExprEngine::ArrayValue>(data.getNewSymbolName(), size, value, false, false, false);
call(data.callbacks, tok->astOperand2(), rhsValue, &data);
}
}
}
if (!rhsValue)
@ -1881,6 +1889,17 @@ static void execute(const Token *start, const Token *end, Data &data)
data.assignStructMember(tok2, &*structVal, memberName, memberValue);
continue;
}
if (tok2->astOperand1()->isUnaryOp("*") && tok2->astOperand1()->astOperand1()->varId()) {
const Token *varToken = tok2->astOperand1()->astOperand1();
ExprEngine::ValuePtr val = data.getValue(varToken->varId(), varToken->valueType(), varToken);
if (val->type == ExprEngine::ValueType::ArrayValue) {
// Try to assign "any" value
auto arrayValue = std::dynamic_pointer_cast<ExprEngine::ArrayValue>(val);
//ExprEngine::ValuePtr anyValue = getValueRangeFromValueType(data.getNewSymbolName(), tok2->astOperand1()->valueType(), *data.settings);
arrayValue->assign(std::make_shared<ExprEngine::IntRange>("0", 0, 0), std::make_shared<ExprEngine::BailoutValue>());
continue;
}
}
if (!Token::Match(tok2->astOperand1(), "%var%"))
throw VerifyException(tok2, "Unhandled assignment in loop");
if (!tok2->astOperand1()->variable())

27
test/testexprengine.cpp
View File

@ -60,6 +60,7 @@ private:
TEST_CASE(while1);
TEST_CASE(while2);
TEST_CASE(while3);
TEST_CASE(while4);
TEST_CASE(array1);
TEST_CASE(array2);
@ -92,6 +93,7 @@ private:
TEST_CASE(structMember1);
TEST_CASE(structMember2);
TEST_CASE(structMember3);
#endif
}
@ -395,6 +397,16 @@ private:
expr(code, "=="));
}
void while4() {
const char code[] = "void f(const char *host, int *len) {\n"
" while (*host)\n"
" *len = 0;\n"
" *len == 0;\n"
"}";
// Currently the *len gets a BailoutValue in the loop
ASSERT_EQUALS("", expr(code, "=="));
}
void array1() {
ASSERT_EQUALS("(assert (= 5 0))\nz3::unsat",
expr("int f() { int arr[10]; arr[4] = 5; return arr[4]==0; }", "=="));
@ -580,6 +592,21 @@ private:
ASSERT_EQUALS(expected, expr(code, "=="));
}
void structMember3() {
const char code[] = "struct S { int x; };\n"
"void foo(struct S *s) {\n"
" s->x = iter->second.data;\n" // assign some unknown value
" return s->x == 1;\n"
"}";
const char expected[] = "(declare-fun $3 () Int)\n"
"(assert (and (>= $3 (- 2147483648)) (<= $3 2147483647)))\n"
"(assert (= $3 1))\n"
"z3::sat";
ASSERT_EQUALS(expected, expr(code, "=="));
}
};
REGISTER_TEST(TestExprEngine)