diff options
| author | Leonardo Alt <leonardoaltt@gmail.com> | 2018-03-01 01:00:13 +0800 |
|---|---|---|
| committer | Leonardo Alt <leonardoaltt@gmail.com> | 2018-03-01 01:05:20 +0800 |
| commit | cff0836c032ecee2710f1c17c49eec0a3b4aa9fc (patch) | |
| tree | 64349305119d23e022c6a407da2e3e146e6f40ea /libsolidity/formal/SSAVariable.h | |
| parent | 21c6b80fc98f6d584f240a47d4a01827768f18f3 (diff) | |
| download | dexon-solidity-cff0836c032ecee2710f1c17c49eec0a3b4aa9fc.tar.gz dexon-solidity-cff0836c032ecee2710f1c17c49eec0a3b4aa9fc.tar.zst dexon-solidity-cff0836c032ecee2710f1c17c49eec0a3b4aa9fc.zip | |
Fix PR comments
Diffstat (limited to 'libsolidity/formal/SSAVariable.h')
| -rw-r--r-- | libsolidity/formal/SSAVariable.h | 12 |
1 files changed, 8 insertions, 4 deletions
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<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. |