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

ExprEngine: Handle pointers to struct as function argument (#2945)

This commit is contained in:
Georgy Komarov 2020-12-13 18:02:35 +03:00 committed by GitHub
parent 81c3ac738d
commit 36ab23f1f7
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 29 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
lib/exprengine.cpp
View File

@ -2625,8 +2625,19 @@ static std::string execute(const Token *start, const Token *end, Data &data)
if (!structVal1)
structVal1 = createVariableValue(*structToken->variable(), data);
auto structVal = std::dynamic_pointer_cast<ExprEngine::StructValue>(structVal1);
if (!structVal)
throw ExprEngineException(tok2, "Unhandled assignment in loop");
if (!structVal) {
// Handle pointer to a struct
if (auto structPtr = std::dynamic_pointer_cast<ExprEngine::ArrayValue>(structVal1)) {
if (structPtr && structPtr->pointer && !structPtr->data.empty()) {
auto indexValue = std::make_shared<ExprEngine::IntRange>("0", 0, 0);
for (auto val: structPtr->read(indexValue)) {
structVal = std::dynamic_pointer_cast<ExprEngine::StructValue>(val.second);
}
}
}
if (!structVal)
throw ExprEngineException(tok2, "Unhandled assignment in loop");
}
data.assignStructMember(tok2, &*structVal, memberName, memberValue);
continue;

16
test/testexprengine.cpp
View File

@ -114,6 +114,8 @@ private:
TEST_CASE(structMember2);
TEST_CASE(structMember3);
TEST_CASE(pointerToStructInLoop);
TEST_CASE(ternaryOperator1);
#endif
}
@ -816,6 +818,20 @@ private:
ASSERT_EQUALS(expected, expr(code, "=="));
}
void pointerToStructInLoop() {
const char code[] = "struct S { int x; };\n"
"void foo(struct S *s) {\n"
" while (1)\n"
" s->x = 42; \n"
"}";
const char expected[] = "(and (>= $3 (- 2147483648)) (<= $3 2147483647))\n"
"(= $3 42)\n"
"z3::sat\n";
ASSERT_EQUALS(expected, expr(code, "=="));
}
void ternaryOperator1() {
const char code[] = "void foo(signed char x) {\n"