diff --git a/lib/exprengine.cpp b/lib/exprengine.cpp index 4b9dc65e6..04cdad1b2 100644 --- a/lib/exprengine.cpp +++ b/lib/exprengine.cpp @@ -1442,6 +1442,16 @@ static ExprEngine::ValuePtr executeAssign(const Token *tok, Data &data) return assignValue; } +static ExprEngine::ValuePtr executeIncDec(const Token *tok, Data &data) +{ + ExprEngine::ValuePtr beforeValue = executeExpression(tok->astOperand1(), data); + ExprEngine::ValuePtr assignValue = simplifyValue(std::make_shared(tok->str().substr(0,1), beforeValue, std::make_shared("1", 1, 1))); + if (tok->astOperand1()->varId() > 0) + data.assignValue(tok->astOperand1(), tok->astOperand1()->varId(), assignValue); + else + throw BugHuntingException(tok, "Unhandled increment/decrement operand"); + return (precedes(tok, tok->astOperand1())) ? assignValue : beforeValue; +} #ifdef USE_Z3 static void checkContract(Data &data, const Token *tok, const Function *function, const std::vector &argValues) @@ -1824,6 +1834,9 @@ static ExprEngine::ValuePtr executeExpression1(const Token *tok, Data &data) // TODO: Handle more operators return executeAssign(tok, data); + if (tok->tokType() == Token::Type::eIncDecOp) + return executeIncDec(tok, data); + if (tok->astOperand1() && tok->astOperand2() && tok->str() == "[") return executeArrayIndex(tok, data); diff --git a/test/testbughuntingchecks.cpp b/test/testbughuntingchecks.cpp index ce225d238..077381a99 100644 --- a/test/testbughuntingchecks.cpp +++ b/test/testbughuntingchecks.cpp @@ -52,7 +52,7 @@ private: ASSERT_EQUALS("[test.cpp:1]: (error) Cannot determine that 'x' is initialized\n", errout.str()); check("void foo() { int x; x++; }"); - TODO_ASSERT_EQUALS("[test.cpp:1]: (error) Cannot determine that 'x' is initialized\n", "", errout.str()); + ASSERT_EQUALS("[test.cpp:1]: (error) Cannot determine that 'x' is initialized\n", errout.str()); } }; diff --git a/test/testexprengine.cpp b/test/testexprengine.cpp index 8ab8d6ee4..0cb121931 100644 --- a/test/testexprengine.cpp +++ b/test/testexprengine.cpp @@ -446,7 +446,7 @@ private: " x == 1;\n" "}"; ASSERT_EQUALS("(and (>= $2 (- 2147483648)) (<= $2 2147483647))\n" - "(= $2 1)\n" + "(= (+ $2 1) 1)\n" "z3::sat\n", expr(code, "==")); }