diff options
| author | chriseth <chris@ethereum.org> | 2018-09-06 03:40:49 +0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-09-06 03:40:49 +0800 |
| commit | 08a7a51f071e2ef30db011fb36d505c7615785ec (patch) | |
| tree | 603e8a79d31e552c9e308a87e3d90f3fcccb854d /libsolidity/formal/SMTChecker.cpp | |
| parent | 9cb72fe6ca0260e465ed3a1700cc4a890480df4f (diff) | |
| parent | 87804b6419a5894601441efe511015adda5fb119 (diff) | |
| download | dexon-solidity-08a7a51f071e2ef30db011fb36d505c7615785ec.tar dexon-solidity-08a7a51f071e2ef30db011fb36d505c7615785ec.tar.gz dexon-solidity-08a7a51f071e2ef30db011fb36d505c7615785ec.tar.bz2 dexon-solidity-08a7a51f071e2ef30db011fb36d505c7615785ec.tar.lz dexon-solidity-08a7a51f071e2ef30db011fb36d505c7615785ec.tar.xz dexon-solidity-08a7a51f071e2ef30db011fb36d505c7615785ec.tar.zst dexon-solidity-08a7a51f071e2ef30db011fb36d505c7615785ec.zip | |
Merge pull request #4887 from ethereum/addressSplit
Split IntegerType into IntegerType and AddressType.
Diffstat (limited to 'libsolidity/formal/SMTChecker.cpp')
| -rw-r--r-- | libsolidity/formal/SMTChecker.cpp | 5 |
1 files changed, 4 insertions, 1 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; |