diff options
Diffstat (limited to 'libsolidity/formal/Why3Translator.h')
| -rw-r--r-- | libsolidity/formal/Why3Translator.h | 17 |
1 files changed, 15 insertions, 2 deletions
diff --git a/libsolidity/formal/Why3Translator.h b/libsolidity/formal/Why3Translator.h index 588b6d80..e5b16844 100644 --- a/libsolidity/formal/Why3Translator.h +++ b/libsolidity/formal/Why3Translator.h @@ -80,6 +80,7 @@ private: virtual bool visit(IfStatement const& _node) override; virtual bool visit(WhileStatement const& _node) override; virtual bool visit(Return const& _node) override; + virtual bool visit(Throw const& _node) override; virtual bool visit(VariableDeclarationStatement const& _node) override; virtual bool visit(ExpressionStatement const&) override; virtual bool visit(Assignment const& _node) override; @@ -104,6 +105,9 @@ private: bool isLocalVariable(VariableDeclaration const* _var) const; bool isLocalVariable(std::string const& _name) const; + /// @returns a string representing an expression that is a copy of this.storage + std::string copyOfStorage() const; + /// Visits the givin statement and indents it unless it is a block /// (which does its own indentation). void visitIndentedUnlessBlock(Statement const& _statement); @@ -117,7 +121,17 @@ private: bool m_seenContract = false; bool m_errorOccured = false; - std::vector<VariableDeclaration const*> m_stateVariables; + /// Metadata relating to the current contract + struct ContractMetadata + { + ContractDefinition const* contract = nullptr; + std::vector<VariableDeclaration const*> stateVariables; + + void reset() { contract = nullptr; stateVariables.clear(); } + }; + + ContractMetadata m_currentContract; + bool m_currentLValueIsRef = false; std::map<std::string, VariableDeclaration const*> m_localVariables; struct Line @@ -129,6 +143,5 @@ private: ErrorList& m_errors; }; - } } |