ExprEngine; Simple handling of increment/decrement
This commit is contained in:
parent
a5a3738df4
commit
6ec15b6d7b
|
@ -1442,6 +1442,16 @@ static ExprEngine::ValuePtr executeAssign(const Token *tok, Data &data)
|
||||||
return assignValue;
|
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<ExprEngine::BinOpResult>(tok->str().substr(0,1), beforeValue, std::make_shared<ExprEngine::IntRange>("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
|
#ifdef USE_Z3
|
||||||
static void checkContract(Data &data, const Token *tok, const Function *function, const std::vector<ExprEngine::ValuePtr> &argValues)
|
static void checkContract(Data &data, const Token *tok, const Function *function, const std::vector<ExprEngine::ValuePtr> &argValues)
|
||||||
|
@ -1824,6 +1834,9 @@ static ExprEngine::ValuePtr executeExpression1(const Token *tok, Data &data)
|
||||||
// TODO: Handle more operators
|
// TODO: Handle more operators
|
||||||
return executeAssign(tok, data);
|
return executeAssign(tok, data);
|
||||||
|
|
||||||
|
if (tok->tokType() == Token::Type::eIncDecOp)
|
||||||
|
return executeIncDec(tok, data);
|
||||||
|
|
||||||
if (tok->astOperand1() && tok->astOperand2() && tok->str() == "[")
|
if (tok->astOperand1() && tok->astOperand2() && tok->str() == "[")
|
||||||
return executeArrayIndex(tok, data);
|
return executeArrayIndex(tok, data);
|
||||||
|
|
||||||
|
|
|
@ -52,7 +52,7 @@ private:
|
||||||
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());
|
||||||
|
|
||||||
check("void foo() { int x; x++; }");
|
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());
|
||||||
}
|
}
|
||||||
};
|
};
|
||||||
|
|
||||||
|
|
|
@ -446,7 +446,7 @@ private:
|
||||||
" x == 1;\n"
|
" x == 1;\n"
|
||||||
"}";
|
"}";
|
||||||
ASSERT_EQUALS("(and (>= $2 (- 2147483648)) (<= $2 2147483647))\n"
|
ASSERT_EQUALS("(and (>= $2 (- 2147483648)) (<= $2 2147483647))\n"
|
||||||
"(= $2 1)\n"
|
"(= (+ $2 1) 1)\n"
|
||||||
"z3::sat\n",
|
"z3::sat\n",
|
||||||
expr(code, "=="));
|
expr(code, "=="));
|
||||||
}
|
}
|
||||||
|
|
Loading…
Reference in New Issue