Skip to content

Commit

Permalink
Add a warning on non-test analysis w/o foundry_success checking (#432)
Browse files Browse the repository at this point in the history
* Added warning non a non-test analysis

* Set Version: 0.1.195

* Addressed PR comments

* changed from info to warning

* Set Version: 0.1.200

* Moved warning closer to the end of execution

* Print info after proof.status

* Set Version: 0.1.201

* Moved warning before proof status

* Set Version: 0.1.204

* Set Version: 0.1.205

* Set Version: 0.1.208

---------

Co-authored-by: devops <[email protected]>
Co-authored-by: rv-jenkins <[email protected]>
Co-authored-by: Petar Maksimović <[email protected]>
  • Loading branch information
4 people authored and qian-hu committed Mar 18, 2024
1 parent 1fc1aac commit 4a54d5c
Show file tree
Hide file tree
Showing 5 changed files with 10 additions and 3 deletions.
2 changes: 1 addition & 1 deletion package/version
Original file line number Diff line number Diff line change
@@ -1 +1 @@
0.1.207
0.1.208
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.207"
version = "0.1.208"
description = "Foundry integration for KEVM"
authors = [
"Runtime Verification, Inc. <[email protected]>",
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.207'
VERSION: Final = '0.1.208'
6 changes: 6 additions & 0 deletions src/kontrol/__main__.py
Original file line number Diff line number Diff line change
Expand Up @@ -306,6 +306,12 @@ def exec_prove(
)
failed = 0
for proof in results:
_, test = proof.id.split('.')
if not any(test.startswith(prefix) for prefix in ['test', 'check', 'prove']):
signature, _ = test.split(':')
_LOGGER.warning(
f"{signature} is not prefixed with 'test', 'prove', or 'check', therefore, it is not reported as failing in the presence of reverts or assertion violations."
)
if proof.passed:
print(f'PROOF PASSED: {proof.id}')
print(f'time: {proof.formatted_exec_time()}')
Expand Down
1 change: 1 addition & 0 deletions src/kontrol/prove.py
Original file line number Diff line number Diff line change
Expand Up @@ -288,6 +288,7 @@ def init_and_run_proof(test: FoundryTest) -> APRFailureInfo | Exception | None:
end_time = time.time()
proof.add_exec_time(end_time - start_time)
proof.write_proof_data()

# Only return the failure info to avoid pickling the whole proof
if proof.failure_info is not None and not isinstance(proof.failure_info, APRFailureInfo):
raise RuntimeError('Generated failure info for APRProof is not APRFailureInfo.')
Expand Down

0 comments on commit 4a54d5c

Please sign in to comment.