From afe83cc28b2b0f31a00911ed0b540e1beb038736 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Wed, 17 Oct 2018 15:56:44 +0200 Subject: Refactor SymbolicAddressVariable and SymbolicVariable allocation --- libsolidity/formal/SymbolicAddressVariable.cpp | 41 ++++++++++++++++++++++++++ 1 file changed, 41 insertions(+) create mode 100644 libsolidity/formal/SymbolicAddressVariable.cpp (limited to 'libsolidity/formal/SymbolicAddressVariable.cpp') diff --git a/libsolidity/formal/SymbolicAddressVariable.cpp b/libsolidity/formal/SymbolicAddressVariable.cpp new file mode 100644 index 00000000..68b95080 --- /dev/null +++ b/libsolidity/formal/SymbolicAddressVariable.cpp @@ -0,0 +1,41 @@ +/* + This file is part of solidity. + + solidity is free software: you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation, either version 3 of the License, or + (at your option) any later version. + + solidity is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + + You should have received a copy of the GNU General Public License + along with solidity. If not, see . +*/ + +#include + +#include + +using namespace std; +using namespace dev; +using namespace dev::solidity; + +SymbolicAddressVariable::SymbolicAddressVariable( + Type const& _type, + string const& _uniqueName, + smt::SolverInterface& _interface +): + SymbolicIntVariable(_type, _uniqueName, _interface) +{ + solAssert(isAddress(_type.category()), ""); +} + +void SymbolicAddressVariable::setUnknownValue() +{ + IntegerType intType{160}; + m_interface.addAssertion(currentValue() >= minValue(intType)); + m_interface.addAssertion(currentValue() <= maxValue(intType)); +} -- cgit v1.2.3