aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity/formal/SMTChecker.cpp
diff options
context:
space:
mode:
authorLeonardo Alt <leo@ethereum.org>2018-08-02 05:27:11 +0800
committerLeonardo Alt <leo@ethereum.org>2018-08-02 05:27:11 +0800
commitb6a265551335edeff2f4e43f4a249fabba5381d7 (patch)
treed065338b43059114e78baf702de5065efb4d9a46 /libsolidity/formal/SMTChecker.cpp
parenta78565e44fbcb1d2e3244a6100c0da464ca73c19 (diff)
downloaddexon-solidity-b6a265551335edeff2f4e43f4a249fabba5381d7.tar
dexon-solidity-b6a265551335edeff2f4e43f4a249fabba5381d7.tar.gz
dexon-solidity-b6a265551335edeff2f4e43f4a249fabba5381d7.tar.bz2
dexon-solidity-b6a265551335edeff2f4e43f4a249fabba5381d7.tar.lz
dexon-solidity-b6a265551335edeff2f4e43f4a249fabba5381d7.tar.xz
dexon-solidity-b6a265551335edeff2f4e43f4a249fabba5381d7.tar.zst
dexon-solidity-b6a265551335edeff2f4e43f4a249fabba5381d7.zip
Replace "value" by "<result>" in the SMT model
Diffstat (limited to 'libsolidity/formal/SMTChecker.cpp')
-rw-r--r--libsolidity/formal/SMTChecker.cpp6
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);
}