cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Fix PR comments

Browse Source
This commit is contained in:
Leonardo Alt 2018-02-28 18:00:13 +01:00
parent 21c6b80fc9
commit cff0836c03
6 changed files with 37 additions and 23 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
libsolidity/formal/SSAVariable.cpp
View File

@ -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<IntegerType const*>(_decl->type().get()))
m_symbVar = make_shared<SymbolicIntVariable>(_decl, _interface);
m_symbolicVar = make_shared<SymbolicIntVariable>(_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());
}

12
libsolidity/formal/SSAVariable.h
View File

@ -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<SymbolicVariable> m_symbVar = nullptr;
std::shared_ptr<SymbolicVariable> 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.

8
libsolidity/formal/SymbolicIntVariable.cpp
View File

@ -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<smt::Expression>(m_interface.newFunction(uniqueSymbol(), smt::Sort::Int, smt::Sort::Int));

10
libsolidity/formal/SymbolicIntVariable.h
View File

@ -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);

8
libsolidity/formal/SymbolicVariable.cpp
View File

@ -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)
{
}

10
libsolidity/formal/SymbolicVariable.h
View File

@ -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: