diff --git a/lib/exprengine.cpp b/lib/exprengine.cpp index 27fd36018..a688e6842 100644 --- a/lib/exprengine.cpp +++ b/lib/exprengine.cpp @@ -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(data.getNewSymbolName(), 0, ~0ULL); - auto value = std::make_shared(data.getNewSymbolName(), -128, 127); - rhsValue = std::make_shared(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(data.getNewSymbolName(), 0, ~0ULL); + auto value = std::make_shared(data.getNewSymbolName(), -128, 127); + rhsValue = std::make_shared(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(val); + //ExprEngine::ValuePtr anyValue = getValueRangeFromValueType(data.getNewSymbolName(), tok2->astOperand1()->valueType(), *data.settings); + arrayValue->assign(std::make_shared("0", 0, 0), std::make_shared()); + continue; + } + } if (!Token::Match(tok2->astOperand1(), "%var%")) throw VerifyException(tok2, "Unhandled assignment in loop"); if (!tok2->astOperand1()->variable()) diff --git a/test/testexprengine.cpp b/test/testexprengine.cpp index f943fe77a..0e694e2e5 100644 --- a/test/testexprengine.cpp +++ b/test/testexprengine.cpp @@ -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)