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/SSAVariable.cpp | 21 +++++++++++++++------ 1 file changed, 15 insertions(+), 6 deletions(-) (limited to 'libsolidity/formal/SSAVariable.cpp') diff --git a/libsolidity/formal/SSAVariable.cpp b/libsolidity/formal/SSAVariable.cpp index 4f8080ab..3f2a61f1 100644 --- a/libsolidity/formal/SSAVariable.cpp +++ b/libsolidity/formal/SSAVariable.cpp @@ -27,15 +27,15 @@ using namespace dev; using namespace dev::solidity; SSAVariable::SSAVariable( - Declaration const* _decl, + Declaration const& _decl, smt::SolverInterface& _interface ) { resetIndex(); - if (dynamic_cast(_decl->type().get())) + if (typeInteger(_decl.type()->category())) m_symbolicVar = make_shared(_decl, _interface); - else if (dynamic_cast(_decl->type().get())) + else if (typeBool(_decl.type()->category())) m_symbolicVar = make_shared(_decl, _interface); else { @@ -43,10 +43,19 @@ SSAVariable::SSAVariable( } } -bool SSAVariable::supportedType(Type const* _decl) +bool SSAVariable::supportedType(Type::Category _category) { - return dynamic_cast(_decl) || - dynamic_cast(_decl); + return typeInteger(_category) || typeBool(_category); +} + +bool SSAVariable::typeInteger(Type::Category _category) +{ + return _category == Type::Category::Integer; +} + +bool SSAVariable::typeBool(Type::Category _category) +{ + return _category == Type::Category::Bool; } void SSAVariable::resetIndex() -- cgit v1.2.3