new free function tests

test/libsolidity/smtCheckerTests/file_level/easy.sol

@@ -0,0 +1,17 @@
+function add(uint a, uint b) pure returns (uint) {
+	return a + b;
+}
+
+contract C {
+	function f(uint x) internal pure returns (uint) {
+		return add(x, 2);
+	}
+	function g() public pure {
+		assert(f(7) == 9); // should hold
+		assert(f(8) == 9); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (222-239): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g()\n    C.f(7) -- internal call\n        add(7, 2) -- internal call\n    C.f(8) -- internal call\n        add(8, 2) -- internal call

test/libsolidity/smtCheckerTests/file_level/enum.sol

@@ -0,0 +1,23 @@
+enum E {
+	READ,
+	WRITE
+}
+
+function allocate(bool b) pure returns (E) {
+	if (b) return E.READ;
+	return E.WRITE;
+}
+
+contract C {
+	function f() public pure {
+		E e1 = allocate(true);
+		assert(e1 == E.READ); // should hold
+		E e2 = allocate(false);
+		assert(e2 == E.READ); // should fail
+		assert(allocate(false) == E.WRITE); // should hold
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (247-267): CHC: Assertion violation happens here.\nCounterexample:\n\ne1 = 0\ne2 = 1\n\nTransaction trace:\nC.constructor()\nC.f()\n    allocate(true) -- internal call\n    allocate(false) -- internal call

test/libsolidity/smtCheckerTests/file_level/free_function_1.sol

@@ -11,5 +11,5 @@ function fun(uint[] calldata _x, uint[] storage _y) view  returns (uint, uint[]
 // ====
 // SMTEngine: all
 // ----
-// Warning 4984: (168-180): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\ndata = []\nx = 1\n = 0\n = 0\na = 0\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.f(1, input)\n    fun(_x, []) -- internal call
+// Warning 4984: (168-180): CHC: Overflow (resulting value larger than 2**256 - 1) happens here.\nCounterexample:\ndata = []\nx = 1\n = 0\n = 0\na = 0\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.f(1, input)\n    ::fun(_x, []) -- internal call
-// Warning 6368: (289-294): CHC: Out of bounds access happens here.\nCounterexample:\ndata = []\nx = 0\ninput = [5, 5, 5, 5, 5, 5, 5, 5, 5, 10, 5, 5, 13, 5, 5, 5, 5, 5, 19, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5]\n = 0\n = 0\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.f(0, [5, 5, 5, 5, 5, 5, 5, 5, 5, 10, 5, 5, 13, 5, 5, 5, 5, 5, 19, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5])\n    fun([5, 5, 5, 5, 5, 5, 5, 5, 5, 10, 5, 5, 13, 5, 5, 5, 5, 5, 19, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5], []) -- internal call
+// Warning 6368: (289-294): CHC: Out of bounds access happens here.\nCounterexample:\ndata = []\nx = 0\ninput = [5, 5, 5, 5, 5, 5, 5, 5, 5, 10, 5, 5, 13, 5, 5, 5, 5, 5, 19, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5]\n = 0\n = 0\n\nTransaction trace:\nC.constructor()\nState: data = []\nC.f(0, [5, 5, 5, 5, 5, 5, 5, 5, 5, 10, 5, 5, 13, 5, 5, 5, 5, 5, 19, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5])\n    ::fun([5, 5, 5, 5, 5, 5, 5, 5, 5, 10, 5, 5, 13, 5, 5, 5, 5, 5, 19, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5, 5], []) -- internal call

test/libsolidity/smtCheckerTests/file_level/free_function_4.sol

@@ -4,4 +4,4 @@ function f()pure {
 // ====
 // SMTEngine: all
 // ----
-// Warning 2072: (52-60): Unused local variable.
+// Warning 2072: (20-28): Unused local variable.

test/libsolidity/smtCheckerTests/file_level/free_function_5.sol

@@ -5,4 +5,4 @@ function f() pure {
 // ====
 // SMTEngine: all
 // ----
-// Warning 6133: (67-83): Statement has no effect.
+// Warning 6133: (35-51): Statement has no effect.

test/libsolidity/smtCheckerTests/file_level/free_namesake_contract_function.sol

@@ -0,0 +1,14 @@
+function f() pure returns (uint) { return 1337; }
+
+contract C {
+	function g() public pure {
+		assert(f() == 42); // should hold
+		assert(f() == 1337); // should fail
+	}
+	function f() internal pure returns (uint) { return 42; }
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 2519: (170-226): This declaration shadows an existing declaration.
+// Warning 6328: (130-149): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nC.constructor()\nC.g()\n    C.f() -- internal call\n    C.f() -- internal call

test/libsolidity/smtCheckerTests/file_level/free_runtimecode.sol

@@ -0,0 +1,20 @@
+contract C {
+	uint public x = 2;
+}
+
+function test() pure returns (bool) {
+	return type(C).runtimeCode.length > 20;
+}
+
+contract D {
+	function f() public pure {
+		assert(test()); // should hold but SMTChecker doesn't know that
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 7507: (82-101): Assertion checker does not yet support this expression.
+// Warning 7507: (82-101): Assertion checker does not yet support this expression.
+// Warning 6328: (161-175): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nD.constructor()\nD.f()\n    test() -- internal call
+// Warning 7507: (82-101): Assertion checker does not yet support this expression.

test/libsolidity/smtCheckerTests/file_level/import.sol

@@ -0,0 +1,28 @@
+==== Source: A ====
+struct S { uint x; }
+function set(S storage a, uint v) { a.x = v; }
+
+==== Source: B ====
+import "A";
+import "A" as A;
+contract C {
+	A.S data;
+	function f(uint v) internal returns (uint one, uint two) {
+		A.set(data, v);
+		one = data.x;
+		set(data, v + 1);
+		two = data.x;
+	}
+	function g() public {
+		(uint x, uint y) = f(7);
+		assert(x == 7); // should hold but the SMTChecker doesn't know that
+		assert(y == 8); // should hold but the SMTChecker doesn't know that
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 8364: (B:115-116): Assertion checker does not yet implement type module "A"
+// Warning 6328: (B:238-252): CHC: Assertion violation happens here.\nCounterexample:\ndata = {x: 0}\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor()\nState: data = {x: 0}\nC.g()\n    C.f(7) -- internal call\n        A:set({x: 0}, 7) -- internal call\n        A:set({x: 0}, 8) -- internal call
+// Warning 6328: (B:308-322): CHC: Assertion violation happens here.\nCounterexample:\ndata = {x: 0}\nx = 0\ny = 0\n\nTransaction trace:\nC.constructor()\nState: data = {x: 0}\nC.g()\n    C.f(7) -- internal call\n        A:set({x: 0}, 7) -- internal call\n        A:set({x: 0}, 8) -- internal call
+// Warning 8364: (B:115-116): Assertion checker does not yet implement type module "A"

test/libsolidity/smtCheckerTests/file_level/libraries_from_free.sol

@@ -0,0 +1,28 @@
+library L {
+	function pub() public pure returns (uint) {
+		return 7;
+	}
+	function inter() internal pure returns (uint) {
+		return 8;
+	}
+}
+
+function fu() pure returns (uint, uint) {
+	return (L.pub(), L.inter());
+}
+
+contract C {
+	function f() public pure {
+		(uint x, uint y) = fu();
+		assert(x == 7); // should hold but SMTChecker doesn't implement delegatecall
+		assert(y == 9); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 4588: (190-197): Assertion checker does not yet implement this type of function call.
+// Warning 4588: (190-197): Assertion checker does not yet implement this type of function call.
+// Warning 6328: (284-298): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 8\ny = 8\n\nTransaction trace:\nC.constructor()\nC.f()\n    fu() -- internal call\n        L.inter() -- internal call
+// Warning 6328: (363-377): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 0\ny = 8\n\nTransaction trace:\nC.constructor()\nC.f()\n    fu() -- internal call\n        L.inter() -- internal call
+// Warning 4588: (190-197): Assertion checker does not yet implement this type of function call.

test/libsolidity/smtCheckerTests/file_level/new_operator.sol

@@ -0,0 +1,20 @@
+contract C {
+	uint public x = 2;
+}
+
+function test() returns (uint) {
+	return (new C()).x();
+}
+
+contract D {
+	function f() public {
+		assert(test() == 2); // should hold but the SMTChecker doesn't support `new`
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 4588: (78-85): Assertion checker does not yet implement this type of function call.
+// Warning 4588: (78-85): Assertion checker does not yet implement this type of function call.
+// Warning 6328: (133-152): CHC: Assertion violation happens here.\nCounterexample:\n\n\nTransaction trace:\nD.constructor()\nD.f()\n    test() -- internal call
+// Warning 4588: (78-85): Assertion checker does not yet implement this type of function call.

test/libsolidity/smtCheckerTests/file_level/overloads.sol

@@ -0,0 +1,18 @@
+function f(uint) pure returns (uint) {
+	return 2;
+}
+function f(string memory) pure returns (uint) {
+	return 3;
+}
+
+contract C {
+	function g() public pure {
+		(uint x, uint y) = (f(2), f("abc"));
+		assert(x == 2); // should hold
+		assert(y == 4); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (229-243): CHC: Assertion violation happens here.\nCounterexample:\n\nx = 2\ny = 3\n\nTransaction trace:\nC.constructor()\nC.g()\n    f(2) -- internal call\n    f([97, 98, 99]) -- internal call

test/libsolidity/smtCheckerTests/file_level/recursion.sol

@@ -0,0 +1,39 @@
+function exp(uint base, uint exponent) pure returns (uint power) {
+	if (exponent == 0)
+		return 1;
+	power = exp(base, exponent / 2);
+	power *= power;
+	if (exponent & 1 == 1)
+		power *= base;
+}
+
+contract C {
+	function g(uint base, uint exponent) internal pure returns (uint) {
+		return exp(base, exponent);
+	}
+	function f() public pure {
+		// All of these should hold but the SMTChecker can't prove them.
+		assert(g(0, 0) == 1);
+		assert(g(0, 1) == 0);
+		assert(g(1, 0) == 1);
+		assert(g(2, 3) == 8);
+		assert(g(3, 10) == 59049);
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 4281: (118-130): CHC: Division by zero might happen here.
+// Warning 4984: (134-148): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
+// Warning 4984: (176-189): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
+// Warning 6328: (430-450): CHC: Assertion violation happens here.
+// Warning 6328: (478-498): CHC: Assertion violation might happen here.
+// Warning 6328: (502-527): CHC: Assertion violation might happen here.
+// Warning 2661: (134-148): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 2661: (176-189): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 2661: (134-148): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 2661: (134-148): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 8065: (176-189): BMC: Overflow (resulting value larger than 2**256 - 1) might happen here.
+// Warning 4661: (478-498): BMC: Assertion violation happens here.
+// Warning 2661: (134-148): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.
+// Warning 4661: (502-527): BMC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/file_level/struct.sol

@@ -0,0 +1,27 @@
+struct S {
+	uint x;
+	uint[] a;
+}
+
+function allocate(uint _x, uint _f) pure returns (S memory) {
+	S memory s;
+	s.x = _x;
+	s.a = new uint[](1);
+	s.a[0] = _f;
+	return s;
+}
+
+contract C {
+	function f() public pure {
+		S memory s = allocate(2, 1);
+		assert(s.x == 2); // should hold
+		assert(s.a[0] == 1); // should hold
+		assert(s.x == 3); // should fail
+		assert(s.a[0] == 4); // should fail
+	}
+}
+// ====
+// SMTEngine: all
+// ----
+// Warning 6328: (317-333): CHC: Assertion violation happens here.\nCounterexample:\n\ns = {x: 2, a: [1]}\n\nTransaction trace:\nC.constructor()\nC.f()\n    allocate(2, 1) -- internal call
+// Warning 6328: (352-371): CHC: Assertion violation happens here.\nCounterexample:\n\ns = {x: 2, a: [1]}\n\nTransaction trace:\nC.constructor()\nC.f()\n    allocate(2, 1) -- internal call