Merge remote-tracking branch 'origin/develop' into breaking

libsolidity/formal/BMC.cpp

@@ -58,13 +58,18 @@ void BMC::analyze(SourceUnit const& _source, map<ASTNode const*, set<Verificatio
 {
 	solAssert(_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker), "");
 
-	m_solvedTargets = move(_solvedTargets);
-	m_context.setSolver(m_interface.get());
-	m_context.clear();
-	m_context.setAssertionAccumulation(true);
-	m_variableUsage.setFunctionInlining(shouldInlineFunctionCall);
+	/// This is currently used to abort analysis of SourceUnits
+	/// containing file level functions or constants.
+	if (SMTEncoder::analyze(_source))
+	{
+		m_solvedTargets = move(_solvedTargets);
+		m_context.setSolver(m_interface.get());
+		m_context.clear();
+		m_context.setAssertionAccumulation(true);
+		m_variableUsage.setFunctionInlining(shouldInlineFunctionCall);
 
-	_source.accept(*this);
+		_source.accept(*this);
+	}
 
 	solAssert(m_interface->solvers() > 0, "");
 	// If this check is true, Z3 and CVC4 are not available

libsolidity/formal/CHC.cpp

@@ -69,18 +69,23 @@ void CHC::analyze(SourceUnit const& _source)
 {
 	solAssert(_source.annotation().experimentalFeatures.count(ExperimentalFeature::SMTChecker), "");
 
-	resetSourceAnalysis();
+	/// This is currently used to abort analysis of SourceUnits
+	/// containing file level functions or constants.
+	if (SMTEncoder::analyze(_source))
+	{
+		resetSourceAnalysis();
 
-	set<SourceUnit const*, EncodingContext::IdCompare> sources;
-	sources.insert(&_source);
-	for (auto const& source: _source.referencedSourceUnits(true))
-		sources.insert(source);
-	for (auto const* source: sources)
-		defineInterfacesAndSummaries(*source);
-	for (auto const* source: sources)
-		source->accept(*this);
+		set<SourceUnit const*, EncodingContext::IdCompare> sources;
+		sources.insert(&_source);
+		for (auto const& source: _source.referencedSourceUnits(true))
+			sources.insert(source);
+		for (auto const* source: sources)
+			defineInterfacesAndSummaries(*source);
+		for (auto const* source: sources)
+			source->accept(*this);
 
-	checkVerificationTargets();
+		checkVerificationTargets();
+	}
 
 	bool ranSolver = true;
 #ifndef HAVE_Z3
@@ -1382,8 +1387,7 @@ void CHC::checkAndReportTarget(
 			m_errorReporter.warning(
 				_errorReporterId,
 				location,
-				"CHC: " + _satMsg,
-				SecondarySourceLocation().append("Counterexample:\n" + *cex, SourceLocation{})
+				"CHC: " + _satMsg + "\nCounterexample:\n" + *cex
 			);
 		else
 			m_errorReporter.warning(

libsolidity/formal/SMTEncoder.cpp

@@ -40,6 +40,38 @@ SMTEncoder::SMTEncoder(smt::EncodingContext& _context):
 {
 }
 
+bool SMTEncoder::analyze(SourceUnit const& _source)
+{
+	set<SourceUnit const*, smt::EncodingContext::IdCompare> sources;
+	sources.insert(&_source);
+	for (auto const& source: _source.referencedSourceUnits(true))
+		sources.insert(source);
+
+	bool analysis = true;
+	for (auto source: sources)
+		for (auto node: source->nodes())
+			if (auto function = dynamic_pointer_cast<FunctionDefinition>(node))
+			{
+				m_errorReporter.warning(
+					6660_error,
+					function->location(),
+					"Model checker analysis was not possible because file level functions are not supported."
+				);
+				analysis = false;
+			}
+			else if (auto var = dynamic_pointer_cast<VariableDeclaration>(node))
+			{
+				m_errorReporter.warning(
+					8195_error,
+					var->location(),
+					"Model checker analysis was not possible because file level constants are not supported."
+				);
+				analysis = false;
+			}
+
+	return analysis;
+}
+
 bool SMTEncoder::visit(ContractDefinition const& _contract)
 {
 	solAssert(m_currentContract, "");

libsolidity/formal/SMTEncoder.h

@@ -52,6 +52,9 @@ class SMTEncoder: public ASTConstVisitor
 public:
 	SMTEncoder(smt::EncodingContext& _context);
 
+	/// @returns true if engine should proceed with analysis.
+	bool analyze(SourceUnit const& _sources);
+
 	/// @returns the leftmost identifier in a multi-d IndexAccess.
 	static Expression const* leftmostBase(IndexAccess const& _indexAccess);