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

ExprEngine: Handle while/for loops

This commit is contained in:
Daniel Marjamäki 2019-10-07 17:44:26 +02:00
parent b76be4581e
commit 21774cbdc4
2 changed files with 59 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

32
lib/exprengine.cpp
View File

@ -124,6 +124,8 @@ namespace {
std::vector<ExprEngine::ValuePtr> 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<ExprEngine::ArrayValue>(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<int> 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);
}

31
test/testexprengine.cpp
View File

@ -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",