8.2.1 Release

Author: yoav-el-certora

Public/CITests/testMutateClient.py

@@ -127,7 +127,7 @@ def test_conf_file_inputs(self) -> None:
         bad_location = f'"manual_mutants": [{{ "file_to_mutate": "{_p("A.sol")}", "mutants_location": "{_p("bad_location")}"}}]'
         suite.expect_failure(description="manual_mutants object missing file_to_mutate",
                              replacements=TestUtil.replace_x(bad_location),
-                             expected="Invalid mutants location")
+                             expected="Invalid file for mutants location")
 
     def test_invalid_runs(self) -> None:
         suite = MutantTestSuite(conf_file_template=_p('mutation_conf_top_level.conf'),
@@ -187,7 +187,7 @@ def test_compile_mutation(self) -> None:
         mutation_attrs['manual_mutants'][0]['mutants_location'] = "does_not_exist"
         suite.expect_failure(description="single manual mutation - bad location",
                              replacements=TestUtil.replace_x(TestUtil.json_to_str(mutation_attrs)),
-                             expected="Invalid mutants location")
+                             expected="Invalid file for mutants location")
 
     def test_mutations_flags(self) -> None:
 

Public/TestEVM/CVLCompilation/StorageComparison/Havoc/Havoc.conf

@@ -0,0 +1,8 @@
+{
+    "files": [
+        "Test.sol"
+    ],
+    "msg": "buggy havoc",
+    "solc": "solc8.28",
+    "verify": "Test:Havoc.spec"
+}

Public/TestEVM/CVLCompilation/StorageComparison/Havoc/Havoc.spec

@@ -0,0 +1,13 @@
+rule testHavoc() {
+    env e;
+    uint before = currentContract.i;
+    storage init = lastStorage;
+
+    changeI(e, 2);
+
+    havoc currentContract.i;
+    require currentContract.i == before, "putting back the old value";
+
+    // this should succeed thanks to the havoc and require
+    assert lastStorage == init;
+}

Public/TestEVM/CVLCompilation/StorageComparison/Havoc/Test.sol

@@ -0,0 +1,7 @@
+contract Test {
+    uint public i;
+
+    function changeI(uint val) external {
+        i = val;
+    }
+}

Public/TestEVM/CVLCompilation/StorageComparison/Havoc/expectedHavoc.json

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