Merge pull request #3099 from ethereum/develop

Merge develop into release for 0.4.18.

1 files changed, 19 insertions, 9 deletions

diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index fd78e578..2d2f05ec 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -234,6 +234,16 @@ void SMTChecker::endVisit(BinaryOperation const& _op)
 
 void SMTChecker::endVisit(FunctionCall const& _funCall)
 {
+	solAssert(_funCall.annotation().kind != FunctionCallKind::Unset, "");
+	if (_funCall.annotation().kind != FunctionCallKind::FunctionCall)
+	{
+		m_errorReporter.warning(
+			_funCall.location(),
+			"Assertion checker does not yet implement this expression."
+		);
+		return;
+	}
+
 	FunctionType const& funType = dynamic_cast<FunctionType const&>(*_funCall.expression().annotation().type);
 
 	std::vector<ASTPointer<Expression const>> const args = _funCall.arguments();
@@ -484,10 +494,10 @@ void SMTChecker::createVariable(VariableDeclaration const& _varDecl, bool _setTo
 	{
 		solAssert(m_currentSequenceCounter.count(&_varDecl) == 0, "");
 		solAssert(m_nextFreeSequenceCounter.count(&_varDecl) == 0, "");
-		solAssert(m_Variables.count(&_varDecl) == 0, "");
+		solAssert(m_variables.count(&_varDecl) == 0, "");
 		m_currentSequenceCounter[&_varDecl] = 0;
 		m_nextFreeSequenceCounter[&_varDecl] = 1;
-		m_Variables.emplace(&_varDecl, m_interface->newFunction(uniqueSymbol(_varDecl), smt::Sort::Int, smt::Sort::Int));
+		m_variables.emplace(&_varDecl, m_interface->newFunction(uniqueSymbol(_varDecl), smt::Sort::Int, smt::Sort::Int));
 		setValue(_varDecl, _setToZero);
 	}
 	else
@@ -556,7 +566,7 @@ smt::Expression SMTChecker::maxValue(IntegerType const& _t)
 
 smt::Expression SMTChecker::expr(Expression const& _e)
 {
-	if (!m_Expressions.count(&_e))
+	if (!m_expressions.count(&_e))
 	{
 		solAssert(_e.annotation().type, "");
 		switch (_e.annotation().type->category())
@@ -565,24 +575,24 @@ smt::Expression SMTChecker::expr(Expression const& _e)
 		{
 			if (RationalNumberType const* rational = dynamic_cast<RationalNumberType const*>(_e.annotation().type.get()))
 				solAssert(!rational->isFractional(), "");
-			m_Expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e)));
+			m_expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e)));
 			break;
 		}
 		case Type::Category::Integer:
-			m_Expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e)));
+			m_expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e)));
 			break;
 		case Type::Category::Bool:
-			m_Expressions.emplace(&_e, m_interface->newBool(uniqueSymbol(_e)));
+			m_expressions.emplace(&_e, m_interface->newBool(uniqueSymbol(_e)));
 			break;
 		default:
 			solAssert(false, "Type not implemented.");
 		}
 	}
-	return m_Expressions.at(&_e);
+	return m_expressions.at(&_e);
 }
 
 smt::Expression SMTChecker::var(Declaration const& _decl)
 {
-	solAssert(m_Variables.count(&_decl), "");
-	return m_Variables.at(&_decl);
+	solAssert(m_variables.count(&_decl), "");
+	return m_variables.at(&_decl);
 }