Skip to content

Commit

Permalink
Fix _method_to_cfg (#109)
Browse files Browse the repository at this point in the history
* Copy the setup proof KCFG

* Simplify statement

* Slide statement

* Simplify statement

* Simplify statement

* Set Version: 0.1.34

* Set Version: 0.1.35

* Set Version: 0.1.36

---------

Co-authored-by: devops <devops@runtimeverification.com>
Co-authored-by: rv-jenkins <admin@runtimeverification.com>
  • Loading branch information
3 people authored Oct 24, 2023
1 parent 868b197 commit cf5e56b
Show file tree
Hide file tree
Showing 4 changed files with 11 additions and 10 deletions.
2 changes: 1 addition & 1 deletion package/version
Original file line number Diff line number Diff line change
@@ -1 +1 @@
0.1.35
0.1.36
2 changes: 1 addition & 1 deletion pyproject.toml
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"

[tool.poetry]
name = "kontrol"
version = "0.1.35"
version = "0.1.36"
description = "Foundry integration for KEVM"
authors = [
"Runtime Verification, Inc. <contact@runtimeverification.com>",
Expand Down
2 changes: 1 addition & 1 deletion src/kontrol/__init__.py
Original file line number Diff line number Diff line change
Expand Up @@ -5,4 +5,4 @@
if TYPE_CHECKING:
from typing import Final

VERSION: Final = '0.1.35'
VERSION: Final = '0.1.36'
15 changes: 8 additions & 7 deletions src/kontrol/prove.py
Original file line number Diff line number Diff line change
Expand Up @@ -364,16 +364,17 @@ def _method_to_cfg(
new_node_ids = []

if setup_proof:
init_node_id = setup_proof.kcfg.node(setup_proof.init).id

cfg = setup_proof.kcfg
final_states = [cover.source for cover in cfg.covers(target_id=setup_proof.target)]
cfg.remove_node(setup_proof.target)
if len(setup_proof.pending) > 0:
if setup_proof.pending:
raise RuntimeError(
f'Initial state proof {setup_proof.id} for {contract.name}.{method.signature} still has pending branches.'
)
if len(final_states) < 1:

init_node_id = setup_proof.init

cfg = KCFG.from_dict(setup_proof.kcfg.to_dict()) # Copy KCFG
final_states = [cover.source for cover in cfg.covers(target_id=setup_proof.target)]
cfg.remove_node(setup_proof.target)
if not final_states:
_LOGGER.warning(
f'Initial state proof {setup_proof.id} for {contract.name}.{method.signature} has no passing branches to build on. Method will not be executed.'
)
Expand Down

0 comments on commit cf5e56b

Please sign in to comment.