Add SMTChecker tests with modules

Leo Alt · Leo Alt · commit 8eb28b10cb28 · 2021-06-01T13:35:10.000+02:00
diff --git a/test/libsolidity/smtCheckerTests/imports/import_as_module_1.sol b/test/libsolidity/smtCheckerTests/imports/import_as_module_1.sol
@@ -0,0 +1,20 @@
+==== Source: A ====
+import "s1.sol" as M;
+contract D is M.C {
+	function f(uint _y) public {
+		g(_y);
+		assert(x == _y); // should hold
+		assert(x > 100); // should fail
+	}
+}
+==== Source: s1.sol ====
+contract C {
+	uint x;
+	function g(uint _x) public {
+		x = _x;
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (A:117-132): CHC: Assertion violation happens here.\nCounterexample:\nx = 0\n_y = 0\n\nTransaction trace:\nD.constructor()\nState: x = 0\nD.f(0)\n    C.g(0) -- internal call
diff --git a/test/libsolidity/smtCheckerTests/imports/import_as_module_2.sol b/test/libsolidity/smtCheckerTests/imports/import_as_module_2.sol
@@ -0,0 +1,26 @@
+==== Source: A ====
+import "s1.sol" as M;
+function f(uint _x) pure {
+	assert(_x > 0);
+}
+contract D {
+	function g(uint _y) public pure {
+		M.f(200); // should hold
+		M.f(_y); // should fail
+		f(10); // should hold
+		f(_y); // should fail
+	}
+}
+==== Source: s1.sol ====
+function f(uint _x) pure {
+	assert(_x > 100);
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 8364: (A:118-119): Assertion checker does not yet implement type module "s1.sol"
+// Warning 8364: (A:145-146): Assertion checker does not yet implement type module "s1.sol"
+// Warning 6328: (A:50-64): CHC: Assertion violation happens here.\nCounterexample:\n\n_y = 0\n\nTransaction trace:\nD.constructor()\nD.g(0)\n    s1.sol:f(200) -- internal call\n    s1.sol:f(0) -- internal call\n    A:f(10) -- internal call\n    A:f(0) -- internal call
+// Warning 6328: (s1.sol:28-44): CHC: Assertion violation happens here.\nCounterexample:\n\n_y = 0\n\nTransaction trace:\nD.constructor()\nD.g(0)\n    s1.sol:f(200) -- internal call\n    s1.sol:f(0) -- internal call
+// Warning 8364: (A:118-119): Assertion checker does not yet implement type module "s1.sol"
+// Warning 8364: (A:145-146): Assertion checker does not yet implement type module "s1.sol"
