diff options
| author | Leonardo Alt <leonardoaltt@gmail.com> | 2018-02-17 16:34:38 +0800 |
|---|---|---|
| committer | Leonardo Alt <leonardoaltt@gmail.com> | 2018-03-01 01:05:20 +0800 |
| commit | 3b2851ee4163bcfbca9e4e23650dfeee1a06653a (patch) | |
| tree | b63e69be2bd74b2809d8933aa01c15d7f4a321c8 /libsolidity/formal/SMTChecker.cpp | |
| parent | f41591b3ddfd3e5c065271058dadb3c6b7f31bbb (diff) | |
| download | dexon-solidity-3b2851ee4163bcfbca9e4e23650dfeee1a06653a.tar.gz dexon-solidity-3b2851ee4163bcfbca9e4e23650dfeee1a06653a.tar.zst dexon-solidity-3b2851ee4163bcfbca9e4e23650dfeee1a06653a.zip | |
Integer min and max values placed under SymbolicIntVar instead of SMTChecker
Diffstat (limited to 'libsolidity/formal/SMTChecker.cpp')
| -rw-r--r-- | libsolidity/formal/SMTChecker.cpp | 14 |
1 files changed, 3 insertions, 11 deletions
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 37dce96c..ad42c105 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -24,6 +24,7 @@ #endif #include <libsolidity/formal/SSAVariable.h> +#include <libsolidity/formal/SymbolicIntVariable.h> #include <libsolidity/formal/VariableUsage.h> #include <libsolidity/interface/ErrorReporter.h> @@ -244,14 +245,14 @@ void SMTChecker::endVisit(TupleExpression const& _tuple) void SMTChecker::checkUnderOverflow(smt::Expression _value, IntegerType const& _type, SourceLocation const& _location) { checkCondition( - _value < minValue(_type), + _value < SymbolicIntVariable::minValue(_type), _location, "Underflow (resulting value less than " + formatNumber(_type.minValue()) + ")", "value", &_value ); checkCondition( - _value > maxValue(_type), + _value > SymbolicIntVariable::maxValue(_type), _location, "Overflow (resulting value larger than " + formatNumber(_type.maxValue()) + ")", "value", @@ -828,15 +829,6 @@ void SMTChecker::defineExpr(Expression const& _e, smt::Expression _value) m_interface->addAssertion(expr(_e) == _value); } -smt::Expression SMTChecker::minValue(IntegerType const& _t) -{ - return smt::Expression(_t.minValue()); -} - -smt::Expression SMTChecker::maxValue(IntegerType const& _t) -{ - return smt::Expression(_t.maxValue()); -} void SMTChecker::popPathCondition() { solAssert(m_pathConditions.size() > 0, "Cannot pop path condition, empty."); |