8.2.3 Release

8.2.3 Release

9b370d58c06748873dd9c1d52ba11e394ec3b042

Author: yoav-el-certora

Public/TestEVM/CVLCompilation/StorageReset/Run.conf

@@ -0,0 +1,19 @@
+{
+    "build_cache": true,
+    "files": [
+        "Test.sol"
+    ],
+    "loop_iter": 3,
+    "msg": "buggy ghost",
+    "optimistic_loop": true,
+    "parametric_contracts": [
+        "Test"
+    ],
+    "rule": [
+        "buggyGhost"
+    ],
+    "rule_sanity": "basic",
+    "solc": "solc8.28",
+    "solc_via_ir": true,
+    "verify": "Test:Test.spec"
+}

Public/TestEVM/CVLCompilation/StorageReset/Test.sol

@@ -0,0 +1,5 @@
+contract Test {
+    uint public i;
+
+    function bar() external {}
+}

Public/TestEVM/CVLCompilation/StorageReset/Test.spec

@@ -0,0 +1,15 @@
+ghost uint256 cachedIndex;
+
+rule buggyGhost(uint256 assetId) {
+    env e;
+
+    cachedIndex = currentContract.i;
+    uint256 before = cachedIndex;
+
+    storage init_state = lastStorage;
+
+    assert before == cachedIndex;
+
+    bar(e) at init_state;
+    assert before == cachedIndex;
+}

Public/TestEVM/CVLCompilation/StorageReset/expectedRun.json

@@ -0,0 +1,5 @@
+{
+  "rules": {
+    "buggyGhost": "SUCCESS"
+  }
+}

Public/TestEVM/Regressions/CERT-9534/Default.conf

@@ -0,0 +1,8 @@
+{
+    "files": [
+        "./Test.sol:Test"
+    ],
+    "optimistic_loop": true,
+    "solc": "solc4.24",
+    "verify": "Test:./trivial.spec"
+}

Public/TestEVM/Regressions/CERT-9534/Test.sol

@@ -0,0 +1,14 @@
+contract Test {
+	function doThing(uint x) internal returns (uint, uint[] memory, uint[] memory) {
+		if(x == 4) {
+			return (0, new uint[](0), new uint[](0));
+		}
+		uint[] memory y = new uint[](x);
+		uint[] memory z = new uint[](x);
+		return (x, y, z);
+	}
+
+	function doStuff(uint z) external {
+		doThing(z);
+	}
+}

Public/TestEVM/Regressions/CERT-9534/expectedDefault.json

@@ -0,0 +1,10 @@
+{
+	"rules": {
+		"trivial": {
+			"SUCCESS": [
+				"doStuff(uint256)"
+			]
+		},
+		"whatever": "SUCCESS"
+	}
+}

Public/TestEVM/Regressions/CERT-9534/trivial.spec

@@ -0,0 +1,10 @@
+rule trivial(method f) {
+	env e;
+	calldataarg arg;
+	f(e, arg);
+	assert true;
+}
+
+rule whatever {
+	assert true;
+}

Public/TestRanger/Merging/Range2.conf

@@ -0,0 +1,8 @@
+{
+    range: "2",
+    ranger_failure_limit: "0",
+    files: ["C.sol"],
+    java_args: ["-Dlevel.bounded.model.checker=info"],
+    prover_args: ["-bmcMerger true"],
+    verify: "C:C.spec"
+}

Public/TestRanger/Merging/expectedRange2.txt

@@ -0,0 +1,3 @@
+bNot1: FAIL
+cNot2: SUCCESS
+cNot8: SUCCESS