SMT should not crash on typecast/structs

2 files changed, 36 insertions, 0 deletions

diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index fd78e578..7c8c089e 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();
diff --git a/test/libsolidity/SMTChecker.cpp b/test/libsolidity/SMTChecker.cpp
index d58f296f..8d712a80 100644
--- a/test/libsolidity/SMTChecker.cpp
+++ b/test/libsolidity/SMTChecker.cpp
@@ -79,6 +79,32 @@ BOOST_AUTO_TEST_CASE(simple_overflow)
 	CHECK_WARNING(text, "Overflow (resulting value larger than");
 }
 
+BOOST_AUTO_TEST_CASE(warn_on_typecast)
+{
+	string text = R"(
+		contract C {
+			function f() public pure returns (uint) {
+				return uint8(1);
+			}
+		}
+	)";
+	CHECK_WARNING(text, "Assertion checker does not yet implement this expression.");
+}
+
+BOOST_AUTO_TEST_CASE(warn_on_struct)
+{
+	string text = R"(
+		contract C {
+			struct A { uint a; uint b; }
+			function f() public pure returns (A) {
+				return A({ a: 1, b: 2 });
+			}
+		}
+	)";
+	/// Multiple warnings, should check for: Assertion checker does not yet implement this expression.
+	CHECK_WARNING_ALLOW_MULTI(text, "");
+}
+
 BOOST_AUTO_TEST_SUITE_END()
 
 }