8.2.2 Release

8.2.2 Release

7308a93ca35c5a1e6b93c8cfdb52ab8da932b372

Author: yoav-el-certora

.gitignore

@@ -1 +1,2 @@
 .idea/
+

Public/TestEVM/FunctionFinders/EmptyModifiers/Test.sol

@@ -6,7 +6,7 @@ contract Test {
 		_;
 	}
 
-	function int_f(string memory) internal initOnly returns (uint) {
+	function int_f(string memory y) internal initOnly returns (uint) {
 		return 0;
 	}
 

Public/TestEVM/MethodPickingTest/Bad.conf

@@ -4,6 +4,6 @@
         "C.sol:D",
         "C.sol:E"
     ],
-    method: ["C.foo(uint256,bool[3][])", "D.foo((uint256,bool[3][]))"],
+    method: ["C.foo(uint256,bool[3][2])", "D.foo((uint256,bool[3][2]))"],
     verify: "C:C.spec"
 }

Public/TestEVM/MethodPickingTest/C.sol

@@ -1,7 +1,7 @@
 contract C {
     struct S {
         uint a;
-        bool[3][] b;
+        bool[3][2] b;
     }
 
     function foo(S memory s) external {}
@@ -11,7 +11,7 @@ contract C {
 contract D {
     struct S {
         uint a;
-        bool[3][] b;
+        bool[3][2] b;
     }
 
     function bar(S memory s) external {}
@@ -21,7 +21,7 @@ contract D {
 contract E {
     struct S {
         uint a;
-        bool[3][] b;
+        bool[3][2] b;
     }
 
     function foo(S memory s) external {}

Public/TestEVM/MethodPickingTest/C.spec

@@ -2,3 +2,5 @@ rule r(method f, env e, calldataarg args) {
     f(e, args);
     satisfy true;
 }
+
+invariant i() 5 >= 0;

Public/TestEVM/MethodPickingTest/ExcludeOnly.conf

@@ -5,9 +5,9 @@
         "C.sol:E"
     ],
     exclude_method: [
-        "foo((uint256,bool[3][]))", // Should exclude only C.foo
-        "D.bar((uint256,bool[3][]))", // Should exclude only D.bar
-        "_.baz((uint256,bool[3][]))" // Should exclude both D.baz and E.baz
+        "foo((uint256,bool[3][2]))", // Should exclude only C.foo
+        "D.bar((uint256,bool[3][2]))", // Should exclude only D.bar
+        "_.baz((uint256,bool[3][2]))" // Should exclude both D.baz and E.baz
     ],
     verify: "C:C.spec"
 }

Public/TestEVM/MethodPickingTest/IncludeAndExclude.conf

@@ -5,12 +5,12 @@
         "C.sol:E"
     ],
     method: [
-        "foo((uint256,bool[3][]))", // Should take only C.foo
-        "D.bar((uint256,bool[3][]))", // Should take only D.bar
-        "_.baz((uint256,bool[3][]))" // Should take both D.baz and E.baz
+        "foo((uint256,bool[3][2]))", // Should take only C.foo
+        "D.bar((uint256,bool[3][2]))", // Should take only D.bar
+        "_.baz((uint256,bool[3][2]))" // Should take both D.baz and E.baz
     ],
     exclude_method: [
-        "D.baz((uint256,bool[3][]))" // should remove D.baz from the set
+        "D.baz((uint256,bool[3][2]))" // should remove D.baz from the set
     ],
     verify: "C:C.spec"
 }

Public/TestEVM/MethodPickingTest/IncludeOnly.conf

@@ -5,9 +5,9 @@
         "C.sol:E"
     ],
     method: [
-        "foo((uint256,bool[3][]))", // Should take only C.foo
-        "D.bar((uint256,bool[3][]))", // Should take only D.bar
-        "_.baz((uint256,bool[3][]))" // Should take both D.baz and E.baz
+        "foo((uint256,bool[3][2]))", // Should take only C.foo
+        "D.bar((uint256,bool[3][2]))", // Should take only D.bar
+        "_.baz((uint256,bool[3][2]))" // Should take both D.baz and E.baz
     ],
     verify: "C:C.spec"
 }

Public/TestEVM/MethodPickingTest/expectedBad.txt

@@ -1,2 +1,2 @@
-Error in spec file: Could not find a method named C.foo(uint256,bool[3][]) in the scene. Did you mean C.foo((uint256,bool[3][]))?
-Error in spec file: Could not find a method named D.foo((uint256,bool[3][])) in the scene. Did you mean C.foo((uint256,bool[3][])) or E.foo((uint256,bool[3][]))?
+Error in spec file: Could not find a method named C.foo(uint256,bool[3][2]) in the scene. Did you mean C.foo((uint256,bool[3][2]))?
+Error in spec file: Could not find a method named D.foo((uint256,bool[3][2])) in the scene. Did you mean C.foo((uint256,bool[3][2])) or E.foo((uint256,bool[3][2]))?

Public/TestEVM/MethodPickingTest/expectedExcludeOnly.json

@@ -5,11 +5,22 @@
 			"FAIL": [],
 			"SANITY_FAIL": [],
 			"SUCCESS": [
-				"C.bar((uint256,bool[3][]))",
-				"E.foo((uint256,bool[3][]))"
+				"C.bar((uint256,bool[3][2]))",
+				"E.foo((uint256,bool[3][2]))"
 			],
 			"TIMEOUT": [],
 			"UNKNOWN": []
-		}
-	}
-}
+		},
+    "i": {
+      "Induction base: After the constructor": "SANITY_FAIL",
+      "Induction step: after external (non-view) methods": {
+        "Using general requirements": {
+          "SANITY_FAIL": [
+            "C.bar((uint256,bool[3][2]))",
+            "E.foo((uint256,bool[3][2]))"
+          ]
+        }
+      }
+    }
+  }
+}