cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Replace "value" by "<result>" in the SMT model

Browse Source
This commit is contained in:
Leonardo Alt 2018-08-01 23:27:11 +02:00
parent a78565e44f
commit b6a2655513
1 changed files with 3 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
libsolidity/formal/SMTChecker.cpp
View File

@ -252,14 +252,14 @@ void SMTChecker::checkUnderOverflow(smt::Expression _value, IntegerType const& _
_value < SymbolicIntVariable::minValue(_type), _value < SymbolicIntVariable::minValue(_type),
_location, _location,
"Underflow (resulting value less than " + formatNumber(_type.minValue()) + ")", "Underflow (resulting value less than " + formatNumber(_type.minValue()) + ")",
"value", "<result>",
&_value &_value
); );
checkCondition( checkCondition(
_value > SymbolicIntVariable::maxValue(_type), _value > SymbolicIntVariable::maxValue(_type),
_location, _location,
"Overflow (resulting value larger than " + formatNumber(_type.maxValue()) + ")", "Overflow (resulting value larger than " + formatNumber(_type.maxValue()) + ")",
"value", "<result>",
&_value &_value
); );
} }
@ -437,7 +437,7 @@ void SMTChecker::arithmeticOperation(BinaryOperation const& _op)
if (_op.getOperator() == Token::Div) if (_op.getOperator() == Token::Div)
{ {
checkCondition(right == 0, _op.location(), "Division by zero", "value", &right); checkCondition(right == 0, _op.location(), "Division by zero", "<result>", &right);
m_interface->addAssertion(right != 0); m_interface->addAssertion(right != 0);
} }