update kontrol specs

runtimeverification · Mar 15, 2024 · 9f54f54 · 9f54f54
1 parent 7605b2e
commit 9f54f54
Show file tree

Hide file tree

Showing 24 changed files with 93 additions and 0 deletions.
diff --git a/tests/specs/kontrol/test-allowchangestest-testallow-0-spec.k b/tests/specs/kontrol/test-allowchangestest-testallow-0-spec.k
@@ -19,6 +19,9 @@ module TEST-ALLOWCHANGESTEST-TESTALLOW-0-SPEC
            <schedule>
              SHANGHAI
            </schedule>
+           <scheduleTuple>
+             getSchedule(SHANGHAI)
+           </scheduleTuple>
            <useGas>
              true
            </useGas>

diff --git a/tests/specs/kontrol/test-allowchangestest-testallow_fail-0-spec.k b/tests/specs/kontrol/test-allowchangestest-testallow_fail-0-spec.k
@@ -19,6 +19,9 @@ module TEST-ALLOWCHANGESTEST-TESTALLOW_FAIL-0-SPEC
            <schedule>
              SHANGHAI
            </schedule>
+           <scheduleTuple>
+             getSchedule(SHANGHAI)
+           </scheduleTuple>
            <useGas>
              true
            </useGas>

diff --git a/tests/specs/kontrol/test-allowchangestest-testfailallowcallstoaddress-0-spec.k b/tests/specs/kontrol/test-allowchangestest-testfailallowcallstoaddress-0-spec.k
@@ -19,6 +19,9 @@ module TEST-ALLOWCHANGESTEST-TESTFAILALLOWCALLSTOADDRESS-0-SPEC
            <schedule>
              SHANGHAI
            </schedule>
+           <scheduleTuple>
+             getSchedule(SHANGHAI)
+           </scheduleTuple>
            <useGas>
              true
            </useGas>

diff --git a/tests/specs/kontrol/test-allowchangestest-testfailallowchangestostorage-0-spec.k b/tests/specs/kontrol/test-allowchangestest-testfailallowchangestostorage-0-spec.k
@@ -19,6 +19,9 @@ module TEST-ALLOWCHANGESTEST-TESTFAILALLOWCHANGESTOSTORAGE-0-SPEC
            <schedule>
              SHANGHAI
            </schedule>
+           <scheduleTuple>
+             getSchedule(SHANGHAI)
+           </scheduleTuple>
            <useGas>
              true
            </useGas>
@@ -321,6 +324,9 @@ module TEST-ALLOWCHANGESTEST-TESTFAILALLOWCHANGESTOSTORAGE-0-SPEC
            <schedule>
              SHANGHAI
            </schedule>
+           <scheduleTuple>
+             getSchedule(SHANGHAI)
+           </scheduleTuple>
            <useGas>
              true
            </useGas>

diff --git a/tests/specs/kontrol/test-arithmetictest-test_max1_broken-uint256-uint256-0-spec.k b/tests/specs/kontrol/test-arithmetictest-test_max1_broken-uint256-uint256-0-spec.k
@@ -17,6 +17,9 @@ module TEST-ARITHMETICTEST-TEST_MAX1_BROKEN-UINT256-UINT256-0-SPEC
            <schedule>
              SHANGHAI
            </schedule>
+           <scheduleTuple>
+             getSchedule(SHANGHAI)
+           </scheduleTuple>
            <useGas>
              true
            </useGas>

diff --git a/tests/specs/kontrol/test-arithmetictest-test_wdiv_rounding-uint256-uint256-0-spec.k b/tests/specs/kontrol/test-arithmetictest-test_wdiv_rounding-uint256-uint256-0-spec.k
@@ -16,6 +16,9 @@ module TEST-ARITHMETICTEST-TEST_WDIV_ROUNDING-UINT256-UINT256-0-SPEC
            <schedule>
              SHANGHAI
            </schedule>
+           <scheduleTuple>
+             getSchedule(SHANGHAI)
+           </scheduleTuple>
            <useGas>
              true
            </useGas>

diff --git a/...ecs/kontrol/test-arithmetictest-test_wmul_wdiv_inverse_underflow-uint256-uint256-0-spec.k b/...ecs/kontrol/test-arithmetictest-test_wmul_wdiv_inverse_underflow-uint256-uint256-0-spec.k
@@ -16,6 +16,9 @@ module TEST-ARITHMETICTEST-TEST_WMUL_WDIV_INVERSE_UNDERFLOW-UINT256-UINT256-0-SP
            <schedule>
              SHANGHAI
            </schedule>
+           <scheduleTuple>
+             getSchedule(SHANGHAI)
+           </scheduleTuple>
            <useGas>
              true
            </useGas>

diff --git a/...kontrol/test-arithmetictest-test_wmul_weakly_increasing_positive-uint256-uint256-0-spec.k b/...kontrol/test-arithmetictest-test_wmul_weakly_increasing_positive-uint256-uint256-0-spec.k
@@ -16,6 +16,9 @@ module TEST-ARITHMETICTEST-TEST_WMUL_WEAKLY_INCREASING_POSITIVE-UINT256-UINT256-
            <schedule>
              SHANGHAI
            </schedule>
+           <scheduleTuple>
+             getSchedule(SHANGHAI)
+           </scheduleTuple>
            <useGas>
              true
            </useGas>
@@ -169,6 +172,9 @@ module TEST-ARITHMETICTEST-TEST_WMUL_WEAKLY_INCREASING_POSITIVE-UINT256-UINT256-
            <schedule>
              SHANGHAI
            </schedule>
+           <scheduleTuple>
+             getSchedule(SHANGHAI)
+           </scheduleTuple>
            <useGas>
              true
            </useGas>

diff --git a/tests/specs/kontrol/test-countertest-testincrement-0-spec.k b/tests/specs/kontrol/test-countertest-testincrement-0-spec.k
@@ -19,6 +19,9 @@ module TEST-COUNTERTEST-TESTINCREMENT-0-SPEC
            <schedule>
              SHANGHAI
            </schedule>
+           <scheduleTuple>
+             getSchedule(SHANGHAI)
+           </scheduleTuple>
            <useGas>
              true
            </useGas>
@@ -323,6 +326,9 @@ module TEST-COUNTERTEST-TESTINCREMENT-0-SPEC
            <schedule>
              SHANGHAI
            </schedule>
+           <scheduleTuple>
+             getSchedule(SHANGHAI)
+           </scheduleTuple>
            <useGas>
              true
            </useGas>
@@ -631,6 +637,9 @@ module TEST-COUNTERTEST-TESTINCREMENT-0-SPEC
            <schedule>
              SHANGHAI
            </schedule>
+           <scheduleTuple>
+             getSchedule(SHANGHAI)
+           </scheduleTuple>
            <useGas>
              true
            </useGas>

diff --git a/tests/specs/kontrol/test-emitcontracttest-testexpectemit-0-spec.k b/tests/specs/kontrol/test-emitcontracttest-testexpectemit-0-spec.k
@@ -19,6 +19,9 @@ module TEST-EMITCONTRACTTEST-TESTEXPECTEMIT-0-SPEC
            <schedule>
              SHANGHAI
            </schedule>
+           <scheduleTuple>
+             getSchedule(SHANGHAI)
+           </scheduleTuple>
            <useGas>
              true
            </useGas>

diff --git a/tests/specs/kontrol/test-emitcontracttest-testexpectemitcheckemitter-0-spec.k b/tests/specs/kontrol/test-emitcontracttest-testexpectemitcheckemitter-0-spec.k
@@ -19,6 +19,9 @@ module TEST-EMITCONTRACTTEST-TESTEXPECTEMITCHECKEMITTER-0-SPEC
            <schedule>
              SHANGHAI
            </schedule>
+           <scheduleTuple>
+             getSchedule(SHANGHAI)
+           </scheduleTuple>
            <useGas>
              true
            </useGas>

diff --git a/tests/specs/kontrol/test-emitcontracttest-testexpectemitdonotcheckdata-0-spec.k b/tests/specs/kontrol/test-emitcontracttest-testexpectemitdonotcheckdata-0-spec.k
@@ -19,6 +19,9 @@ module TEST-EMITCONTRACTTEST-TESTEXPECTEMITDONOTCHECKDATA-0-SPEC
            <schedule>
              SHANGHAI
            </schedule>
+           <scheduleTuple>
+             getSchedule(SHANGHAI)
+           </scheduleTuple>
            <useGas>
              true
            </useGas>

diff --git a/tests/specs/kontrol/test-expectcalltest-testexpectregularcall-0-spec.k b/tests/specs/kontrol/test-expectcalltest-testexpectregularcall-0-spec.k
@@ -19,6 +19,9 @@ module TEST-EXPECTCALLTEST-TESTEXPECTREGULARCALL-0-SPEC
            <schedule>
              SHANGHAI
            </schedule>
+           <scheduleTuple>
+             getSchedule(SHANGHAI)
+           </scheduleTuple>
            <useGas>
              true
            </useGas>

diff --git a/tests/specs/kontrol/test-expectcalltest-testexpectstaticcall-0-spec.k b/tests/specs/kontrol/test-expectcalltest-testexpectstaticcall-0-spec.k
@@ -19,6 +19,9 @@ module TEST-EXPECTCALLTEST-TESTEXPECTSTATICCALL-0-SPEC
            <schedule>
              SHANGHAI
            </schedule>
+           <scheduleTuple>
+             getSchedule(SHANGHAI)
+           </scheduleTuple>
            <useGas>
              true
            </useGas>

diff --git a/tests/specs/kontrol/test-expectreverttest-test_expectrevert_bytes4-0-spec.k b/tests/specs/kontrol/test-expectreverttest-test_expectrevert_bytes4-0-spec.k
@@ -19,6 +19,9 @@ module TEST-EXPECTREVERTTEST-TEST_EXPECTREVERT_BYTES4-0-SPEC
            <schedule>
              SHANGHAI
            </schedule>
+           <scheduleTuple>
+             getSchedule(SHANGHAI)
+           </scheduleTuple>
            <useGas>
              true
            </useGas>
@@ -319,6 +322,9 @@ module TEST-EXPECTREVERTTEST-TEST_EXPECTREVERT_BYTES4-0-SPEC
            <schedule>
              SHANGHAI
            </schedule>
+           <scheduleTuple>
+             getSchedule(SHANGHAI)
+           </scheduleTuple>
            <useGas>
              true
            </useGas>

diff --git a/tests/specs/kontrol/test-expectreverttest-test_expectrevert_message-0-spec.k b/tests/specs/kontrol/test-expectreverttest-test_expectrevert_message-0-spec.k
@@ -19,6 +19,9 @@ module TEST-EXPECTREVERTTEST-TEST_EXPECTREVERT_MESSAGE-0-SPEC
            <schedule>
              SHANGHAI
            </schedule>
+           <scheduleTuple>
+             getSchedule(SHANGHAI)
+           </scheduleTuple>
            <useGas>
              true
            </useGas>

diff --git a/tests/specs/kontrol/test-expectreverttest-test_expectrevert_returnvalue-0-spec.k b/tests/specs/kontrol/test-expectreverttest-test_expectrevert_returnvalue-0-spec.k
@@ -19,6 +19,9 @@ module TEST-EXPECTREVERTTEST-TEST_EXPECTREVERT_RETURNVALUE-0-SPEC
            <schedule>
              SHANGHAI
            </schedule>
+           <scheduleTuple>
+             getSchedule(SHANGHAI)
+           </scheduleTuple>
            <useGas>
              true
            </useGas>

diff --git a/tests/specs/kontrol/test-expectreverttest-testfail_expectrevert_bytes4-0-spec.k b/tests/specs/kontrol/test-expectreverttest-testfail_expectrevert_bytes4-0-spec.k
@@ -19,6 +19,9 @@ module TEST-EXPECTREVERTTEST-TESTFAIL_EXPECTREVERT_BYTES4-0-SPEC
            <schedule>
              SHANGHAI
            </schedule>
+           <scheduleTuple>
+             getSchedule(SHANGHAI)
+           </scheduleTuple>
            <useGas>
              true
            </useGas>

diff --git a/tests/specs/kontrol/test-expectreverttest-testfail_expectrevert_failandsuccess-0-spec.k b/tests/specs/kontrol/test-expectreverttest-testfail_expectrevert_failandsuccess-0-spec.k
@@ -19,6 +19,9 @@ module TEST-EXPECTREVERTTEST-TESTFAIL_EXPECTREVERT_FAILANDSUCCESS-0-SPEC
            <schedule>
              SHANGHAI
            </schedule>
+           <scheduleTuple>
+             getSchedule(SHANGHAI)
+           </scheduleTuple>
            <useGas>
              true
            </useGas>

diff --git a/tests/specs/kontrol/test-expectreverttest-testfail_expectrevert_false-0-spec.k b/tests/specs/kontrol/test-expectreverttest-testfail_expectrevert_false-0-spec.k
@@ -19,6 +19,9 @@ module TEST-EXPECTREVERTTEST-TESTFAIL_EXPECTREVERT_FALSE-0-SPEC
            <schedule>
              SHANGHAI
            </schedule>
+           <scheduleTuple>
+             getSchedule(SHANGHAI)
+           </scheduleTuple>
            <useGas>
              true
            </useGas>
@@ -317,6 +320,9 @@ module TEST-EXPECTREVERTTEST-TESTFAIL_EXPECTREVERT_FALSE-0-SPEC
            <schedule>
              SHANGHAI
            </schedule>
+           <scheduleTuple>
+             getSchedule(SHANGHAI)
+           </scheduleTuple>
            <useGas>
              true
            </useGas>

diff --git a/tests/specs/kontrol/test-owneruponlytest-testincrementasowner-0-spec.k b/tests/specs/kontrol/test-owneruponlytest-testincrementasowner-0-spec.k
@@ -19,6 +19,9 @@ module TEST-OWNERUPONLYTEST-TESTINCREMENTASOWNER-0-SPEC
            <schedule>
              SHANGHAI
            </schedule>
+           <scheduleTuple>
+             getSchedule(SHANGHAI)
+           </scheduleTuple>
            <useGas>
              true
            </useGas>
@@ -321,6 +324,9 @@ module TEST-OWNERUPONLYTEST-TESTINCREMENTASOWNER-0-SPEC
            <schedule>
              SHANGHAI
            </schedule>
+           <scheduleTuple>
+             getSchedule(SHANGHAI)
+           </scheduleTuple>
            <useGas>
              true
            </useGas>

diff --git a/tests/specs/kontrol/test-safetest-testwithdrawfuzz-uint96-0-spec.k b/tests/specs/kontrol/test-safetest-testwithdrawfuzz-uint96-0-spec.k
@@ -19,6 +19,9 @@ module TEST-SAFETEST-TESTWITHDRAWFUZZ-UINT96-0-SPEC
            <schedule>
              SHANGHAI
            </schedule>
+           <scheduleTuple>
+             getSchedule(SHANGHAI)
+           </scheduleTuple>
            <useGas>
              true
            </useGas>

diff --git a/tests/specs/kontrol/test-storetest-testaccesses-0-spec.k b/tests/specs/kontrol/test-storetest-testaccesses-0-spec.k
@@ -19,6 +19,9 @@ module TEST-STORETEST-TESTACCESSES-0-SPEC
            <schedule>
              SHANGHAI
            </schedule>
+           <scheduleTuple>
+             getSchedule(SHANGHAI)
+           </scheduleTuple>
            <useGas>
              true
            </useGas>

diff --git a/tests/specs/kontrol/test-storetest-teststoreload-0-spec.k b/tests/specs/kontrol/test-storetest-teststoreload-0-spec.k
@@ -19,6 +19,9 @@ module TEST-STORETEST-TESTSTORELOAD-0-SPEC
            <schedule>
              SHANGHAI
            </schedule>
+           <scheduleTuple>
+             getSchedule(SHANGHAI)
+           </scheduleTuple>
            <useGas>
              true
            </useGas>