[SMTChecker] Inline calls to internal functions

test/libsolidity/SMTChecker.cpp

@@ -137,16 +137,17 @@ BOOST_AUTO_TEST_CASE(function_call_does_not_clear_local_vars)
 {
 	string text = R"(
 		contract C {
-			function f() public {
+			function g() public pure {}
+			function f() public view {
 				uint a = 3;
-				this.f();
+				this.g();
 				assert(a == 3);
-				f();
+				g();
 				assert(a == 3);
 			}
 		}
 	)";
-	CHECK_SUCCESS_NO_WARNINGS(text);
+	CHECK_WARNING(text, "Assertion checker does not yet implement this type of function call");
 }
 
 BOOST_AUTO_TEST_CASE(branches_merge_variables)
@@ -569,7 +570,10 @@ BOOST_AUTO_TEST_CASE(constant_condition)
 			}
 		}
 	)";
-	CHECK_WARNING(text, "Condition is always true");
+	CHECK_WARNING_ALLOW_MULTI(text, (vector<string>{
+		"Condition is always true",
+		"Assertion checker does not yet implement this type of function call"
+	}));
 	text = R"(
 		contract C {
 			function f(uint x) public pure {
@@ -577,7 +581,10 @@ BOOST_AUTO_TEST_CASE(constant_condition)
 			}
 		}
 	)";
-	CHECK_WARNING(text, "Condition is always false");
+	CHECK_WARNING_ALLOW_MULTI(text, (vector<string>{
+		"Condition is always false",
+		"Assertion checker does not yet implement this type of function call"
+	}));
 	// a plain literal constant is fine
 	text = R"(
 		contract C {
@@ -586,7 +593,7 @@ BOOST_AUTO_TEST_CASE(constant_condition)
 			}
 		}
 	)";
-	CHECK_SUCCESS_NO_WARNINGS(text);
+	CHECK_WARNING(text, "Assertion checker does not yet implement this type of function call");
 }
 
 

test/libsolidity/smtCheckerTests/functions/functions_identity_1.sol

@@ -0,0 +1,13 @@
+pragma experimental SMTChecker;
+contract C
+{
+	function h(uint x) public pure returns (uint) {
+		return x;
+	}
+	function g() public pure {
+		uint x;
+		x = h(42);
+		assert(x > 0);
+	}
+}
+

test/libsolidity/smtCheckerTests/functions/functions_identity_1_fail.sol

@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+contract C
+{
+	function h(uint x) public pure returns (uint) {
+		return x;
+	}
+	function g() public pure {
+		uint x;
+		x = h(0);
+		assert(x > 0);
+	}
+}
+
+// ----
+// Warning: (161-174): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/functions_identity_2.sol

@@ -0,0 +1,17 @@
+pragma experimental SMTChecker;
+contract C
+{
+	function h(uint x) public pure returns (uint) {
+		return k(x);
+	}
+
+	function k(uint x) public pure returns (uint) {
+		return x;
+	}
+	function g() public pure {
+		uint x;
+		x = h(2);
+		assert(x > 0);
+	}
+}
+

test/libsolidity/smtCheckerTests/functions/functions_identity_2_fail.sol

@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+contract C
+{
+	function h(uint x) public pure returns (uint) {
+		return k(x);
+	}
+
+	function k(uint x) public pure returns (uint) {
+		return x;
+	}
+	function g() public pure {
+		uint x;
+		x = h(0);
+		assert(x > 0);
+	}
+}
+
+// ----
+// Warning: (229-242): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple.sol

@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+contract C
+{
+	function h(uint x) public pure returns (uint) {
+		return x;
+	}
+	function g() public pure {
+		uint x;
+		x = (h)(42);
+		assert(x > 0);
+	}
+}
+
+// ----

test/libsolidity/smtCheckerTests/functions/functions_identity_as_tuple_fail.sol

@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+contract C
+{
+	function h(uint x) public pure returns (uint) {
+		return x;
+	}
+	function g() public pure {
+		uint x;
+		x = (h)(0);
+		assert(x > 0);
+	}
+}
+
+// ----
+// Warning: (163-176): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/functions_recursive.sol

@@ -0,0 +1,17 @@
+pragma experimental SMTChecker;
+contract C
+{
+	uint a;
+	function g() public {
+		if (a > 0)
+		{
+			a = a - 1;
+			g();
+		}
+		else
+			assert(a == 0);
+	}
+}
+
+// ----
+// Warning: (111-114): Assertion checker does not support recursive function calls.

test/libsolidity/smtCheckerTests/functions/functions_recursive_indirect.sol

@@ -0,0 +1,26 @@
+pragma experimental SMTChecker;
+contract C
+{
+	uint a;
+	function f() public {
+		if (a > 0)
+		{
+			a = a - 1;
+			g();
+		}
+		else
+			assert(a == 0);
+	}
+	function g() public {
+		if (a > 0)
+		{
+			a = a - 1;
+			f();
+		}
+		else
+			assert(a == 0);
+	}
+}
+// ----
+// Warning: (206-209): Assertion checker does not support recursive function calls.
+// Warning: (111-114): Assertion checker does not support recursive function calls.

test/libsolidity/smtCheckerTests/functions/functions_storage_var_1.sol

@@ -0,0 +1,14 @@
+pragma experimental SMTChecker;
+contract C
+{
+	uint a;
+	function f(uint x) public {
+		uint y;
+		a = (y = x);
+	}
+	function g() public {
+		f(1);
+		assert(a > 0);
+	}
+}
+

test/libsolidity/smtCheckerTests/functions/functions_storage_var_1_fail.sol

@@ -0,0 +1,16 @@
+pragma experimental SMTChecker;
+contract C
+{
+	uint a;
+	function f(uint x) public {
+		uint y;
+		a = (y = x);
+	}
+	function g() public {
+		f(0);
+		assert(a > 0);
+	}
+}
+
+// ----
+// Warning: (144-157): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/functions_storage_var_2.sol

@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+contract C
+{
+	uint a;
+	function f(uint x) public {
+		uint y;
+		a = (y = x);
+	}
+	function g() public {
+		f(1);
+		f(42);
+		assert(a > 1);
+	}
+}
+

test/libsolidity/smtCheckerTests/functions/functions_storage_var_2_fail.sol

@@ -0,0 +1,17 @@
+pragma experimental SMTChecker;
+contract C
+{
+	uint a;
+	function f(uint x) public {
+		uint y;
+		a = (y = x);
+	}
+	function g() public {
+		f(1);
+		f(0);
+		assert(a > 0);
+	}
+}
+
+// ----
+// Warning: (152-165): Assertion violation happens here

test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_for.sol

@@ -0,0 +1,8 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(bool x) public pure { require(x); for (;x;) {} }
+}
+// ----
+// Warning: (98-99): For loop condition is always true.

test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_for_only_call.sol

@@ -0,0 +1,7 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(bool x) public pure { for (;x;) {} }
+	function g() public pure { f(true); }
+}

test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_if.sol

@@ -0,0 +1,7 @@
+pragma experimental SMTChecker;
+contract C
+{
+	function f(bool x) public pure { require(x); if (x) {} }
+}
+// ----
+// Warning: (95-96): Condition is always true.

test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_require.sol

@@ -0,0 +1,8 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(bool x) public pure { x = true; require(x); }
+}
+// ----
+// Warning: (98-99): Condition is always true.

test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_require_only_call.sol

@@ -0,0 +1,7 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(bool x) public pure { require(x); }
+	function g() public pure { f(true); }
+}

test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_while.sol

@@ -0,0 +1,8 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(bool x) public pure { require(x); while (x) {} }
+}
+// ----
+// Warning: (99-100): While loop condition is always true.

test/libsolidity/smtCheckerTests/functions/functions_trivial_condition_while_only_call.sol

@@ -0,0 +1,7 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	function f(bool x) public pure { while (x) {} }
+	function g() public pure { f(true); }
+}