From 4117e859eb5780873177cf1c93eb8379e17ed247 Mon Sep 17 00:00:00 2001 From: Leonardo Alt Date: Mon, 30 Apr 2018 16:30:41 +0200 Subject: [SMTChecker] Declaring all state vars before any function is visited --- libsolidity/formal/SMTChecker.cpp | 15 +++++++++++++-- libsolidity/formal/SMTChecker.h | 2 ++ 2 files changed, 15 insertions(+), 2 deletions(-) (limited to 'libsolidity/formal') diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 358f1c58..425c5c1e 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -58,12 +58,23 @@ void SMTChecker::analyze(SourceUnit const& _source) _source.accept(*this); } +bool SMTChecker::visit(ContractDefinition const& _contract) +{ + for (auto _var : _contract.stateVariables()) + if (_var->type()->isValueType()) + createVariable(*_var); + return true; +} + +void SMTChecker::endVisit(ContractDefinition const&) +{ + m_stateVariables.clear(); +} + void SMTChecker::endVisit(VariableDeclaration const& _varDecl) { if (_varDecl.isLocalVariable() && _varDecl.type()->isValueType() &&_varDecl.value()) assignment(_varDecl, *_varDecl.value(), _varDecl.location()); - else if (_varDecl.isStateVariable() && _varDecl.type()->isValueType()) - createVariable(_varDecl); } bool SMTChecker::visit(FunctionDefinition const& _function) diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index 6e64235e..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; -- cgit