diff --git a/docs/conf.py b/docs/conf.py index f038ad53f18..98f0c776ffd 100644 --- a/docs/conf.py +++ b/docs/conf.py @@ -9,8 +9,8 @@ project = 'pyk' author = 'Runtime Verification, Inc' copyright = '2024, Runtime Verification, Inc' -version = '0.1.615' -release = '0.1.615' +version = '0.1.616' +release = '0.1.616' # -- General configuration --------------------------------------------------- # https://www.sphinx-doc.org/en/master/usage/configuration.html#general-configuration diff --git a/package/version b/package/version index cd9d220d6e3..c0e9cbfae1a 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.615 +0.1.616 diff --git a/pyproject.toml b/pyproject.toml index 72b229da429..21e3c6d05cd 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.615" +version = "0.1.616" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/src/pyk/ktool/kprove.py b/src/pyk/ktool/kprove.py index 56009b3d8ea..8ab3b468886 100644 --- a/src/pyk/ktool/kprove.py +++ b/src/pyk/ktool/kprove.py @@ -364,10 +364,7 @@ def _get_claim_module(_label: str) -> str | None: return None all_claims = { - claim.label: (claim, _get_claim_module(claim.label)) - for module in flat_module_list.modules - for claim in module.claims - if _get_claim_module(claim.label) is not None + claim.label: (claim, module.name) for module in flat_module_list.modules for claim in module.claims } claim_labels = list(all_claims.keys()) if claim_labels is None else list(claim_labels) diff --git a/src/tests/integration/k-files/multi-claim-spec.k b/src/tests/integration/k-files/multi-claim-spec.k index 3f6f56e346b..2967dc7c01e 100644 --- a/src/tests/integration/k-files/multi-claim-spec.k +++ b/src/tests/integration/k-files/multi-claim-spec.k @@ -26,15 +26,19 @@ module MULTI-CLAIM-SPEC claim a => b + claim a => c + claim [dep]: c => a claim [main.1]: a => c [depends(dep,MULTI-CLAIM-SPEC-DEPENDENCY-1.dep-1.1)] - claim [main.2]: a => c [depends(dep,MULTI-CLAIM-SPEC-DEPENDENCY-1.dep-1.2)] - claim [main.3]: a => c [depends(MULTI-CLAIM-SPEC.dep)] - claim [main.4]: a => c [depends(dep-1.2)] - claim [rep-dep]: c => b endmodule + +module MULTI-CLAIM-BROKEN-SPEC + imports MULTI-CLAIM-SPEC + + claim [bad-dep]: a => b [depends(non-existent-1)] +endmodule diff --git a/src/tests/integration/kprove/test_get_claims.py b/src/tests/integration/kprove/test_get_claims.py index dae2dfb92f6..f40dd244259 100644 --- a/src/tests/integration/kprove/test_get_claims.py +++ b/src/tests/integration/kprove/test_get_claims.py @@ -95,3 +95,11 @@ def test_get_claims( assert set(expected_graph.keys()) == set(actual_graph.keys()) for claim_label, deps in expected_graph.items(): assert set(deps) == set(actual_graph[claim_label]) + + def test_get_claims_unlabeled(self, kprove: KProve) -> None: + claims = kprove.get_claims(self.KOMPILE_MAIN_FILE, self.SPEC_MODULE_NAME) + assert len(claims) == 10 + + def test_get_claims_broken(self, kprove: KProve) -> None: + with pytest.raises(ValueError): + kprove.get_claims(self.KOMPILE_MAIN_FILE, 'MULTI-CLAIM-BROKEN-SPEC')