diff --git a/.github/workflows/test-pr.yml b/.github/workflows/test-pr.yml index 8ce11f6006..c743855c83 100644 --- a/.github/workflows/test-pr.yml +++ b/.github/workflows/test-pr.yml @@ -81,7 +81,7 @@ jobs: name: 'Build and Test KEVM concrete execution' needs: kevm-pyk-code-quality-checks runs-on: [self-hosted, linux, normal] - timeout-minutes: 35 + timeout-minutes: 45 steps: - name: 'Check out code' uses: actions/checkout@v3 diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 9bcc95b3eb..97fc2a032b 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.223" +version = "1.0.224" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py index 175e3f30f7..ed5de539f5 100644 --- a/kevm-pyk/src/kevm_pyk/__main__.py +++ b/kevm-pyk/src/kevm_pyk/__main__.py @@ -22,9 +22,9 @@ from .cli import KEVMCLIArgs, node_id_like from .foundry import ( Foundry, - FoundryNodePrinter, foundry_kompile, foundry_list, + foundry_node_printer, foundry_prove, foundry_remove_node, foundry_section_edge, @@ -34,7 +34,7 @@ foundry_to_dot, ) from .gst_to_kore import _mode_to_kore, _schedule_to_kore -from .kevm import KEVM, KEVMNodePrinter +from .kevm import KEVM, kevm_node_printer from .kompile import KompileTarget, kevm_kompile from .solc_to_k import solc_compile, solc_to_k from .utils import arg_pair_of, ensure_ksequence_on_k_cell, get_apr_proof_for_spec, kevm_apr_prove, print_failure_info @@ -440,7 +440,9 @@ def exec_show_kcfg( exclude_claim_labels=exclude_claim_labels, ) - proof_show = APRProofShow(kevm, node_printer=KEVMNodePrinter(kevm)) + node_printer = kevm_node_printer(kevm, proof) + proof_show = APRProofShow(kevm, node_printer=node_printer) + res_lines = proof_show.show( proof, nodes=nodes, @@ -469,7 +471,7 @@ def exec_view_kcfg( **kwargs: Any, ) -> None: kevm = KEVM(definition_dir) - apr_proof = get_apr_proof_for_spec( + proof = get_apr_proof_for_spec( kevm, spec_file, save_directory=save_directory, @@ -480,8 +482,10 @@ def exec_view_kcfg( exclude_claim_labels=exclude_claim_labels, ) - viewer = APRProofViewer(apr_proof, kevm, node_printer=KEVMNodePrinter(kevm)) - viewer.run() + node_printer = kevm_node_printer(kevm, proof) + proof_view = APRProofViewer(proof, kevm, node_printer=node_printer) + + proof_view.run() def exec_foundry_prove( @@ -629,11 +633,11 @@ def exec_run( def exec_foundry_view_kcfg(foundry_root: Path, test: str, **kwargs: Any) -> None: foundry = Foundry(foundry_root) - apr_proofs_dir = foundry.out / 'apr_proofs' + proofs_dir = foundry.out / 'apr_proofs' contract_name, test_name = test.split('.') proof_digest = foundry.proof_digest(contract_name, test_name) - apr_proof = APRProof.read_proof(proof_digest, apr_proofs_dir) + proof = APRProof.read_proof(proof_digest, proofs_dir) def _short_info(cterm: CTerm) -> Iterable[str]: return foundry.short_info_for_contract(contract_name, cterm) @@ -641,9 +645,8 @@ def _short_info(cterm: CTerm) -> Iterable[str]: def _custom_view(elem: KCFGElem) -> Iterable[str]: return foundry.custom_view(contract_name, elem) - viewer = APRProofViewer( - apr_proof, foundry.kevm, node_printer=FoundryNodePrinter(foundry, contract_name), custom_view=_custom_view - ) + node_printer = foundry_node_printer(foundry, contract_name, proof) + viewer = APRProofViewer(proof, foundry.kevm, node_printer=node_printer, custom_view=_custom_view) viewer.run() diff --git a/kevm-pyk/src/kevm_pyk/foundry.py b/kevm-pyk/src/kevm_pyk/foundry.py index a5f12428a7..cf6db2b13a 100644 --- a/kevm-pyk/src/kevm_pyk/foundry.py +++ b/kevm-pyk/src/kevm_pyk/foundry.py @@ -24,7 +24,7 @@ from pyk.prelude.ml import mlEqualsTrue from pyk.proof.proof import Proof from pyk.proof.reachability import APRBMCProof, APRProof -from pyk.proof.show import APRProofShow +from pyk.proof.show import APRBMCProofNodePrinter, APRProofNodePrinter, APRProofShow from pyk.utils import BugReport, ensure_dir_path, hash_str, run_process, single, unique from .kevm import KEVM, KEVMNodePrinter @@ -46,6 +46,7 @@ from pyk.kast import KInner from pyk.kcfg.kcfg import NodeIdLike from pyk.kcfg.tui import KCFGElem + from pyk.proof.show import NodePrinter _LOGGER: Final = logging.getLogger(__name__) @@ -623,7 +624,9 @@ def _short_info(cterm: CTerm) -> Iterable[str]: '', ] - proof_show = APRProofShow(foundry.kevm, node_printer=FoundryNodePrinter(foundry, contract_name)) + node_printer = foundry_node_printer(foundry, contract_name, proof) + proof_show = APRProofShow(foundry.kevm, node_printer=node_printer) + res_lines = proof_show.show( proof, nodes=nodes, @@ -644,13 +647,16 @@ def _short_info(cterm: CTerm) -> Iterable[str]: def foundry_to_dot(foundry_root: Path, test: str) -> None: foundry = Foundry(foundry_root) - apr_proofs_dir = foundry.out / 'apr_proofs' - dump_dir = apr_proofs_dir / 'dump' + proofs_dir = foundry.out / 'apr_proofs' + dump_dir = proofs_dir / 'dump' contract_name, test_name = test.split('.') proof_digest = foundry.proof_digest(contract_name, test_name) - apr_proof = APRProof.read_proof(proof_digest, apr_proofs_dir) - proof_show = APRProofShow(foundry.kevm, node_printer=FoundryNodePrinter(foundry, contract_name)) - proof_show.dump(apr_proof, dump_dir, dot=True) + proof = APRProof.read_proof(proof_digest, proofs_dir) + + node_printer = foundry_node_printer(foundry, contract_name, proof) + proof_show = APRProofShow(foundry.kevm, node_printer=node_printer) + + proof_show.dump(proof, dump_dir, dot=True) def foundry_list(foundry_root: Path) -> list[str]: @@ -1092,7 +1098,7 @@ class FoundryNodePrinter(KEVMNodePrinter): contract_name: str def __init__(self, foundry: Foundry, contract_name: str): - super().__init__(foundry.kevm) + KEVMNodePrinter.__init__(self, foundry.kevm) self.foundry = foundry self.contract_name = contract_name @@ -1105,3 +1111,23 @@ def print_node(self, kcfg: KCFG, node: KCFG.Node) -> list[str]: path, start, end = srcmap_data ret_strs.append(f'src: {str(path)}:{start}:{end}') return ret_strs + + +class FoundryAPRNodePrinter(FoundryNodePrinter, APRProofNodePrinter): + def __init__(self, foundry: Foundry, contract_name: str, proof: APRProof): + FoundryNodePrinter.__init__(self, foundry, contract_name) + APRProofNodePrinter.__init__(self, proof, foundry.kevm) + + +class FoundryAPRBMCNodePrinter(FoundryNodePrinter, APRBMCProofNodePrinter): + def __init__(self, foundry: Foundry, contract_name: str, proof: APRBMCProof): + FoundryNodePrinter.__init__(self, foundry, contract_name) + APRBMCProofNodePrinter.__init__(self, proof, foundry.kevm) + + +def foundry_node_printer(foundry: Foundry, contract_name: str, proof: APRProof) -> NodePrinter: + if type(proof) is APRBMCProof: + return FoundryAPRBMCNodePrinter(foundry, contract_name, proof) + if type(proof) is APRProof: + return FoundryAPRNodePrinter(foundry, contract_name, proof) + raise ValueError(f'Cannot build NodePrinter for proof type: {type(proof)}') diff --git a/kevm-pyk/src/kevm_pyk/kevm.py b/kevm-pyk/src/kevm_pyk/kevm.py index a7711a7abe..37fd88754f 100644 --- a/kevm-pyk/src/kevm_pyk/kevm.py +++ b/kevm-pyk/src/kevm_pyk/kevm.py @@ -14,6 +14,8 @@ from pyk.prelude.kint import intToken, ltInt from pyk.prelude.ml import mlEqualsTrue from pyk.prelude.string import stringToken +from pyk.proof.reachability import APRBMCProof, APRProof +from pyk.proof.show import APRBMCProofNodePrinter, APRProofNodePrinter if TYPE_CHECKING: from collections.abc import Iterable @@ -393,10 +395,30 @@ class KEVMNodePrinter(NodePrinter): kevm: KEVM def __init__(self, kevm: KEVM): - super().__init__(kevm) + NodePrinter.__init__(self, kevm) self.kevm = kevm def print_node(self, kcfg: KCFG, node: KCFG.Node) -> list[str]: ret_strs = super().print_node(kcfg, node) ret_strs += self.kevm.short_info(node.cterm) return ret_strs + + +class KEVMAPRNodePrinter(KEVMNodePrinter, APRProofNodePrinter): + def __init__(self, kevm: KEVM, proof: APRProof): + KEVMNodePrinter.__init__(self, kevm) + APRProofNodePrinter.__init__(self, proof, kevm) + + +class KEVMAPRBMCNodePrinter(KEVMNodePrinter, APRBMCProofNodePrinter): + def __init__(self, kevm: KEVM, proof: APRBMCProof): + KEVMNodePrinter.__init__(self, kevm) + APRBMCProofNodePrinter.__init__(self, proof, kevm) + + +def kevm_node_printer(kevm: KEVM, proof: APRProof) -> NodePrinter: + if type(proof) is APRBMCProof: + return KEVMAPRBMCNodePrinter(kevm, proof) + if type(proof) is APRProof: + return KEVMAPRNodePrinter(kevm, proof) + raise ValueError(f'Cannot build NodePrinter for proof type: {type(proof)}') diff --git a/kevm-pyk/src/tests/integration/test-data/contracts.k.expected b/kevm-pyk/src/tests/integration/test-data/contracts.k.expected index 13cc7901af..df4bcba21f 100644 --- a/kevm-pyk/src/tests/integration/test-data/contracts.k.expected +++ b/kevm-pyk/src/tests/integration/test-data/contracts.k.expected @@ -862,6 +862,8 @@ module BMCLOOPSTEST-CONTRACT syntax BMCLoopsTestMethod ::= "failed" "(" ")" [symbol(), klabel(method_BMCLoopsTest_failed_)] + syntax BMCLoopsTestMethod ::= "test_bmc" "(" Int ":" "uint256" ")" [symbol(), klabel(method_BMCLoopsTest_test_bmc_uint256)] + syntax BMCLoopsTestMethod ::= "test_countdown_concrete" "(" ")" [symbol(), klabel(method_BMCLoopsTest_test_countdown_concrete_)] syntax BMCLoopsTestMethod ::= "test_countdown_symbolic" "(" Int ":" "uint256" ")" [symbol(), klabel(method_BMCLoopsTest_test_countdown_symbolic_uint256)] @@ -877,6 +879,10 @@ module BMCLOOPSTEST-CONTRACT rule ( BMCLoopsTest . failed ( ) => #abiCallData ( "failed" , .TypedArgs ) ) + rule ( BMCLoopsTest . test_bmc ( V0_n : uint256 ) => #abiCallData ( "test_bmc" , #uint256 ( V0_n ) , .TypedArgs ) ) + ensures #rangeUInt ( 256 , V0_n ) + + rule ( BMCLoopsTest . test_countdown_concrete ( ) => #abiCallData ( "test_countdown_concrete" , .TypedArgs ) ) @@ -896,6 +902,9 @@ module BMCLOOPSTEST-CONTRACT rule ( selector ( "failed()" ) => 3124842406 ) + rule ( selector ( "test_bmc(uint256)" ) => 2531276689 ) + + rule ( selector ( "test_countdown_concrete()" ) => 1189516988 ) diff --git a/kevm-pyk/src/tests/integration/test-data/foundry/test/BMCLoops.t.sol b/kevm-pyk/src/tests/integration/test-data/foundry/test/BMCLoops.t.sol index f97e41ff9f..70c89b8528 100644 --- a/kevm-pyk/src/tests/integration/test-data/foundry/test/BMCLoops.t.sol +++ b/kevm-pyk/src/tests/integration/test-data/foundry/test/BMCLoops.t.sol @@ -20,4 +20,12 @@ contract BMCLoopsTest is Test { } assert(n == 0); } + + function test_bmc(uint256 n) public { + uint256 x = 0; + for (uint256 i = 0; i < n; ++i) { + x += 1; + } + assertEq(x, n); + } } diff --git a/kevm-pyk/src/tests/integration/test-data/show/AssertTest.testFail_assert_false.expected b/kevm-pyk/src/tests/integration/test-data/show/AssertTest.testFail_assert_false.expected index 839c4ee907..5d6f6ee9f0 100644 --- a/kevm-pyk/src/tests/integration/test-data/show/AssertTest.testFail_assert_false.expected +++ b/kevm-pyk/src/tests/integration/test-data/show/AssertTest.testFail_assert_false.expected @@ -37,7 +37,7 @@ -module SUMMARY-ASSERTTEST.TESTFAIL-ASSERT-FALSE:2A3527C34E566A9F170452CD78ECD8B40FA4041EBAB206050F339275402306E0 +module SUMMARY-ASSERTTEST.TESTFAIL-ASSERT-FALSE:D9767505A49B578A77DD3E9B8A9FE01EAFE474E8A6AA79E26F018CC5DA6F799A rule [BASIC-BLOCK-1-TO-3]: diff --git a/kevm-pyk/src/tests/integration/test-data/show/AssertTest.testFail_assert_true.expected b/kevm-pyk/src/tests/integration/test-data/show/AssertTest.testFail_assert_true.expected index 2d1f8be447..948f5f0ffe 100644 --- a/kevm-pyk/src/tests/integration/test-data/show/AssertTest.testFail_assert_true.expected +++ b/kevm-pyk/src/tests/integration/test-data/show/AssertTest.testFail_assert_true.expected @@ -20,7 +20,7 @@ │ statusCode: EVMC_SUCCESS │ │ (2 steps) -└─ 5 (leaf) +└─ 5 (leaf, terminal) k: #halt ~> CONTINUATION:K pc: 213 callDepth: 0 @@ -241,7 +241,7 @@ Node 5: -module SUMMARY-ASSERTTEST.TESTFAIL-ASSERT-TRUE:5DDA90333A0F7F4C47CCBF2CF8C9EA5168661E8EFAE31E01F4E7535CEBDD5E2A +module SUMMARY-ASSERTTEST.TESTFAIL-ASSERT-TRUE:B64469810687DD4D52CB523504A17EF06BC096E85D850767931F8B92A7CB4CD2 rule [BASIC-BLOCK-1-TO-3]: diff --git a/kevm-pyk/src/tests/integration/test-data/show/AssertTest.testFail_expect_revert.expected b/kevm-pyk/src/tests/integration/test-data/show/AssertTest.testFail_expect_revert.expected index 3a6086c7a3..c2aba5a654 100644 --- a/kevm-pyk/src/tests/integration/test-data/show/AssertTest.testFail_expect_revert.expected +++ b/kevm-pyk/src/tests/integration/test-data/show/AssertTest.testFail_expect_revert.expected @@ -34,7 +34,7 @@ │ statusCode: EVMC_REVERT │ │ (5 steps) -└─ 7 (leaf) +└─ 7 (leaf, terminal) k: #halt ~> CONTINUATION:K pc: 992 callDepth: 0 @@ -263,7 +263,7 @@ Node 7: -module SUMMARY-ASSERTTEST.TESTFAIL-EXPECT-REVERT:544A7CD7EC24BD75539E5995E7BA8DAD8C49229C42024AE5A37FC7A300FDB8C6 +module SUMMARY-ASSERTTEST.TESTFAIL-EXPECT-REVERT:C06C5EA6446D70FBDD360FECAB0A1147918BDDEF043645F28130D54891127053 rule [BASIC-BLOCK-1-TO-3]: diff --git a/kevm-pyk/src/tests/integration/test-data/show/AssertTest.test_assert_false.expected b/kevm-pyk/src/tests/integration/test-data/show/AssertTest.test_assert_false.expected index 6325c61e9e..8e463c83e4 100644 --- a/kevm-pyk/src/tests/integration/test-data/show/AssertTest.test_assert_false.expected +++ b/kevm-pyk/src/tests/integration/test-data/show/AssertTest.test_assert_false.expected @@ -20,7 +20,7 @@ │ statusCode: EVMC_REVERT │ │ (2 steps) -└─ 5 (leaf) +└─ 5 (leaf, terminal) k: #halt ~> CONTINUATION:K pc: 992 callDepth: 0 @@ -241,7 +241,7 @@ Node 5: -module SUMMARY-ASSERTTEST.TEST-ASSERT-FALSE:ECCEE15056474B7F502FE275CD66FA785BDCF0201A2E45F20541204B52B78F69 +module SUMMARY-ASSERTTEST.TEST-ASSERT-FALSE:08F836935DBCC810AE1CEBB9276F3B79DE040475AFCDA8C9DC5D47AA2E65AB2C rule [BASIC-BLOCK-1-TO-3]: diff --git a/kevm-pyk/src/tests/integration/test-data/show/AssertTest.test_assert_true.expected b/kevm-pyk/src/tests/integration/test-data/show/AssertTest.test_assert_true.expected index 34ce6295f3..1867d8adf0 100644 --- a/kevm-pyk/src/tests/integration/test-data/show/AssertTest.test_assert_true.expected +++ b/kevm-pyk/src/tests/integration/test-data/show/AssertTest.test_assert_true.expected @@ -37,7 +37,7 @@ -module SUMMARY-ASSERTTEST.TEST-ASSERT-TRUE:ED7C70C8FF6A057076CEBCAC150C6D41D6A815B024C1E7A3390E1416A302BA35 +module SUMMARY-ASSERTTEST.TEST-ASSERT-TRUE:E200EADD2408C03C6CCDB315095224AC1D58DF84031A945BF166ABAB4AE2A531 rule [BASIC-BLOCK-1-TO-3]: diff --git a/kevm-pyk/src/tests/integration/test-data/show/AssertTest.test_failing_branch.expected b/kevm-pyk/src/tests/integration/test-data/show/AssertTest.test_failing_branch.expected index 7c222d4662..faafd7ee7e 100644 --- a/kevm-pyk/src/tests/integration/test-data/show/AssertTest.test_failing_branch.expected +++ b/kevm-pyk/src/tests/integration/test-data/show/AssertTest.test_failing_branch.expected @@ -73,7 +73,7 @@ │ statusCode: EVMC_REVERT │ │ (2 steps) - └─ 11 (leaf) + └─ 11 (leaf, terminal) k: #halt ~> CONTINUATION:K pc: 992 callDepth: 0 @@ -291,7 +291,7 @@ Node 11: -module SUMMARY-ASSERTTEST.TEST-FAILING-BRANCH:D64D5EC416625C695FDA65AECE2A7D12DFC18C28905CDE381B286CB7B8A2571D +module SUMMARY-ASSERTTEST.TEST-FAILING-BRANCH:C60CB1C30ED782C5B61A621FCA10BE831A7CC1ECB96FE691F94F331F484FD273 rule [BASIC-BLOCK-1-TO-3]: diff --git a/kevm-pyk/src/tests/integration/test-data/show/AssertTest.test_revert_branch.expected b/kevm-pyk/src/tests/integration/test-data/show/AssertTest.test_revert_branch.expected index b7c5a87df5..ca30f4a7fb 100644 --- a/kevm-pyk/src/tests/integration/test-data/show/AssertTest.test_revert_branch.expected +++ b/kevm-pyk/src/tests/integration/test-data/show/AssertTest.test_revert_branch.expected @@ -36,7 +36,7 @@ ┃ │ statusCode: EVMC_REVERT ┃ │ ┃ │ (2 steps) -┃ └─ 10 (leaf) +┃ └─ 10 (leaf, terminal) ┃ k: #halt ~> CONTINUATION:K ┃ pc: 992 ┃ callDepth: 0 @@ -293,7 +293,7 @@ Node 10: -module SUMMARY-ASSERTTEST.TEST-REVERT-BRANCH:6FFE05225C2677A93E50834ED1E0DA7AEEBA5E533F9CB61BBDCEA13E9E7DBB75 +module SUMMARY-ASSERTTEST.TEST-REVERT-BRANCH:794968430243366DC0B838DD3DC47D2AD99E08CBBD3C2B29529697015104F332 rule [BASIC-BLOCK-1-TO-3]: diff --git a/kevm-pyk/src/tests/integration/test-data/show/AssumeTest.testFail_assume_false.expected b/kevm-pyk/src/tests/integration/test-data/show/AssumeTest.testFail_assume_false.expected index 5778e2b7eb..cb66ed4227 100644 --- a/kevm-pyk/src/tests/integration/test-data/show/AssumeTest.testFail_assume_false.expected +++ b/kevm-pyk/src/tests/integration/test-data/show/AssumeTest.testFail_assume_false.expected @@ -34,7 +34,7 @@ │ statusCode: EVMC_SUCCESS │ │ (2 steps) -└─ 7 (leaf) +└─ 7 (leaf, terminal) k: #halt ~> CONTINUATION:K pc: 183 callDepth: 0 diff --git a/kevm-pyk/src/tests/integration/test-data/show/AssumeTest.test_assume_false.expected b/kevm-pyk/src/tests/integration/test-data/show/AssumeTest.test_assume_false.expected index be312548f0..ca1cc54398 100644 --- a/kevm-pyk/src/tests/integration/test-data/show/AssumeTest.test_assume_false.expected +++ b/kevm-pyk/src/tests/integration/test-data/show/AssumeTest.test_assume_false.expected @@ -62,7 +62,7 @@ │ statusCode: EVMC_SUCCESS │ │ (2 steps) -└─ 11 (leaf) +└─ 11 (leaf, terminal) k: #halt ~> CONTINUATION:K pc: 183 callDepth: 0 diff --git a/kevm-pyk/src/tests/integration/test-data/show/LoopsTest.sum_N.expected b/kevm-pyk/src/tests/integration/test-data/show/LoopsTest.sum_N.expected index 1e0a9c73bc..d366daae8b 100644 --- a/kevm-pyk/src/tests/integration/test-data/show/LoopsTest.sum_N.expected +++ b/kevm-pyk/src/tests/integration/test-data/show/LoopsTest.sum_N.expected @@ -104,7 +104,7 @@ -module SUMMARY-LOOPSTEST.SUM-N:9AB5598CDC14FE56910D2D8F0BF923F62A3151DDDBB71424C6C3C2029CDEFBAC +module SUMMARY-LOOPSTEST.SUM-N:062CC914DAA13A8EAF189DADDC9178CE923938A59F8855C3A0DE5EB7260670A7 rule [BASIC-BLOCK-1-TO-3]: diff --git a/kevm-pyk/src/tests/integration/test-data/show/SetUpDeployTest.test_extcodesize.expected b/kevm-pyk/src/tests/integration/test-data/show/SetUpDeployTest.test_extcodesize.expected index 58717b4287..622dd94cdd 100644 --- a/kevm-pyk/src/tests/integration/test-data/show/SetUpDeployTest.test_extcodesize.expected +++ b/kevm-pyk/src/tests/integration/test-data/show/SetUpDeployTest.test_extcodesize.expected @@ -37,7 +37,7 @@ -module SUMMARY-SETUPDEPLOYTEST.TEST-EXTCODESIZE:883A7D4D9F2D676FC173461729F19F46CBB27F41F2B65126CEB8C0E98FB04F0D +module SUMMARY-SETUPDEPLOYTEST.TEST-EXTCODESIZE:F212E6B5B768844563A8F6DD11A901624CB91DFB16BE406C2E472F1B39DA0237 rule [BASIC-BLOCK-1-TO-3]: diff --git a/package/debian/changelog b/package/debian/changelog index 9ef644d6fd..0fd8d235c1 100644 --- a/package/debian/changelog +++ b/package/debian/changelog @@ -1,4 +1,4 @@ -kevm (1.0.223) unstable; urgency=medium +kevm (1.0.224) unstable; urgency=medium * Initial Release. diff --git a/package/version b/package/version index 1237070e7d..ddcbc71752 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.223 +1.0.224 diff --git a/tests/foundry/bmc-tests b/tests/foundry/bmc-tests index c3496d0dd2..dd2dca691f 100644 --- a/tests/foundry/bmc-tests +++ b/tests/foundry/bmc-tests @@ -1,2 +1,3 @@ +BMCLoopsTest.test_bmc BMCLoopsTest.test_countdown_concrete BMCLoopsTest.test_countdown_symbolic diff --git a/tests/foundry/test/BMCLoops.t.sol b/tests/foundry/test/BMCLoops.t.sol index f97e41ff9f..70c89b8528 100644 --- a/tests/foundry/test/BMCLoops.t.sol +++ b/tests/foundry/test/BMCLoops.t.sol @@ -20,4 +20,12 @@ contract BMCLoopsTest is Test { } assert(n == 0); } + + function test_bmc(uint256 n) public { + uint256 x = 0; + for (uint256 i = 0; i < n; ++i) { + x += 1; + } + assertEq(x, n); + } }