diff options
Diffstat (limited to 'libsolidity/formal/SMTChecker.h')
| -rw-r--r-- | libsolidity/formal/SMTChecker.h | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index 7e7996cf..50d40ab9 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -50,6 +50,8 @@ private: // because the order of expression evaluation is undefined // TODO: or just force a certain order, but people might have a different idea about that. + virtual bool visit(ContractDefinition const& _node) override; + virtual void endVisit(ContractDefinition const& _node) override; virtual void endVisit(VariableDeclaration const& _node) override; virtual bool visit(FunctionDefinition const& _node) override; virtual void endVisit(FunctionDefinition const& _node) override; @@ -111,6 +113,7 @@ private: smt::CheckResult checkSatisfiable(); void initializeLocalVariables(FunctionDefinition const& _function); + void resetStateVariables(); void resetVariables(std::vector<Declaration const*> _variables); /// Given two different branches and the touched variables, /// merge the touched variables into after-branch ite variables @@ -160,9 +163,10 @@ private: std::shared_ptr<smt::SolverInterface> m_interface; std::shared_ptr<VariableUsage> m_variableUsage; - bool m_conditionalExecutionHappened = false; + bool m_loopExecutionHappened = false; std::map<Expression const*, smt::Expression> m_expressions; std::map<Declaration const*, SSAVariable> m_variables; + std::map<Declaration const*, SSAVariable> m_stateVariables; std::vector<smt::Expression> m_pathConditions; ErrorReporter& m_errorReporter; |