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

Bug hunting; Fixed array init

This commit is contained in:
Daniel Marjamäki 2020-12-14 22:15:10 +01:00
parent 4e90356a76
commit 82635417d2
2 changed files with 12 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
lib/exprengine.cpp
View File

@ -891,8 +891,12 @@ ExprEngine::ArrayValue::ArrayValue(DataBase *data, const Variable *var)
size.push_back(std::make_shared<ExprEngine::IntRange>(data->getNewSymbolName(), 1, ExprEngine::ArrayValue::MAXSIZE)); size.push_back(std::make_shared<ExprEngine::IntRange>(data->getNewSymbolName(), 1, ExprEngine::ArrayValue::MAXSIZE));
} }
const Token *initToken = var->nameToken();
while (initToken && initToken->str() != "=")
initToken = initToken->astParent();
ValuePtr val; ValuePtr val;
if (var && !var->isGlobal() && !var->isStatic() && !(var->isArgument() && var->isConst())) if (var && !var->isGlobal() && !var->isStatic() && !(var->isArgument() && var->isConst()) && !initToken)
val = std::make_shared<ExprEngine::UninitValue>(); val = std::make_shared<ExprEngine::UninitValue>();
else if (var && var->valueType()) { else if (var && var->valueType()) {
::ValueType vt(*var->valueType()); ::ValueType vt(*var->valueType());

9
test/testexprengine.cpp
View File

@ -87,6 +87,7 @@ private:
TEST_CASE(array6); TEST_CASE(array6);
TEST_CASE(arrayInit1); TEST_CASE(arrayInit1);
TEST_CASE(arrayInit2); TEST_CASE(arrayInit2);
TEST_CASE(arrayInit3);
TEST_CASE(arrayUninit); TEST_CASE(arrayUninit);
TEST_CASE(arrayInLoop); TEST_CASE(arrayInLoop);
@ -615,8 +616,8 @@ private:
} }
void array2() { void array2() {
ASSERT_EQUALS("(and (>= |$3:4| 0) (<= |$3:4| 255))\n" ASSERT_EQUALS("(and (>= |$4:4| 0) (<= |$4:4| 255))\n"
"(= |$3:4| 365)\n" "(= |$4:4| 365)\n"
"z3::unsat\n", "z3::unsat\n",
expr("void dostuff(unsigned char *); int f() { unsigned char arr[10] = \"\"; dostuff(arr); return arr[4] == 365; }", "==")); expr("void dostuff(unsigned char *); int f() { unsigned char arr[10] = \"\"; dostuff(arr); return arr[4] == 365; }", "=="));
} }
@ -672,6 +673,10 @@ private:
ASSERT_EQUALS("66", getRange("void f() { char str[] = \"hello\"; str[0] = \'B\'; }", "str[0]=\'B\'")); ASSERT_EQUALS("66", getRange("void f() { char str[] = \"hello\"; str[0] = \'B\'; }", "str[0]=\'B\'"));
} }
void arrayInit3() {
ASSERT_EQUALS("-32768:32767", getRange("void f() { short buf[5] = {2, 1, 0, 3, 4}; ret = buf[2]; }", "buf[2]"));
}
void arrayUninit() { void arrayUninit() {
ASSERT_EQUALS("?", getRange("int f() { int arr[10]; return arr[4]; }", "arr[4]")); ASSERT_EQUALS("?", getRange("int f() { int arr[10]; return arr[4]; }", "arr[4]"));
} }