diff options
Diffstat (limited to 'libsolidity/formal/SMTChecker.cpp')
| -rw-r--r-- | libsolidity/formal/SMTChecker.cpp | 33 |
1 files changed, 29 insertions, 4 deletions
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index c4dee22d..358f1c58 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -62,6 +62,8 @@ 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) @@ -72,13 +74,13 @@ bool SMTChecker::visit(FunctionDefinition const& _function) "Assertion checker does not yet support constructors and functions with modifiers." ); m_currentFunction = &_function; - // We only handle local variables, so we clear at the beginning of the function. - // If we add storage variables, those should be cleared differently. m_interface->reset(); m_variables.clear(); + m_variables.insert(m_stateVariables.begin(), m_stateVariables.end()); m_pathConditions.clear(); m_loopExecutionHappened = false; initializeLocalVariables(_function); + resetStateVariables(); return true; } @@ -586,6 +588,12 @@ void SMTChecker::checkCondition( expressionsToEvaluate.emplace_back(currentValue(*var)); expressionNames.push_back(var->name()); } + for (auto const& var: m_stateVariables) + if (knownVariable(*var.first)) + { + expressionsToEvaluate.emplace_back(currentValue(*var.first)); + expressionNames.push_back(var.first->name()); + } } smt::CheckResult result; vector<string> values; @@ -607,7 +615,8 @@ void SMTChecker::checkCondition( message << " for:\n"; solAssert(values.size() == expressionNames.size(), ""); for (size_t i = 0; i < values.size(); ++i) - message << " " << expressionNames.at(i) << " = " << values.at(i) << "\n"; + if (expressionsToEvaluate.at(i).name != values.at(i)) + message << " " << expressionNames.at(i) << " = " << values.at(i) << "\n"; } else message << "."; @@ -722,6 +731,15 @@ void SMTChecker::initializeLocalVariables(FunctionDefinition const& _function) setZeroValue(*retParam); } +void SMTChecker::resetStateVariables() +{ + for (auto const& variable: m_stateVariables) + { + newValue(*variable.first); + setUnknownValue(*variable.first); + } +} + void SMTChecker::resetVariables(vector<Declaration const*> _variables) { for (auto const* decl: _variables) @@ -752,7 +770,14 @@ bool SMTChecker::createVariable(VariableDeclaration const& _varDecl) if (SSAVariable::isSupportedType(_varDecl.type()->category())) { solAssert(m_variables.count(&_varDecl) == 0, ""); - m_variables.emplace(&_varDecl, SSAVariable(_varDecl, *m_interface)); + solAssert(m_stateVariables.count(&_varDecl) == 0, ""); + if (_varDecl.isLocalVariable()) + m_variables.emplace(&_varDecl, SSAVariable(_varDecl, *m_interface)); + else + { + solAssert(_varDecl.isStateVariable(), ""); + m_stateVariables.emplace(&_varDecl, SSAVariable(_varDecl, *m_interface)); + } return true; } else |