From 10529e994f9a587436c57bfdeef52476da9770bb Mon Sep 17 00:00:00 2001
From: Alex Beregszaszi <alex@rtfs.hu>
Date: Wed, 4 Oct 2017 12:18:40 +0100
Subject: SMT should not crash on typecast/structs
---
libsolidity/formal/SMTChecker.cpp | 10 ++++++++++
test/libsolidity/SMTChecker.cpp | 26 ++++++++++++++++++++++++++
2 files changed, 36 insertions(+)
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()
}
--
cgit v1.2.3