From 363692c5e79705cbd799e72f69a7a5620057bb7f Mon Sep 17 00:00:00 2001 From: Lisandra Date: Sat, 16 Mar 2024 12:02:07 +0000 Subject: [PATCH] Add a warning on non-test analysis w/o `foundry_success` checking (#432) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * 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 Co-authored-by: rv-jenkins Co-authored-by: Petar Maksimović --- package/version | 2 +- pyproject.toml | 2 +- src/kontrol/__init__.py | 2 +- src/kontrol/__main__.py | 6 ++++++ src/kontrol/prove.py | 1 + 5 files changed, 10 insertions(+), 3 deletions(-) diff --git a/package/version b/package/version index fd859c0f5..c6af5cc58 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.207 +0.1.208 diff --git a/pyproject.toml b/pyproject.toml index 711bdd896..4c2f7268e 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -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. ", diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py index 689327d58..54e34f0d4 100644 --- a/src/kontrol/__init__.py +++ b/src/kontrol/__init__.py @@ -5,4 +5,4 @@ if TYPE_CHECKING: from typing import Final -VERSION: Final = '0.1.207' +VERSION: Final = '0.1.208' diff --git a/src/kontrol/__main__.py b/src/kontrol/__main__.py index 3e5381b04..6b5e8441d 100644 --- a/src/kontrol/__main__.py +++ b/src/kontrol/__main__.py @@ -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()}') diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py index 8298d29b4..355136520 100644 --- a/src/kontrol/prove.py +++ b/src/kontrol/prove.py @@ -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.')