From 3d7188ac7b64049710149d6ef53efdc6edbcf7d0 Mon Sep 17 00:00:00 2001
From: Martin Blicha <blichm@usi.ch>
Date: Sat, 9 Jan 2021 16:35:46 +0100
Subject: [PATCH] update to the tests

---
 .../try_multiple_catch_clauses_2.sol          | 24 ++++++++++++++++
 ...ry_multiple_returned_values_with_tuple.sol | 28 +++++++++++++++++++
 .../try_catch/try_inside_while.sol            | 13 +++++++++
 .../try_multiple_catch_clauses_2.sol          | 22 +++++++++++++++
 ...ry_multiple_returned_values_with_tuple.sol | 26 +++++++++++++++++
 5 files changed, 113 insertions(+)
 create mode 100644 test/libsolidity/smtCheckerTests/bmc_coverage/try_multiple_catch_clauses_2.sol
 create mode 100644 test/libsolidity/smtCheckerTests/bmc_coverage/try_multiple_returned_values_with_tuple.sol
 create mode 100644 test/libsolidity/smtCheckerTests/try_catch/try_inside_while.sol
 create mode 100644 test/libsolidity/smtCheckerTests/try_catch/try_multiple_catch_clauses_2.sol
 create mode 100644 test/libsolidity/smtCheckerTests/try_catch/try_multiple_returned_values_with_tuple.sol

diff --git a/test/libsolidity/smtCheckerTests/bmc_coverage/try_multiple_catch_clauses_2.sol b/test/libsolidity/smtCheckerTests/bmc_coverage/try_multiple_catch_clauses_2.sol
new file mode 100644
index 000000000..eb6fe4756
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/bmc_coverage/try_multiple_catch_clauses_2.sol
@@ -0,0 +1,24 @@
+pragma experimental SMTChecker;
+contract C {
+
+	function g() public pure {}
+
+	function f() public view {
+		uint x = 0;
+		bool success = false;
+		try this.g() {
+			success = true;
+			x = 1;
+		} catch Error (string memory /*reason*/) {
+			x = 2;
+		} catch (bytes memory /*reason*/) {
+			x = 3;
+		}
+		assert(x > 0 && x < 4); // should hold
+		assert(x == 0); // should fail
+	}
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 4661: (338-352): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/bmc_coverage/try_multiple_returned_values_with_tuple.sol b/test/libsolidity/smtCheckerTests/bmc_coverage/try_multiple_returned_values_with_tuple.sol
new file mode 100644
index 000000000..136d96542
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/bmc_coverage/try_multiple_returned_values_with_tuple.sol
@@ -0,0 +1,28 @@
+pragma experimental SMTChecker;
+contract C {
+
+	struct S {
+		uint x;
+		int y;
+	}
+
+	function g() public pure returns (bool b, S memory s) {
+		b = true;
+		s.x = 42;
+		s.y = -1;
+	}
+
+	function f() public view {
+		bool success = false;
+		try this.g() returns (bool b, S memory s) {
+			success = true;
+			assert(b && s.x == 42 && s.y == -1); // should hold
+		} catch {
+		}
+		assert(success); // fails, not guaranteed that there will be no error
+	}
+}
+// ====
+// SMTEngine: bmc
+// ----
+// Warning 4661: (368-383): BMC: Assertion violation happens here.
diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_inside_while.sol b/test/libsolidity/smtCheckerTests/try_catch/try_inside_while.sol
new file mode 100644
index 000000000..465773b7b
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/try_catch/try_inside_while.sol
@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+contract C {
+	function f() public returns (uint) {
+		while(1==1)
+			try this.f() returns (uint b) {
+				b = 2;
+			} catch {
+			}
+	}
+}
+// ----
+// Warning 6321: (75-79): Unnamed return variable can remain unassigned. Add an explicit return with value to all non-reverting code paths or name the variable.
+// Warning 6838: (91-95): BMC: Condition is always true.
diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_multiple_catch_clauses_2.sol b/test/libsolidity/smtCheckerTests/try_catch/try_multiple_catch_clauses_2.sol
new file mode 100644
index 000000000..6aaabbc4a
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/try_catch/try_multiple_catch_clauses_2.sol
@@ -0,0 +1,22 @@
+pragma experimental SMTChecker;
+contract C {
+
+	function g() public pure {}
+
+	function f() public view {
+		uint x = 0;
+		bool success = false;
+		try this.g() {
+			success = true;
+			x = 1;
+		} catch Error (string memory /*reason*/) {
+			x = 2;
+		} catch (bytes memory /*reason*/) {
+			x = 3;
+		}
+		assert(x > 0 && x < 4); // should hold
+		assert(x == 0); // should fail
+	}
+}
+// ----
+// Warning 6328: (338-352): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nC.constructor()\nC.f()
diff --git a/test/libsolidity/smtCheckerTests/try_catch/try_multiple_returned_values_with_tuple.sol b/test/libsolidity/smtCheckerTests/try_catch/try_multiple_returned_values_with_tuple.sol
new file mode 100644
index 000000000..e1294f417
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/try_catch/try_multiple_returned_values_with_tuple.sol
@@ -0,0 +1,26 @@
+pragma experimental SMTChecker;
+contract C {
+
+	struct S {
+		uint x;
+		int y;
+	}
+
+	function g() public pure returns (bool b, S memory s) {
+		b = true;
+		s.x = 42;
+		s.y = -1;
+	}
+
+	function f() public view {
+		bool success = false;
+		try this.g() returns (bool b, S memory s) {
+			success = true;
+			assert(b && s.x == 42 && s.y == -1);
+		} catch {
+		}
+		assert(success); // fails, not guaranteed that there will be no error
+	}
+}
+// ----
+// Warning 6328: (353-368): CHC: Assertion violation happens here.\nCounterexample:\n\n\n\n\nTransaction trace:\nC.constructor()\nC.f()