diff --git a/lib/exprengine.cpp b/lib/exprengine.cpp index 39b05e4f6..6ef8079ab 100644 --- a/lib/exprengine.cpp +++ b/lib/exprengine.cpp @@ -124,6 +124,8 @@ namespace { std::vector constraints; void assignValue(const Token *tok, unsigned int varId, ExprEngine::ValuePtr value) { + if (varId == 0) + return; mTrackExecution->symbolRange(tok, value); if (value) { if (auto arr = std::dynamic_pointer_cast(value)) { @@ -1069,10 +1071,6 @@ static void execute(const Token *start, const Token *end, Data &data) // TODO this is a bailout throw std::runtime_error("Unhandled:" + tok->str()); - if (Token::Match(tok, "for|while (")) - // TODO this is a bailout - throw std::runtime_error("Unhandled:" + tok->str()); - // Variable declaration.. if (tok->variable() && tok->variable()->nameToken() == tok) { if (Token::Match(tok, "%varid% ; %varid% =", tok->varId())) { @@ -1144,6 +1142,32 @@ static void execute(const Token *start, const Token *end, Data &data) return; } + if (Token::Match(tok, "for|while (") && Token::simpleMatch(tok->linkAt(1), ") {")) { + const Token *bodyStart = tok->linkAt(1)->next(); + const Token *bodyEnd = bodyStart->link(); + + // TODO this is very rough code + std::set changedVariables; + for (const Token *tok2 = tok; tok2 != bodyEnd; tok2 = tok2->next()) { + if (Token::Match(tok2, "%var% %assign%")) { + // give variable "any" value + int varid = tok2->varId(); + if (changedVariables.find(varid) != changedVariables.end()) + continue; + changedVariables.insert(varid); + data.assignValue(tok2->next(), varid, createVariableValue(*tok2->variable(), data)); + } else if (Token::Match(tok2, "++|--") && tok2->astOperand1() && tok2->astOperand1()->variable()) { + // give variable "any" value + const Token *vartok = tok2->astOperand1(); + int varid = vartok->varId(); + if (changedVariables.find(varid) != changedVariables.end()) + continue; + changedVariables.insert(varid); + data.assignValue(tok2, varid, createVariableValue(*vartok->variable(), data)); + } + } + } + if (Token::simpleMatch(tok, "} else {")) tok = tok->linkAt(2); } diff --git a/test/testexprengine.cpp b/test/testexprengine.cpp index a6af2ec94..9506176b3 100644 --- a/test/testexprengine.cpp +++ b/test/testexprengine.cpp @@ -46,6 +46,9 @@ private: TEST_CASE(switch1); + TEST_CASE(while1); + TEST_CASE(while2); + TEST_CASE(array1); TEST_CASE(array2); TEST_CASE(array3); @@ -201,6 +204,34 @@ private: expr(code, "==")); } + void while1() { + const char code[] = "void f(int y) {\n" + " int x = 0;\n" + " while (x < y)\n" + " x = x + 34;\n" + " x == 1;\n" + "}"; + ASSERT_EQUALS("(declare-fun $2 () Int)\n" + "(assert (<= $2 2147483647))\n" + "(assert (>= $2 (- 2147483648)))\n" + "(assert (= (+ $2 34) 1))\n", + expr(code, "==")); + } + + void while2() { + const char code[] = "void f(int y) {\n" + " int x = 0;\n" + " while (x < y)\n" + " x++;\n" + " x == 1;\n" + "}"; + ASSERT_EQUALS("(declare-fun $2 () Int)\n" + "(assert (<= $2 2147483647))\n" + "(assert (>= $2 (- 2147483648)))\n" + "(assert (= $2 1))\n", + expr(code, "==")); + } + void array1() { ASSERT_EQUALS("(assert (= 5 0))\n",