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

---
 test/libsolidity/SMTChecker.cpp | 26 ++++++++++++++++++++++++++
 1 file changed, 26 insertions(+)

(limited to 'test/libsolidity/SMTChecker.cpp')

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