Merge pull request ethereum#3943 from ethereum/smt_remove_branch_warning

[SMTChecker] Remove 'information is erase' message for if-else
sledrho · Apr 20, 2018 · 6767327 · 6767327
2 parents 0f32843 + ba3d16f
commit 6767327
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 10 deletions.
diff --git 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
@@ -160,7 +160,7 @@ class SMTChecker: private ASTConstVisitor
 
 	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;