diff options
| author | Daniel Kirchner <daniel@ekpyron.org> | 2018-09-03 23:45:58 +0800 |
|---|---|---|
| committer | Daniel Kirchner <daniel@ekpyron.org> | 2018-09-05 18:19:14 +0800 |
| commit | 87804b6419a5894601441efe511015adda5fb119 (patch) | |
| tree | 72fc5334d21933570c8b94ec6a22879c98a692ca /libsolidity/formal | |
| parent | a996ea266c4542b37503c1d2261a17f3d5a55dbb (diff) | |
| download | dexon-solidity-87804b6419a5894601441efe511015adda5fb119.tar.gz dexon-solidity-87804b6419a5894601441efe511015adda5fb119.tar.zst dexon-solidity-87804b6419a5894601441efe511015adda5fb119.zip | |
Split IntegerType into IntegerType and AddressType.
Diffstat (limited to 'libsolidity/formal')
| -rw-r--r-- | libsolidity/formal/SMTChecker.cpp | 5 | ||||
| -rw-r--r-- | libsolidity/formal/SSAVariable.cpp | 2 | ||||
| -rw-r--r-- | libsolidity/formal/SymbolicIntVariable.cpp | 14 |
3 files changed, 15 insertions, 6 deletions
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 88c1e56a..49c90405 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -394,7 +394,7 @@ void SMTChecker::endVisit(Identifier const& _identifier) void SMTChecker::endVisit(Literal const& _literal) { Type const& type = *_literal.annotation().type; - if (type.category() == Type::Category::Integer || type.category() == Type::Category::RationalNumber) + if (type.category() == Type::Category::Integer || type.category() == Type::Category::Address || type.category() == Type::Category::RationalNumber) { if (RationalNumberType const* rational = dynamic_cast<RationalNumberType const*>(&type)) solAssert(!rational->isFractional(), ""); @@ -540,6 +540,8 @@ void SMTChecker::assignment(VariableDeclaration const& _variable, smt::Expressio TypePointer type = _variable.type(); if (auto const* intType = dynamic_cast<IntegerType const*>(type.get())) checkUnderOverflow(_value, *intType, _location); + else if (dynamic_cast<AddressType const*>(type.get())) + checkUnderOverflow(_value, IntegerType(160), _location); m_interface->addAssertion(newValue(_variable) == _value); } @@ -862,6 +864,7 @@ void SMTChecker::createExpr(Expression const& _e) m_expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e))); break; } + case Type::Category::Address: case Type::Category::Integer: m_expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e))); break; diff --git a/libsolidity/formal/SSAVariable.cpp b/libsolidity/formal/SSAVariable.cpp index f3213e03..4fc2dd45 100644 --- a/libsolidity/formal/SSAVariable.cpp +++ b/libsolidity/formal/SSAVariable.cpp @@ -50,7 +50,7 @@ bool SSAVariable::isSupportedType(Type::Category _category) bool SSAVariable::isInteger(Type::Category _category) { - return _category == Type::Category::Integer; + return _category == Type::Category::Integer || _category == Type::Category::Address; } bool SSAVariable::isBool(Type::Category _category) diff --git a/libsolidity/formal/SymbolicIntVariable.cpp b/libsolidity/formal/SymbolicIntVariable.cpp index 5e71fdcc..4f65b1fd 100644 --- a/libsolidity/formal/SymbolicIntVariable.cpp +++ b/libsolidity/formal/SymbolicIntVariable.cpp @@ -29,7 +29,11 @@ SymbolicIntVariable::SymbolicIntVariable( ): SymbolicVariable(_decl, _interface) { - solAssert(m_declaration.type()->category() == Type::Category::Integer, ""); + solAssert( + m_declaration.type()->category() == Type::Category::Integer || + m_declaration.type()->category() == Type::Category::Address, + "" + ); } smt::Expression SymbolicIntVariable::valueAtSequence(int _seq) const @@ -44,9 +48,11 @@ void SymbolicIntVariable::setZeroValue(int _seq) void SymbolicIntVariable::setUnknownValue(int _seq) { - auto const& intType = dynamic_cast<IntegerType const&>(*m_declaration.type()); - m_interface.addAssertion(valueAtSequence(_seq) >= minValue(intType)); - m_interface.addAssertion(valueAtSequence(_seq) <= maxValue(intType)); + auto intType = dynamic_pointer_cast<IntegerType const>(m_declaration.type()); + if (!intType) + intType = make_shared<IntegerType>(160); + m_interface.addAssertion(valueAtSequence(_seq) >= minValue(*intType)); + m_interface.addAssertion(valueAtSequence(_seq) <= maxValue(*intType)); } smt::Expression SymbolicIntVariable::minValue(IntegerType const& _t) |