Merge pull request #6675 from ethereum/smt_delete

[SMTChecker] Support delete

test/libsolidity/smtCheckerTests/operators/delete_array.sol

@@ -0,0 +1,21 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	uint[] a;
+	function f(bool b) public {
+		a[2] = 3;
+		require(b);
+		if (b)
+			delete a;
+		else
+			delete a[2];
+		// Assertion fails as false positive because
+		// setZeroValue for arrays needs \forall i . a[i] = 0
+		// which is still unimplemented.
+		assert(a[2] == 0);
+	}
+}
+// ----
+// Warning: (118-119): Condition is always true.
+// Warning: (297-314): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/delete_array_2d.sol

@@ -0,0 +1,15 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	uint[][] a;
+	function f() public {
+		require(a[2][3] == 4);
+		delete a;
+		// Fails as false positive.
+		// setZeroValue needs forall for arrays.
+		assert(a[2][3] == 0);
+	}
+}
+// ----
+// Warning: (194-214): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/delete_array_index.sol

@@ -0,0 +1,17 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	uint[] a;
+	function f(bool b) public {
+		a[2] = 3;
+		require(!b);
+		if (b)
+			delete a;
+		else
+			delete a[2];
+		assert(a[2] == 0);
+	}
+}
+// ----
+// Warning: (119-120): Condition is always false.

test/libsolidity/smtCheckerTests/operators/delete_array_index_2d.sol

@@ -0,0 +1,19 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	uint[][] a;
+	function f(bool b) public {
+		require(a[2][3] == 4);
+		if (b)
+			delete a;
+		else
+			delete a[2];
+		// Fails as false positive since
+		// setZeroValue for arrays needs forall
+		// which is unimplemented.
+		assert(a[2][3] == 0);
+	}
+}
+// ----
+// Warning: (266-286): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/delete_function.sol

@@ -0,0 +1,27 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	uint[] a;
+	function g() internal {
+		delete a;
+	}
+	function h() internal {
+		delete a[2];
+	}
+	function f(bool b) public {
+		a[2] = 3;
+		require(b);
+		if (b)
+			g();
+		else
+			h();
+		// Assertion fails as false positive because
+		// setZeroValue for arrays needs \forall i . a[i] = 0
+		// which is still unimplemented.
+		assert(a[2] == 0);
+	}
+}
+// ----
+// Warning: (201-202): Condition is always true.
+// Warning: (367-384): Assertion violation happens here

test/libsolidity/smtCheckerTests/operators/delete_struct.sol

@@ -0,0 +1,27 @@
+pragma experimental SMTChecker;
+
+contract C
+{
+	struct S
+	{
+		uint x;
+	}
+	function f(bool b) public {
+		S memory s;
+		s.x = 2;
+		if (b)
+			delete s;
+		else
+			delete s.x;
+		assert(s.x == 0);
+	}
+}
+// ----
+// Warning: (73-192): Function state mutability can be restricted to pure
+// Warning: (103-113): Assertion checker does not yet support the type of this variable.
+// Warning: (117-120): Assertion checker does not yet support this expression.
+// Warning: (117-124): Assertion checker does not yet implement such assignments.
+// Warning: (165-168): Assertion checker does not yet support this expression.
+// Warning: (158-168): Assertion checker does not yet implement "delete" for this expression.
+// Warning: (179-182): Assertion checker does not yet support this expression.
+// Warning: (172-188): Assertion violation happens here