aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity/formal/SymbolicIntVariable.cpp
diff options
context:
space:
mode:
authorLeonardo Alt <leo@ethereum.org>2018-10-18 21:03:52 +0800
committerLeonardo Alt <leo@ethereum.org>2018-10-19 21:52:16 +0800
commitb46b827c30584968c6815b456b8c0c775c35ae48 (patch)
tree7ea55c6c685cc81779d5dd7bc3f44da22918840e /libsolidity/formal/SymbolicIntVariable.cpp
parentc13b5280c1b44f18a2a1fb61ef5556e91c5678e7 (diff)
downloaddexon-solidity-b46b827c30584968c6815b456b8c0c775c35ae48.tar.gz
dexon-solidity-b46b827c30584968c6815b456b8c0c775c35ae48.tar.zst
dexon-solidity-b46b827c30584968c6815b456b8c0c775c35ae48.zip
[SMTChecker] Support msg.*, tx.*, block.*, gasleft and blockhash
Diffstat (limited to 'libsolidity/formal/SymbolicIntVariable.cpp')
-rw-r--r--libsolidity/formal/SymbolicIntVariable.cpp8
1 files changed, 4 insertions, 4 deletions
diff --git a/libsolidity/formal/SymbolicIntVariable.cpp b/libsolidity/formal/SymbolicIntVariable.cpp
index cf1a7486..a5939842 100644
--- a/libsolidity/formal/SymbolicIntVariable.cpp
+++ b/libsolidity/formal/SymbolicIntVariable.cpp
@@ -24,13 +24,13 @@ using namespace dev;
using namespace dev::solidity;
SymbolicIntVariable::SymbolicIntVariable(
- Type const& _type,
+ TypePointer _type,
string const& _uniqueName,
smt::SolverInterface& _interface
):
- SymbolicVariable(_type, _uniqueName, _interface)
+ SymbolicVariable(move(_type), _uniqueName, _interface)
{
- solAssert(isNumber(_type.category()), "");
+ solAssert(isNumber(m_type->category()), "");
}
smt::Expression SymbolicIntVariable::valueAtIndex(int _index) const
@@ -45,7 +45,7 @@ void SymbolicIntVariable::setZeroValue()
void SymbolicIntVariable::setUnknownValue()
{
- auto intType = dynamic_cast<IntegerType const*>(&m_type);
+ auto intType = dynamic_cast<IntegerType const*>(m_type.get());
solAssert(intType, "");
m_interface.addAssertion(currentValue() >= minValue(*intType));
m_interface.addAssertion(currentValue() <= maxValue(*intType));