From 6ae82fcec2cbae20f2f8481ce5f2c2dd28df972e Mon Sep 17 00:00:00 2001
From: Leonardo Alt <leo@ethereum.org>
Date: Wed, 7 Apr 2021 17:16:31 +0200
Subject: [PATCH] Add tests for the library bug

---
 .../internal_library_external_call_1.sol      | 26 +++++++++++++++
 .../internal_library_external_call_2.sol      | 29 +++++++++++++++++
 .../internal_library_external_call_3.sol      | 32 +++++++++++++++++++
 3 files changed, 87 insertions(+)
 create mode 100644 test/libsolidity/smtCheckerTests/external_calls/internal_library_external_call_1.sol
 create mode 100644 test/libsolidity/smtCheckerTests/external_calls/internal_library_external_call_2.sol
 create mode 100644 test/libsolidity/smtCheckerTests/external_calls/internal_library_external_call_3.sol

diff --git a/test/libsolidity/smtCheckerTests/external_calls/internal_library_external_call_1.sol b/test/libsolidity/smtCheckerTests/external_calls/internal_library_external_call_1.sol
new file mode 100644
index 000000000..37af9be9c
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/external_calls/internal_library_external_call_1.sol
@@ -0,0 +1,26 @@
+interface I {
+    function i() external;
+}
+
+library L {
+    function f(I _i) internal {
+        _i.i();
+    }
+}
+
+contract C {
+    uint x;
+    bool inG;
+    function s() public {
+        require(inG);
+        x = 2;
+    }
+    function g(I _i) public {
+        inG = true;
+        L.f(_i);
+        assert(x == 0);
+        inG = false;
+    }
+}
+// ----
+// Warning 6328: (296-310): CHC: Assertion violation happens here.\nCounterexample:\nx = 2, inG = true\n_i = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, inG = false\nC.g(0)\n    L.f(0) -- internal call\n        _i.i() -- untrusted external call, synthesized as:\n            C.s() -- reentrant call
diff --git a/test/libsolidity/smtCheckerTests/external_calls/internal_library_external_call_2.sol b/test/libsolidity/smtCheckerTests/external_calls/internal_library_external_call_2.sol
new file mode 100644
index 000000000..eb4513d7f
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/external_calls/internal_library_external_call_2.sol
@@ -0,0 +1,29 @@
+interface I {
+    function i() external;
+}
+
+library L {
+    function f(I _i) internal {
+        _i.i();
+    }
+	function g(I _i) internal {
+		f(_i);
+	}
+}
+
+contract C {
+    uint x;
+    bool inG;
+    function s() public {
+        require(inG);
+        x = 2;
+    }
+    function g(I _i) public {
+        inG = true;
+        L.g(_i);
+        assert(x == 0);
+        inG = false;
+    }
+}
+// ----
+// Warning 6328: (337-351): CHC: Assertion violation happens here.\nCounterexample:\nx = 2, inG = true\n_i = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, inG = false\nC.g(0)\n    L.g(0) -- internal call\n        L.f(0) -- internal call\n            _i.i() -- untrusted external call, synthesized as:\n                C.s() -- reentrant call
diff --git a/test/libsolidity/smtCheckerTests/external_calls/internal_library_external_call_3.sol b/test/libsolidity/smtCheckerTests/external_calls/internal_library_external_call_3.sol
new file mode 100644
index 000000000..495c9dcc9
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/external_calls/internal_library_external_call_3.sol
@@ -0,0 +1,32 @@
+interface I {
+    function i() external;
+}
+
+library M {
+    function f(I _i) internal {
+        _i.i();
+    }
+}
+
+library L {
+	function g(I _i) internal {
+		M.f(_i);
+	}
+}
+
+contract C {
+    uint x;
+    bool inG;
+    function s() public {
+        require(inG);
+        x = 2;
+    }
+    function g(I _i) public {
+        inG = true;
+        L.g(_i);
+        assert(x == 0);
+        inG = false;
+    }
+}
+// ----
+// Warning 6328: (354-368): CHC: Assertion violation happens here.\nCounterexample:\nx = 2, inG = true\n_i = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, inG = false\nC.g(0)\n    L.g(0) -- internal call\n        M.f(0) -- internal call\n            _i.i() -- untrusted external call, synthesized as:\n                C.s() -- reentrant call