From cff0836c032ecee2710f1c17c49eec0a3b4aa9fc Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Wed, 28 Feb 2018 18:00:13 +0100 Subject: Fix PR comments --- libsolidity/formal/SSAVariable.cpp | 12 +++++++----- libsolidity/formal/SSAVariable.h | 12 ++++++++---- libsolidity/formal/SymbolicIntVariable.cpp | 8 +++++--- libsolidity/formal/SymbolicIntVariable.h | 10 ++++++---- libsolidity/formal/SymbolicVariable.cpp | 8 +++++--- libsolidity/formal/SymbolicVariable.h | 10 ++++++---- 6 files changed, 37 insertions(+), 23 deletions(-) (limited to 'libsolidity/formal') diff --git a/libsolidity/formal/SSAVariable.cpp b/libsolidity/formal/SSAVariable.cpp index 7f214687..4e6bcbcb 100644 --- a/libsolidity/formal/SSAVariable.cpp +++ b/libsolidity/formal/SSAVariable.cpp @@ -25,13 +25,15 @@ using namespace std; using namespace dev; using namespace dev::solidity; -SSAVariable::SSAVariable(Declaration const* _decl, - smt::SolverInterface& _interface) +SSAVariable::SSAVariable( + Declaration const* _decl, + smt::SolverInterface& _interface +) { resetIndex(); if (dynamic_cast(_decl->type().get())) - m_symbVar = make_shared(_decl, _interface); + m_symbolicVar = make_shared(_decl, _interface); else { solAssert(false, ""); @@ -62,10 +64,10 @@ int SSAVariable::next() const void SSAVariable::setZeroValue() { - m_symbVar->setZeroValue(index()); + m_symbolicVar->setZeroValue(index()); } void SSAVariable::setUnknownValue() { - m_symbVar->setUnknownValue(index()); + m_symbolicVar->setUnknownValue(index()); } diff --git a/libsolidity/formal/SSAVariable.h b/libsolidity/formal/SSAVariable.h index b87693c2..4ec92aa1 100644 --- a/libsolidity/formal/SSAVariable.h +++ b/libsolidity/formal/SSAVariable.h @@ -36,8 +36,10 @@ class SSAVariable public: /// @param _decl Used to determine the type and forwarded to the symbolic var. /// @param _interface Forwarded to the symbolic var such that it can give constraints to the solver. - explicit SSAVariable(Declaration const* _decl, - smt::SolverInterface& _interface); + SSAVariable( + Declaration const* _decl, + smt::SolverInterface& _interface + ); SSAVariable(SSAVariable const&) = default; SSAVariable(SSAVariable&&) = default; SSAVariable& operator=(SSAVariable const&) = default; @@ -45,7 +47,9 @@ public: void resetIndex(); + /// This function returns the current index of this SSA variable. int index() const; + /// This function returns the next free index of this SSA variable. int next() const; int operator++() @@ -74,10 +78,10 @@ public: private: smt::Expression valueAtSequence(int _seq) const { - return (*m_symbVar)(_seq); + return (*m_symbolicVar)(_seq); } - std::shared_ptr m_symbVar = nullptr; + std::shared_ptr m_symbolicVar = nullptr; int m_currentSequenceCounter; /// The next free sequence counter is a shared pointer because we want /// the copy and the copied to share it. diff --git a/libsolidity/formal/SymbolicIntVariable.cpp b/libsolidity/formal/SymbolicIntVariable.cpp index c206f1cd..d08dc155 100644 --- a/libsolidity/formal/SymbolicIntVariable.cpp +++ b/libsolidity/formal/SymbolicIntVariable.cpp @@ -23,9 +23,11 @@ using namespace std; using namespace dev; using namespace dev::solidity; -SymbolicIntVariable::SymbolicIntVariable(Declaration const* _decl, - smt::SolverInterface&_interface) - : SymbolicVariable(_decl, _interface) +SymbolicIntVariable::SymbolicIntVariable( + Declaration const* _decl, + smt::SolverInterface& _interface +): + SymbolicVariable(_decl, _interface) { solAssert(m_declaration->type()->category() == Type::Category::Integer, ""); m_expression = make_shared(m_interface.newFunction(uniqueSymbol(), smt::Sort::Int, smt::Sort::Int)); diff --git a/libsolidity/formal/SymbolicIntVariable.h b/libsolidity/formal/SymbolicIntVariable.h index 0066bb75..8a9b5d5d 100644 --- a/libsolidity/formal/SymbolicIntVariable.h +++ b/libsolidity/formal/SymbolicIntVariable.h @@ -29,11 +29,13 @@ namespace solidity /** * Specialization of SymbolicVariable for Integers */ -class SymbolicIntVariable : public SymbolicVariable +class SymbolicIntVariable: public SymbolicVariable { public: - explicit SymbolicIntVariable(Declaration const* _decl, - smt::SolverInterface& _interface); + SymbolicIntVariable( + Declaration const* _decl, + smt::SolverInterface& _interface + ); SymbolicIntVariable(SymbolicIntVariable const&) = default; SymbolicIntVariable(SymbolicIntVariable&&) = default; SymbolicIntVariable& operator=(SymbolicIntVariable const&) = default; @@ -41,7 +43,7 @@ public: /// Sets the var to 0. void setZeroValue(int _seq); - /// Sets the valid interval for the var. + /// Sets the variable to the full valid value range. void setUnknownValue(int _seq); static smt::Expression minValue(IntegerType const& _t); diff --git a/libsolidity/formal/SymbolicVariable.cpp b/libsolidity/formal/SymbolicVariable.cpp index 13f5d9b6..629049ea 100644 --- a/libsolidity/formal/SymbolicVariable.cpp +++ b/libsolidity/formal/SymbolicVariable.cpp @@ -23,9 +23,11 @@ using namespace std; using namespace dev; using namespace dev::solidity; -SymbolicVariable::SymbolicVariable(Declaration const* _decl, - smt::SolverInterface& _interface) - : m_declaration(_decl), +SymbolicVariable::SymbolicVariable( + Declaration const* _decl, + smt::SolverInterface& _interface +): + m_declaration(_decl), m_interface(_interface) { } diff --git a/libsolidity/formal/SymbolicVariable.h b/libsolidity/formal/SymbolicVariable.h index 66633b73..2b59e57a 100644 --- a/libsolidity/formal/SymbolicVariable.h +++ b/libsolidity/formal/SymbolicVariable.h @@ -36,8 +36,10 @@ class Declaration; class SymbolicVariable { public: - explicit SymbolicVariable(Declaration const* _decl, - smt::SolverInterface& _interface); + SymbolicVariable( + Declaration const* _decl, + smt::SolverInterface& _interface + ); SymbolicVariable(SymbolicVariable const&) = default; SymbolicVariable(SymbolicVariable&&) = default; SymbolicVariable& operator=(SymbolicVariable const&) = default; @@ -52,8 +54,8 @@ public: /// Sets the var to the default value of its type. virtual void setZeroValue(int _seq) = 0; - /// The unknown value depends on the type. For example, an interval is set for Integers. - /// This is decided by the subclasses. + /// The unknown value is the full range of valid values, + /// and that's sub-type dependent. virtual void setUnknownValue(int _seq) = 0; protected: -- cgit