[SMTChecker] Clear state knowledge after external function calls

4 files changed, 64 insertions, 1 deletions

diff --git a/test/libsolidity/smtCheckerTests/functions/function_call_does_not_clear_local_vars.sol b/test/libsolidity/smtCheckerTests/functions/function_call_does_not_clear_local_vars.sol
index b4260224..0ceb3b46 100644
--- a/test/libsolidity/smtCheckerTests/functions/function_call_does_not_clear_local_vars.sol
+++ b/test/libsolidity/smtCheckerTests/functions/function_call_does_not_clear_local_vars.sol
@@ -9,5 +9,4 @@ contract C {
     }
 }
 // ----
-// Warning: (99-107): Assertion checker does not yet implement this type of function call.
 // Warning: (141-144): Assertion checker does not support recursive function calls.
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_external_1.sol b/test/libsolidity/smtCheckerTests/functions/functions_external_1.sol
new file mode 100644
index 00000000..16482e7a
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_external_1.sol
@@ -0,0 +1,21 @@
+pragma experimental SMTChecker;
+
+contract D
+{
+	function g(uint x) public;
+}
+
+contract C
+{
+	uint x;
+	function f(uint y, D d) public {
+		require(x == y);
+		assert(x == y);
+		d.g(y);
+		// Storage knowledge is cleared after an external call.
+		assert(x == y);
+	}
+}
+// ----
+// Warning: (119-122): Assertion checker does not yet support the type of this variable.
+// Warning: (240-254): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_external_2.sol b/test/libsolidity/smtCheckerTests/functions/functions_external_2.sol
new file mode 100644
index 00000000..1e704c9d
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_external_2.sol
@@ -0,0 +1,21 @@
+pragma experimental SMTChecker;
+
+contract D
+{
+	function g(uint x) public;
+}
+
+contract C
+{
+	mapping (uint => uint) map;
+	function f(uint y, D d) public {
+		require(map[0] == map[1]);
+		assert(map[0] == map[1]);
+		d.g(y);
+		// Storage knowledge is cleared after an external call.
+		assert(map[0] == map[1]);
+	}
+}
+// ----
+// Warning: (139-142): Assertion checker does not yet support the type of this variable.
+// Warning: (280-304): Assertion violation happens here
diff --git a/test/libsolidity/smtCheckerTests/functions/functions_external_3.sol b/test/libsolidity/smtCheckerTests/functions/functions_external_3.sol
new file mode 100644
index 00000000..dd36ec73
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/functions/functions_external_3.sol
@@ -0,0 +1,22 @@
+pragma experimental SMTChecker;
+
+contract D
+{
+	function g(uint x) public;
+}
+
+contract C
+{
+	mapping (uint => uint) storageMap;
+	function f(uint y, D d) public {
+		mapping (uint => uint) storage map = storageMap;
+		require(map[0] == map[1]);
+		assert(map[0] == map[1]);
+		d.g(y);
+		// Storage knowledge is cleared after an external call.
+		assert(map[0] == map[1]);
+	}
+}
+// ----
+// Warning: (146-149): Assertion checker does not yet support the type of this variable.
+// Warning: (338-362): Assertion violation happens here