From 6a940f0a99e941c48e5deb695e89ac52784c4f3c Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Sun, 21 Jan 2018 13:58:56 +0100 Subject: [SMTChecker] Support to Bool variables --- libsolidity/formal/SymbolicBoolVariable.cpp | 43 +++++++++++++++++++++++++++++ 1 file changed, 43 insertions(+) create mode 100644 libsolidity/formal/SymbolicBoolVariable.cpp (limited to 'libsolidity/formal/SymbolicBoolVariable.cpp') diff --git a/libsolidity/formal/SymbolicBoolVariable.cpp b/libsolidity/formal/SymbolicBoolVariable.cpp new file mode 100644 index 00000000..e2a5687d --- /dev/null +++ b/libsolidity/formal/SymbolicBoolVariable.cpp @@ -0,0 +1,43 @@ +/* + 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; + +SymbolicBoolVariable::SymbolicBoolVariable( + Declaration const* _decl, + smt::SolverInterface&_interface +): + SymbolicVariable(_decl, _interface) +{ + solAssert(m_declaration->type()->category() == Type::Category::Bool, ""); + m_expression = make_shared(m_interface.newFunction(uniqueSymbol(), smt::Sort::Int, smt::Sort::Bool)); +} + +void SymbolicBoolVariable::setZeroValue(int _seq) +{ + m_interface.addAssertion(valueAtSequence(_seq) == smt::Expression(false)); +} + +void SymbolicBoolVariable::setUnknownValue(int) +{ +} -- cgit v1.2.3 From c2d26eb6a20a21f5fe4b5d78a39f8c23f7f3f5cb Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Fri, 9 Mar 2018 16:19:03 +0100 Subject: [SMTChecker_Bool] Fix PR comments; Add support to gt, ge, lt, le. and tests. --- libsolidity/formal/SymbolicBoolVariable.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'libsolidity/formal/SymbolicBoolVariable.cpp') diff --git a/libsolidity/formal/SymbolicBoolVariable.cpp b/libsolidity/formal/SymbolicBoolVariable.cpp index e2a5687d..e5c56e46 100644 --- a/libsolidity/formal/SymbolicBoolVariable.cpp +++ b/libsolidity/formal/SymbolicBoolVariable.cpp @@ -24,12 +24,12 @@ using namespace dev; using namespace dev::solidity; SymbolicBoolVariable::SymbolicBoolVariable( - Declaration const* _decl, + Declaration const& _decl, smt::SolverInterface&_interface ): SymbolicVariable(_decl, _interface) { - solAssert(m_declaration->type()->category() == Type::Category::Bool, ""); + solAssert(m_declaration.type()->category() == Type::Category::Bool, ""); m_expression = make_shared(m_interface.newFunction(uniqueSymbol(), smt::Sort::Int, smt::Sort::Bool)); } -- cgit v1.2.3 From 8d087d1889826271a78ce537b8d1a2ceb11574dd Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Thu, 5 Apr 2018 12:20:41 +0200 Subject: [SMTChecker] Removing usage of UFs to access SSA indices --- libsolidity/formal/SymbolicBoolVariable.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'libsolidity/formal/SymbolicBoolVariable.cpp') diff --git a/libsolidity/formal/SymbolicBoolVariable.cpp b/libsolidity/formal/SymbolicBoolVariable.cpp index e5c56e46..5cf22d7d 100644 --- a/libsolidity/formal/SymbolicBoolVariable.cpp +++ b/libsolidity/formal/SymbolicBoolVariable.cpp @@ -30,7 +30,11 @@ SymbolicBoolVariable::SymbolicBoolVariable( SymbolicVariable(_decl, _interface) { solAssert(m_declaration.type()->category() == Type::Category::Bool, ""); - m_expression = make_shared(m_interface.newFunction(uniqueSymbol(), smt::Sort::Int, smt::Sort::Bool)); +} + +smt::Expression SymbolicBoolVariable::valueAtSequence(int _seq) const +{ + return m_interface.newBool(uniqueSymbol(_seq)); } void SymbolicBoolVariable::setZeroValue(int _seq) -- cgit v1.2.3