This repository has been archived by the owner on Apr 25, 2024. It is now read-only.
v0.1.616
ehildenb
tagged this
07 Feb 20:24
Here: https://github.com/runtimeverification/pyk/pull/842, a mistake was made where claims without labels were filtered out of the claims to be processed and returned by `KProve.get_claims`. This PR addresses that and adds tests. In particular: - Two claims in the `multi-claim-spec.k` which were ill-formed because of dependencies (but not tested for it) are removed. - An ill-formed (because of dependencies) claim is added in a separate module, and a new test added which exercises that a `ValueError` is thrown when loading this module. - A new test is added which asserts that the correct number of claims is loaded from the main module. On `master`, this test is failing because it skips claims without labels, but is fixed on this PR. - Adjustments to how claims are filtered are made, so that it's simpler and includes all claims, even ones without explicit module names in the label. --------- Co-authored-by: devops <devops@runtimeverification.com>
Assets 2
-
2024-02-07T20:24:40Z -
2024-02-07T20:24:40Z - Loading