Skip to content

Add option witness.invariant.all-locals to only print locals definitely in scope#1362

Merged
sim642 merged 3 commits intomasterfrom
issue_1361
Feb 19, 2024
Merged

Add option witness.invariant.all-locals to only print locals definitely in scope#1362
sim642 merged 3 commits intomasterfrom
issue_1361

Conversation

@michael-schwarz
Copy link
Copy Markdown
Member

Closes #1361.

@michael-schwarz michael-schwarz added feature sv-comp SV-COMP (analyses, results), witnesses labels Feb 10, 2024
@sim642 sim642 added the pr-dependency Depends or builds on another PR, which should be merged before label Feb 14, 2024
@sim642
Copy link
Copy Markdown
Member

sim642 commented Feb 14, 2024

It would be good to have tests for this, but I'll have to get #1357 ready for that.

Or a quick temporary alternative is to have a cram test just for Goblint output (not the witness itself) to test for the printed number of generated witness entries changing due to this option.

@michael-schwarz
Copy link
Copy Markdown
Member Author

Maybe this is worth merging ahead of the tests, so we can produce new witnesses for our colleagues in Freiburg to experiment with?

@sim642 sim642 added this to the v2.4.0 milestone Feb 19, 2024
@sim642 sim642 merged commit 447d5c4 into master Feb 19, 2024
@sim642 sim642 deleted the issue_1361 branch February 19, 2024 08:57
@sim642 sim642 removed the pr-dependency Depends or builds on another PR, which should be merged before label Feb 19, 2024
@sim642 sim642 mentioned this pull request Feb 19, 2024
7 tasks
@sim642 sim642 modified the milestones: v2.4.0, SV-COMP 2025 Jul 24, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

feature sv-comp SV-COMP (analyses, results), witnesses

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Witnesses: Filter invariants about variables possibly not in scope

2 participants