diff options
| author | Leonardo Alt <leo@ethereum.org> | 2018-08-02 05:27:11 +0800 |
|---|---|---|
| committer | Leonardo Alt <leo@ethereum.org> | 2018-08-02 05:27:11 +0800 |
| commit | b6a265551335edeff2f4e43f4a249fabba5381d7 (patch) | |
| tree | d065338b43059114e78baf702de5065efb4d9a46 | |
| parent | a78565e44fbcb1d2e3244a6100c0da464ca73c19 (diff) | |
| download | dexon-solidity-b6a265551335edeff2f4e43f4a249fabba5381d7.tar.gz dexon-solidity-b6a265551335edeff2f4e43f4a249fabba5381d7.tar.zst dexon-solidity-b6a265551335edeff2f4e43f4a249fabba5381d7.zip | |
Replace "value" by "<result>" in the SMT model
| -rw-r--r-- | libsolidity/formal/SMTChecker.cpp | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 109c8dbe..15300bc6 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -252,14 +252,14 @@ void SMTChecker::checkUnderOverflow(smt::Expression _value, IntegerType const& _ _value < SymbolicIntVariable::minValue(_type), _location, "Underflow (resulting value less than " + formatNumber(_type.minValue()) + ")", - "value", + "<result>", &_value ); checkCondition( _value > SymbolicIntVariable::maxValue(_type), _location, "Overflow (resulting value larger than " + formatNumber(_type.maxValue()) + ")", - "value", + "<result>", &_value ); } @@ -437,7 +437,7 @@ void SMTChecker::arithmeticOperation(BinaryOperation const& _op) 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); } |