ExprEngine: Simplify array value if possible, ensure each array data has a unique name

This commit is contained in:
Daniel Marjamäki 2019-09-29 21:19:21 +02:00
parent 03ff32993e
commit 1ccc303602
2 changed files with 12 additions and 3 deletions

View File

@ -412,6 +412,13 @@ ExprEngine::ConditionalValue::Vector ExprEngine::ArrayValue::read(ExprEngine::Va
ret.push_back(std::pair<ValuePtr,ValuePtr>(indexAndValue.index, std::make_shared<ExprEngine::IntRange>("", cmin, cmax)));
continue;
}
// Rename IntRange
if (auto i = std::dynamic_pointer_cast<ExprEngine::IntRange>(indexAndValue.value)) {
ret.push_back(std::pair<ValuePtr,ValuePtr>(indexAndValue.index, std::make_shared<ExprEngine::IntRange>(indexAndValue.value->name + ":" + index->name, i->minValue, i->maxValue)));
continue;
}
ret.push_back(std::pair<ValuePtr,ValuePtr>(indexAndValue.index, indexAndValue.value));
}
@ -874,6 +881,8 @@ static ExprEngine::ValuePtr executeArrayIndex(const Token *tok, Data &data)
auto conditionalValues = arrayValue->read(indexValue);
for (auto value: conditionalValues)
call(data.callbacks, tok, value.second);
if (conditionalValues.size() == 1 && !conditionalValues[0].first)
return conditionalValues[0].second;
return std::make_shared<ExprEngine::ConditionalValue>(data.getNewSymbolName(), conditionalValues);
}

View File

@ -157,7 +157,6 @@ private:
ASSERT_EQUALS("2", getRange("void f(unsigned char x) { x = 258; int a = x }", "a=x"));
}
void if1() {
ASSERT_EQUALS("7:32768", getRange("inf f(short x) { if (x > 5) a = x + 1; }", "x+1"));
}
@ -198,8 +197,9 @@ private:
void array4() {
const char code[] = "int buf[10];\n"
"void f() { int x = buf[0]; }";
ASSERT_EQUALS("2:20: $2=-2147483648:2147483647\n"
"2:26: { buf=($1,size=10,[:]=$2) x=($3,{{(null),$2}})}\n",
ASSERT_EQUALS("2:16: $2:0=-2147483648:2147483647\n"
"2:20: $2=-2147483648:2147483647\n"
"2:26: { buf=($1,size=10,[:]=$2) x=$2:0}\n",
trackExecution(code));
}