tests

test/libsolidity/smtCheckerTests/natspec/abstract_function_nondet_1.sol

@@ -0,0 +1,17 @@
+contract C {
+	/// @custom:smtchecker abstract-function-nondet
+	function f(uint x) internal pure returns (uint) {
+		return x;
+	}
+	function g(uint y) public pure {
+		uint z = f(y);
+		// Generally holds, but here it doesn't because function
+		// `f` has been abstracted by nondeterministic values.
+		assert(z == y);
+	}
+}
+// ====
+// SMTEngine: chc
+// SMTIgnoreCex: yes
+// ----
+// Warning 6328: (297-311): CHC: Assertion violation happens here.

test/libsolidity/smtCheckerTests/natspec/abstract_function_nondet_pow_no_abstraction.sol

@@ -0,0 +1,43 @@
+contract C {
+	function e(uint _e) public pure {
+		// Without abstracting function `pow` the solver
+		// fails to prove that `++i` does not overflow.
+		for (uint i = 0; i < _e; ++i)
+			pow(_e, _e);
+	}
+
+	function pow(uint base, uint exponent) internal pure returns (uint) {
+		if (base == 0) {
+			return 0;
+		}
+		if (exponent == 0) {
+			return 1;
+		}
+		if (exponent == 1) {
+			return base;
+		}
+		uint y = 1;
+		while(exponent > 1) {
+			if(exponent % 2 == 0) {
+				base = base * base;
+				exponent = exponent / 2;
+			} else {
+				y = base * y;
+				base = base * base;
+				exponent = (exponent - 1) / 2;
+			}
+		}
+		return base * y;
+	}
+}
+// ====
+// SMTEngine: chc
+// ----
+// Warning 4984: (176-179): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
+// Warning 4281: (435-447): CHC: Division by zero might happen here.
+// Warning 4984: (467-478): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
+// Warning 4281: (495-507): CHC: Division by zero might happen here.
+// Warning 4984: (529-537): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
+// Warning 4984: (550-561): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
+// Warning 3944: (579-591): CHC: Underflow (resulting value less than 0) might happen here.
+// Warning 4984: (616-624): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.

test/libsolidity/smtCheckerTests/natspec/abstract_function_nondet_pow_with_abstraction.sol

@@ -0,0 +1,35 @@
+contract C {
+	function e(uint _e) public pure {
+		// Without abstracting function `pow` the solver
+		// fails to prove that `++i` does not overflow.
+		for (uint i = 0; i < _e; ++i)
+			pow(_e, _e);
+	}
+
+	/// @custom:smtchecker abstract-function-nondet
+	function pow(uint base, uint exponent) internal pure returns (uint) {
+		if (base == 0) {
+			return 0;
+		}
+		if (exponent == 0) {
+			return 1;
+		}
+		if (exponent == 1) {
+			return base;
+		}
+		uint y = 1;
+		while(exponent > 1) {
+			if(exponent % 2 == 0) {
+				base = base * base;
+				exponent = exponent / 2;
+			} else {
+				y = base * y;
+				base = base * base;
+				exponent = (exponent - 1) / 2;
+			}
+		}
+		return base * y;
+	}
+}
+// ====
+// SMTEngine: chc

test/libsolidity/smtCheckerTests/natspec/natspec_smtchecker_empty.sol

@@ -0,0 +1,11 @@
+contract C {
+	/// @custom:smtchecker
+	function f(uint x) internal pure returns (uint) {
+		return x;
+	}
+}
+// ====
+// SMTEngine: chc
+// ----
+// Warning 3130: (38-102): Unknown option for "custom:smtchecker": ""
+// Warning 3130: (38-102): Unknown option for "custom:smtchecker": ""

test/libsolidity/smtCheckerTests/natspec/natspec_smtchecker_error_1.sol

@@ -0,0 +1,11 @@
+contract C {
+	/// @custom:smtchecker abstract-function
+	function f(uint x) internal pure returns (uint) {
+		return x;
+	}
+}
+// ====
+// SMTEngine: chc
+// ----
+// Warning 3130: (56-120): Unknown option for "custom:smtchecker": "abstract-function"
+// Warning 3130: (56-120): Unknown option for "custom:smtchecker": "abstract-function"

test/libsolidity/smtCheckerTests/natspec/safe_assert_false_positive.sol

@@ -0,0 +1,32 @@
+contract C {
+	uint x;
+	uint y;
+
+	function g(uint _x) public {
+		f1(_x);
+		// If the body of function `f` is ignored while keeping the state,
+		// the assertion is true and not reporting it would be a false negative.
+		// However, since `f` can change the state, the state variables are also
+		// assigned nondeterministic values after a call to `f`.
+		// Therefore the assertion below should fail.
+		assert(x == 0);
+
+		f2(_x);
+		assert(y == 0); // should fail
+	}
+
+	/// @custom:smtchecker abstract-function-nondet
+	function f1(uint _x) internal {
+		x = _x;
+	}
+
+	function f2(uint _y) internal {
+		y = _y;
+	}
+
+}
+// ====
+// SMTEngine: chc
+// ----
+// Warning 6328: (400-414): CHC: Assertion violation happens here.\nCounterexample:\nx = 1, y = 0\n_x = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, y = 0\nC.g(0)\n    C.f1(0) -- internal call
+// Warning 6328: (429-443): CHC: Assertion violation happens here.\nCounterexample:\nx = 1, y = 1\n_x = 1\n\nTransaction trace:\nC.constructor()\nState: x = 0, y = 0\nC.g(1)\n    C.f1(1) -- internal call\n    C.f2(1) -- internal call

test/libsolidity/smtCheckerTests/natspec/safe_assert_false_positive_pure.sol

@@ -0,0 +1,29 @@
+contract C {
+	uint x;
+	uint y;
+
+	function g(uint _x) public {
+		uint z = f1(_x);
+		assert(x == 0); // should hold because f1 is pure
+		assert(z == _x); // should hold but f1 was abstracted as nondet, so it fails
+
+		uint t = f2(_x);
+		assert(y == 0); // should hold because f1 is pure and f2 is view
+		assert(t == _x); // should hold
+	}
+
+	/// @custom:smtchecker abstract-function-nondet
+	function f1(uint _x) internal pure returns (uint) {
+		return _x;
+	}
+
+	function f2(uint _y) internal view returns (uint) {
+		return _y;
+	}
+}
+// ====
+// SMTEngine: chc
+// ----
+// Warning 2018: (33-335): Function state mutability can be restricted to view
+// Warning 2018: (457-524): Function state mutability can be restricted to pure
+// Warning 6328: (135-150): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, y = 0\n_x = 0\nz = 1\nt = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, y = 0\nC.g(0)\n    C.f1(0) -- internal call

test/libsolidity/smtCheckerTests/natspec/unsafe_assert_remains_unsafe.sol

@@ -0,0 +1,27 @@
+contract C {
+	uint x;
+	uint y;
+
+	function g(uint _x) public {
+		f1(_x);
+		assert(x > 0); // should fail
+
+		f2(_x);
+		assert(y > 0); // should fail
+	}
+
+	/// @custom:smtchecker abstract-function-nondet
+	function f1(uint _x) internal {
+		x = _x;
+	}
+
+	function f2(uint _y) internal {
+		y = _y;
+	}
+
+}
+// ====
+// SMTEngine: chc
+// ----
+// Warning 6328: (74-87): CHC: Assertion violation happens here.\nCounterexample:\nx = 0, y = 0\n_x = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, y = 0\nC.g(0)\n    C.f1(0) -- internal call
+// Warning 6328: (117-130): CHC: Assertion violation happens here.\nCounterexample:\nx = 1, y = 0\n_x = 0\n\nTransaction trace:\nC.constructor()\nState: x = 0, y = 0\nC.g(0)\n    C.f1(0) -- internal call\n    C.f2(0) -- internal call

test/libsolidity/smtCheckerTests/operators/conditional_assignment_statevar_1.sol

@@ -14,7 +14,6 @@ contract C {
 // ====
 // SMTEngine: all
 // ----
-// Warning 1218: (134-140): CHC: Error trying to invoke SMT solver.
 // Warning 4984: (134-140): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
 // Warning 4984: (143-146): CHC: Overflow (resulting value larger than 2**256 - 1) might happen here.
 // Warning 2661: (134-140): BMC: Overflow (resulting value larger than 2**256 - 1) happens here.

test/libsolidity/smtCheckerTests/types/array_literal_7.sol

@@ -18,6 +18,7 @@ contract C
 }
 // ====
 // SMTEngine: all
+// SMTIgnoreCex: yes
 // ----
-// Warning 6328: (226-254): CHC: Assertion violation happens here.\nCounterexample:\ns = [1, 2, 3]\na = [1, 2, 3]\nb = [1, 2, 4, 3]\nc = [1, 2, 4, 3]\n\nTransaction trace:\nC.constructor()\nState: s = []\nC.f()
+// Warning 6328: (226-254): CHC: Assertion violation happens here.
-// Warning 6328: (315-335): CHC: Assertion violation happens here.\nCounterexample:\ns = [1, 2, 3]\na = [1, 2, 3]\nb = [1, 2, 4, 3]\nc = [1, 2, 4, 3]\n\nTransaction trace:\nC.constructor()\nState: s = []\nC.f()
+// Warning 6328: (315-335): CHC: Assertion violation happens here.