diff options
Diffstat (limited to 'libsolidity/formal')
| -rw-r--r-- | libsolidity/formal/SMTChecker.cpp | 18 | ||||
| -rw-r--r-- | libsolidity/formal/SMTChecker.h | 2 |
2 files changed, 10 insertions, 10 deletions
diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp index 777e57c3..c4dee22d 100644 --- a/libsolidity/formal/SMTChecker.cpp +++ b/libsolidity/formal/SMTChecker.cpp @@ -77,7 +77,7 @@ bool SMTChecker::visit(FunctionDefinition const& _function) m_interface->reset(); m_variables.clear(); m_pathConditions.clear(); - m_conditionalExecutionHappened = false; + m_loopExecutionHappened = false; initializeLocalVariables(_function); return true; } @@ -132,6 +132,7 @@ bool SMTChecker::visit(WhileStatement const& _node) visitBranch(_node.body(), expr(_node.condition())); } + m_loopExecutionHappened = true; resetVariables(touchedVariables); return false; @@ -171,7 +172,7 @@ bool SMTChecker::visit(ForStatement const& _node) m_interface->pop(); - m_conditionalExecutionHappened = true; + m_loopExecutionHappened = true; std::swap(sequenceCountersStart, m_variables); resetVariables(touchedVariables); @@ -548,7 +549,6 @@ SMTChecker::VariableSequenceCounters SMTChecker::visitBranch(Statement const& _s if (_condition) popPathCondition(); - m_conditionalExecutionHappened = true; std::swap(m_variables, beforeVars); return beforeVars; @@ -591,10 +591,10 @@ void SMTChecker::checkCondition( vector<string> values; tie(result, values) = checkSatisfiableAndGenerateModel(expressionsToEvaluate); - string conditionalComment; - if (m_conditionalExecutionHappened) - conditionalComment = - "\nNote that some information is erased after conditional execution of parts of the code.\n" + string loopComment; + if (m_loopExecutionHappened) + loopComment = + "\nNote that some information is erased after the execution of loops.\n" "You can re-introduce information using require()."; switch (result) { @@ -611,13 +611,13 @@ void SMTChecker::checkCondition( } else message << "."; - m_errorReporter.warning(_location, message.str() + conditionalComment); + m_errorReporter.warning(_location, message.str() + loopComment); break; } case smt::CheckResult::UNSATISFIABLE: break; case smt::CheckResult::UNKNOWN: - m_errorReporter.warning(_location, _description + " might happen here." + conditionalComment); + m_errorReporter.warning(_location, _description + " might happen here." + loopComment); break; case smt::CheckResult::ERROR: m_errorReporter.warning(_location, "Error trying to invoke SMT solver."); diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index 7e7996cf..fd54fb5c 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -160,7 +160,7 @@ 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::vector<smt::Expression> m_pathConditions; |