Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Add kprove options to filter claims #2834

Merged
merged 4 commits into from
Aug 30, 2022
Merged

Add kprove options to filter claims #2834

merged 4 commits into from
Aug 30, 2022

Conversation

radumereuta
Copy link
Contributor

Fixes: #2812

@ehildenb
Copy link
Member

Also, can you add a test where there are 3 claims, 2 that are failing, and 1 that are passing. If you say kprove --exclude faliing1 --exclude failing2, the overall command should pass and give back #Top.

Baltoli
Baltoli suggested changes Aug 30, 2022
View reviewed changes
Copy link
Contributor

@Baltoli Baltoli left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It would be good to have explicit tests for the --trusted and --exclude flags as well as --claims. At the moment I don't think those code paths will be exercised.

@radumereuta
Copy link
Contributor Author

@Baltoli @ehildenb please check if these tests are enough.

@rv-jenkins rv-jenkins merged commit a6875a6 into master Aug 30, 2022
@rv-jenkins rv-jenkins deleted the fix2812-kprove-filter branch August 30, 2022 23:46
@ehildenb ehildenb mentioned this pull request Sep 9, 2022
Merged
@radumereuta radumereuta mentioned this pull request Sep 19, 2022
Closed
5 tasks
h0nzZik pushed a commit to h0nzZik/k that referenced this pull request Nov 24, 2022
@rv-jenkins
Update dependency: haskell-backend/src/main/native/haskell-backend (r…
25daaba 
…untimeverification#2201)

* haskell-backend/src/main/native/haskell-backend: 66e2b1d1 - Fix Cabal build for Update issue runtimeverification#2836 (runtimeverification#2838)

* haskell-backend/src/main/native/haskell-backend: 29acc44c - Add oneLineDoc implementations to all existing Entry-instances (runtimeverification#2830)

* haskell-backend/src/main/native/haskell-backend: b0e0fc62 - Update regression tests (runtimeverification#2834)

* haskell-backend/src/main/native/haskell-backend: 8bb992f0 - Update dependency: deps/k_release (runtimeverification#2836)

Co-authored-by: Erik Kaneda <erik.kaneda@runtimeverification.com>
@radumereuta radumereuta mentioned this pull request Jan 23, 2023
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@ehildenb ehildenb ehildenb approved these changes

@dwightguth dwightguth dwightguth approved these changes

@Baltoli Baltoli Baltoli approved these changes

Assignees
No one assigned
Labels
automerge
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

[kprove] Control which claims the backend discharges
5 participants
@radumereuta @ehildenb @Baltoli @dwightguth @rv-jenkins