Verification; Fix false positive in while loops
This commit is contained in:
parent
043634be27
commit
d4ec8075a4
|
@ -1563,7 +1563,7 @@ static void execute(const Token *start, const Token *end, Data &data)
|
||||||
if (changedVariables.find(varid) != changedVariables.end())
|
if (changedVariables.find(varid) != changedVariables.end())
|
||||||
continue;
|
continue;
|
||||||
changedVariables.insert(varid);
|
changedVariables.insert(varid);
|
||||||
data.assignValue(tok2, varid, createVariableValue(*tok2->astOperand1()->variable(), data));
|
data.assignValue(tok2, varid, getValueRangeFromValueType(data.getNewSymbolName(), tok2->astOperand1()->valueType(), *data.settings));
|
||||||
} else if (Token::Match(tok2, "++|--") && tok2->astOperand1() && tok2->astOperand1()->variable()) {
|
} else if (Token::Match(tok2, "++|--") && tok2->astOperand1() && tok2->astOperand1()->variable()) {
|
||||||
// give variable "any" value
|
// give variable "any" value
|
||||||
const Token *vartok = tok2->astOperand1();
|
const Token *vartok = tok2->astOperand1();
|
||||||
|
|
|
@ -318,9 +318,9 @@ private:
|
||||||
" x = x + 34;\n"
|
" x = x + 34;\n"
|
||||||
" x == 340;\n"
|
" x == 340;\n"
|
||||||
"}";
|
"}";
|
||||||
ASSERT_EQUALS("(declare-fun $4 () Int)\n"
|
ASSERT_EQUALS("(declare-fun $2 () Int)\n"
|
||||||
"(assert (and (>= $4 (- 2147483648)) (<= $4 2147483647)))\n"
|
"(assert (and (>= $2 (- 2147483648)) (<= $2 2147483647)))\n"
|
||||||
"(assert (= (+ $4 34) 340))\n"
|
"(assert (= (+ $2 34) 340))\n"
|
||||||
"z3::sat",
|
"z3::sat",
|
||||||
expr(code, "=="));
|
expr(code, "=="));
|
||||||
}
|
}
|
||||||
|
|
Loading…
Reference in New Issue