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/SymbolicIntVariable.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/SymbolicIntVariable.cpp')
| -rw-r--r-- | libsolidity/formal/SymbolicIntVariable.cpp | 14 |
1 files changed, 10 insertions, 4 deletions
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) |