ExprEngine; Improved handling of stream read

This commit is contained in:
Daniel Marjamäki 2020-06-21 20:05:26 +02:00
parent 11e2b5ea14
commit 5497e8ed67
2 changed files with 39 additions and 0 deletions

View File

@ -1936,6 +1936,26 @@ static ExprEngine::ValuePtr executeDot(const Token *tok, Data &data)
return memberValue;
}
static void streamReadSetValue(const Token *tok, Data &data)
{
if (!tok || !tok->valueType())
return;
auto rangeValue = getValueRangeFromValueType(data.getNewSymbolName(), tok->valueType(), *data.settings);
if (rangeValue)
assignExprValue(tok, rangeValue, data);
}
static ExprEngine::ValuePtr executeStreamRead(const Token *tok, Data &data)
{
tok = tok->astOperand2();
while (Token::simpleMatch(tok, ">>")) {
streamReadSetValue(tok->astOperand1(), data);
tok = tok->astOperand2();
}
streamReadSetValue(tok, data);
return ExprEngine::ValuePtr();
}
static ExprEngine::ValuePtr executeBinaryOp(const Token *tok, Data &data)
{
ExprEngine::ValuePtr v1 = executeExpression(tok->astOperand1(), data);
@ -2085,6 +2105,9 @@ static ExprEngine::ValuePtr executeExpression1(const Token *tok, Data &data)
return std::make_shared<ExprEngine::IntRange>(std::to_string(v), v, v);
}
if (data.tokenizer->isCPP() && tok->str() == ">>" && !tok->astParent() && tok->isBinaryOp() && Token::Match(tok->astOperand1(), "%name%|::"))
return executeStreamRead(tok, data);
if (tok->astOperand1() && tok->astOperand2())
return executeBinaryOp(tok, data);

View File

@ -60,6 +60,8 @@ private:
TEST_CASE(if5);
TEST_CASE(ifelse1);
TEST_CASE(istream);
TEST_CASE(switch1);
TEST_CASE(switch2);
@ -407,6 +409,20 @@ private:
}
void istream() {
const char code[] = "void foo(const std::string& in) {\n"
" std::istringstream istr(in);\n"
" unsigned short x=5;\n"
" istr >> x;\n"
" x==3;\n"
"}";
ASSERT_EQUALS("(and (>= $2 0) (<= $2 65535))\n"
"(= $2 3)\n"
"z3::sat\n",
expr(code, "=="));
}
void switch1() {
const char code[] = "void f(int x) {\n"
" switch (x) {\n"