Load claims using ClaimLoader (#2532)

* Replace calls to `KProve.get_claims` by `ClaimLoader.load_claims` * Set Version: 1.0.649 * Set Version: 1.0.650 * Set Version: 1.0.652 * Set Version: 1.0.655 * Set Version: 1.0.659 * Set Version: 1.0.660 * Set Version: 1.0.661 --------- Co-authored-by: devops <[email protected]> Co-authored-by: Andrei Văcaru <[email protected]> Co-authored-by: Everett Hildenbrandt <[email protected]>
runtimeverification · Jul 31, 2024 · d7f2081 · d7f2081
1 parent c325c55
commit d7f2081
Show file tree

Hide file tree

Showing 5 changed files with 9 additions and 7 deletions.
diff --git 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.660"
+version = "1.0.661"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py
@@ -5,4 +5,4 @@
 if TYPE_CHECKING:
     from typing import Final
 
-VERSION: Final = '1.0.660'
+VERSION: Final = '1.0.661'
diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py
@@ -23,6 +23,7 @@
 from pyk.kdist import kdist
 from pyk.kore.rpc import KoreClient
 from pyk.kore.tools import kore_print
+from pyk.ktool.claim_loader import ClaimLoader
 from pyk.ktool.kompile import LLVMKompileType
 from pyk.proof import APRProof
 from pyk.proof.implies import EqualityProof
@@ -250,7 +251,7 @@ def is_functional(claim: KClaim) -> bool:
     llvm_definition_dir = definition_dir / 'llvm-library' if (options.use_booster or options.use_booster_dev) else None
 
     _LOGGER.info(f'Extracting claims from file: {options.spec_file}')
-    all_claims = kevm.get_claims(
+    all_claims = ClaimLoader(kevm).load_claims(
         options.spec_file,
         spec_module_name=options.spec_module,
         include_dirs=include_dirs,
@@ -411,7 +412,7 @@ def exec_prune(options: PruneOptions) -> None:
 
     _LOGGER.info(f'Extracting claims from file: {options.spec_file}')
     claim = single(
-        kevm.get_claims(
+        ClaimLoader(kevm).load_claims(
             options.spec_file,
             spec_module_name=options.spec_module,
             include_dirs=include_dirs,
@@ -459,7 +460,7 @@ def exec_section_edge(options: SectionEdgeOptions) -> None:
     include_dirs += config.INCLUDE_DIRS
 
     claim = single(
-        kevm.get_claims(
+        ClaimLoader(kevm).load_claims(
             options.spec_file,
             spec_module_name=options.spec_module,
             include_dirs=include_dirs,

diff --git a/kevm-pyk/src/kevm_pyk/utils.py b/kevm-pyk/src/kevm_pyk/utils.py
@@ -19,6 +19,7 @@
 from pyk.kcfg import KCFGExplore
 from pyk.kore.rpc import KoreClient, KoreExecLogFormat, TransportType, kore_server
 from pyk.ktool import TypeInferenceMode
+from pyk.ktool.claim_loader import ClaimLoader
 from pyk.prelude.ml import is_bottom, is_top
 from pyk.proof import APRProof, APRProver
 from pyk.proof.implies import EqualityProof, ImpliesProver
@@ -80,7 +81,7 @@ def get_apr_proof_for_spec(
 
     _LOGGER.info(f'Extracting claim from file: {spec_file}')
     claim = single(
-        kprove.get_claims(
+        ClaimLoader(kprove).load_claims(
             spec_file,
             spec_module_name=spec_module_name,
             include_dirs=include_dirs,

diff --git a/package/version b/package/version
@@ -1 +1 @@
-1.0.660
+1.0.661