From 5497e8ed67dcf781818f16176c2e6780d34ba3b8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Marjam=C3=A4ki?= Date: Sun, 21 Jun 2020 20:05:26 +0200 Subject: [PATCH] ExprEngine; Improved handling of stream read --- lib/exprengine.cpp | 23 +++++++++++++++++++++++ test/testexprengine.cpp | 16 ++++++++++++++++ 2 files changed, 39 insertions(+) diff --git a/lib/exprengine.cpp b/lib/exprengine.cpp index 0cfdb45ef..a25720b4d 100644 --- a/lib/exprengine.cpp +++ b/lib/exprengine.cpp @@ -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(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); diff --git a/test/testexprengine.cpp b/test/testexprengine.cpp index 28cf10f76..c01455cd8 100644 --- a/test/testexprengine.cpp +++ b/test/testexprengine.cpp @@ -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"