Skip to content
This repository has been archived by the owner on Apr 25, 2024. It is now read-only.

v0.1.616

@ehildenb 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