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

ExprEngine: Improved handling of struct member assignments in loop

This commit is contained in:
Daniel Marjamäki 2019-10-14 19:41:32 +02:00
parent ee280a94fb
commit 8c5c070d6a
2 changed files with 38 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

25
lib/exprengine.cpp
View File

@ -1250,6 +1250,31 @@ static void execute(const Token *start, const Token *end, Data &data)
std::set<int> changedVariables;
for (const Token *tok2 = tok; tok2 != bodyEnd; tok2 = tok2->next()) {
if (Token::Match(tok2, "%assign%")) {
if (Token::Match(tok2->astOperand1(), ". %name% =") && tok2->astOperand1()->astOperand1() && tok2->astOperand1()->astOperand1()->valueType()) {
const Token *structToken = tok2->astOperand1()->astOperand1();
if (!structToken || !structToken->valueType() || !structToken->varId())
throw VerifyException(tok2, "Unhandled assignment in loop");
const Scope *structScope = structToken->valueType()->typeScope;
if (!structScope)
throw VerifyException(tok2, "Unhandled assignment in loop");
const std::string &memberName = tok2->previous()->str();
ExprEngine::ValuePtr structVal1 = data.getValue(structToken->varId(), structToken->valueType(), structToken);
auto structVal = std::dynamic_pointer_cast<ExprEngine::StructValue>(structVal1);
if (!structVal)
throw VerifyException(tok2, "Unhandled assignment in loop");
ExprEngine::ValuePtr memberValue;
for (const Variable &member : structScope->varlist) {
if (memberName == member.name() && member.valueType()) {
memberValue = createVariableValue(member, data);
break;
}
}
if (!memberValue)
throw VerifyException(tok2, "Unhandled assignment in loop");
data.assignStructMember(tok2, &*structVal, memberName, memberValue);
continue;
}
if (!Token::Match(tok2->astOperand1(), "%var%"))
throw VerifyException(tok2, "Unhandled assignment in loop");
// give variable "any" value

13
test/testexprengine.cpp
View File

@ -50,6 +50,7 @@ private:
TEST_CASE(while1);
TEST_CASE(while2);
TEST_CASE(while3);
TEST_CASE(array1);
TEST_CASE(array2);
@ -271,6 +272,18 @@ private:
expr(code, "=="));
}
void while3() {
const char code[] = "struct AB {int a; int b;};\n"
"void f() {\n"
" struct AB ab;\n"
" while (1)\n"
" ab.a = 3;\n"
" ab.a == 0;\n"
"}";
ASSERT_EQUALS("(assert (= 3 0))\n"
"z3::unsat",
expr(code, "=="));
}
void array1() {
ASSERT_EQUALS("(assert (= 5 0))\nz3::unsat",