Regression building the C semantics for the LLVM backend #866
Assignees
Comments
Baltoli
pushed a commit
that referenced
this issue
Apr 9, 2024
Here: runtimeverification/pyk#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 <[email protected]>
Baltoli
pushed a commit
that referenced
this issue
Apr 9, 2024
Here: runtimeverification/pyk#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 <[email protected]>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
See the last two commits on: kframework/c-semantics#558
Somewhere after 9bdeac2 K started not terminating when kompiling the C semantics for the LLVM backend.
The text was updated successfully, but these errors were encountered: