aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity/formal/SMTChecker.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'libsolidity/formal/SMTChecker.cpp')
-rw-r--r--libsolidity/formal/SMTChecker.cpp15
1 files changed, 13 insertions, 2 deletions
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)