checkSymbolic -> symbolic

OpenZeppelin · May 22, 2024 · 8366a6d · 8366a6d
1 parent b4a1141
commit 8366a6d
Show file tree

Hide file tree

Showing 5 changed files with 12 additions and 12 deletions.
diff --git a/.github/workflows/formal-verification.yml b/.github/workflows/formal-verification.yml
@@ -83,4 +83,4 @@ jobs:
       - name: Install python packages
         run: pip install -r fv-requirements.txt
       - name: Run Halmos
-        run: halmos --match-test '^checkSymbolic|^testSymbolic' -vv
+        run: halmos --match-test '^symbolic|^testSymbolic' -vv
diff --git a/scripts/generate/templates/SlotDerivation.t.js b/scripts/generate/templates/SlotDerivation.t.js
@@ -13,7 +13,7 @@ import {SlotDerivation} from "@openzeppelin/contracts/utils/SlotDerivation.sol";
 const array = `\
 bytes[] private _array;
 
-function checkSymbolicDeriveArray(uint256 length, uint256 offset) public {
+function symbolicDeriveArray(uint256 length, uint256 offset) public {
   vm.assume(length > 0);
   vm.assume(offset < length);
   _assertDeriveArray(length, offset);
@@ -68,7 +68,7 @@ function testDeriveMapping${name}(${type} memory key) public {
   _assertDeriveMapping${name}(key);
 }
 
-function checkSymbolicDeriveMapping${name}() public {
+function symbolicDeriveMapping${name}() public {
   _assertDeriveMapping${name}(svm.create${name}(256, "DeriveMapping${name}Input"));
 }
 

diff --git a/test/utils/Arrays.t.sol b/test/utils/Arrays.t.sol
@@ -12,7 +12,7 @@ contract ArraysTest is Test, SymTest {
         _assertSort(values);
     }
 
-    function checkSymbolicSort() public {
+    function symbolicSort() public {
         uint256[] memory values = new uint256[](3);
         for (uint256 i = 0; i < 3; i++) {
             values[i] = svm.createUint256("arrayElement");

diff --git a/test/utils/ShortStrings.t.sol b/test/utils/ShortStrings.t.sol
@@ -15,7 +15,7 @@ contract ShortStringsTest is Test, SymTest {
         _assertRoundtripShort(input);
     }
 
-    function checkSymbolicRoundtripShort() external {
+    function symbolicRoundtripShort() external {
         string memory input = svm.createString(31, "RoundtripShortInput");
         _assertRoundtripShort(input);
     }
@@ -24,13 +24,13 @@ contract ShortStringsTest is Test, SymTest {
         _assertRoundtripWithFallback(input, fallbackInitial);
     }
 
-    function checkSymbolicRoundtripWithFallbackLong() external {
+    function symbolicRoundtripWithFallbackLong() external {
         string memory input = svm.createString(256, "RoundtripWithFallbackInput");
         string memory fallbackInitial = svm.createString(256, "RoundtripWithFallbackFallbackInitial");
         _assertRoundtripWithFallback(input, fallbackInitial);
     }
 
-    function checkSymbolicRoundtripWithFallbackShort() external {
+    function symbolicRoundtripWithFallbackShort() external {
         string memory input = svm.createString(31, "RoundtripWithFallbackInput");
         string memory fallbackInitial = svm.createString(31, "RoundtripWithFallbackFallbackInitial");
         _assertRoundtripWithFallback(input, fallbackInitial);
@@ -46,7 +46,7 @@ contract ShortStringsTest is Test, SymTest {
         _assertLengthShort(input);
     }
 
-    function checkSymbolicLengthShort() external {
+    function symbolicLengthShort() external {
         string memory input = svm.createString(31, "LengthShortInput");
         _assertLengthShort(input);
     }
@@ -56,7 +56,7 @@ contract ShortStringsTest is Test, SymTest {
         _assertLengthWithFallback(input);
     }
 
-    function checkSymbolicLengthWithFallback() external {
+    function symbolicLengthWithFallback() external {
         uint256 length = 256;
         string memory input = svm.createString(length, "LengthWithFallbackInput");
         string memory fallbackInitial = svm.createString(length, "LengthWithFallbackFallbackInitial");

diff --git a/test/utils/SlotDerivation.t.sol b/test/utils/SlotDerivation.t.sol
@@ -12,7 +12,7 @@ contract SlotDerivationTest is Test, SymTest {
 
     bytes[] private _array;
 
-    function checkSymbolicDeriveArray(uint256 length, uint256 offset) public {
+    function symbolicDeriveArray(uint256 length, uint256 offset) public {
         vm.assume(length > 0);
         vm.assume(offset < length);
         _assertDeriveArray(length, offset);
@@ -182,7 +182,7 @@ contract SlotDerivationTest is Test, SymTest {
         _assertDeriveMappingString(key);
     }
 
-    function checkSymbolicDeriveMappingString() public {
+    function symbolicDeriveMappingString() public {
         _assertDeriveMappingString(svm.createString(256, "DeriveMappingStringInput"));
     }
 
@@ -207,7 +207,7 @@ contract SlotDerivationTest is Test, SymTest {
         _assertDeriveMappingBytes(key);
     }
 
-    function checkSymbolicDeriveMappingBytes() public {
+    function symbolicDeriveMappingBytes() public {
         _assertDeriveMappingBytes(svm.createBytes(256, "DeriveMappingBytesInput"));
     }