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

SV-COMP 2025 development #1601

Merged
merged 30 commits into from
Nov 28, 2024
Merged

SV-COMP 2025 development #1601

merged 30 commits into from
Nov 28, 2024

Conversation

sim642
Copy link
Member

@sim642 sim642 commented Oct 17, 2024 •
edited
Loading

This branch contains development and integration for SV-COMP 2025. This branch is used for creating verifier archives for preruns.

PRs

It includes some not-yet merged PRs:

  1. Remove witness exclude-vars from svcomp conf #1593
  2. Partially support imaxabs for SV-COMP #1519
  3. Add YAML invariant_set indices to widening tokens #1596

Changes

Additionally, it contains:

  1. Add more precise YAML witness generation summary. (Otherwise we just report 1 invariant_set with no details on the number of invariants in that set entry.)
  2. Add witness.yaml.strict option description.
  3. Update YAML witness validation result for refutation under new scoring schema. (It was fine to output false before, because there was no penalty, but now there is.)
  4. Fix YAML witness validate/unassume error with empty (unparsable) path. (Raised an obscure Invalid_argument exception before.)

TODO

  • Merge master in (regularly).

sim642 added 18 commits June 20, 2024 12:56
@sim642
Enable ana.float.evaluate_math_functions in svcomp24 and svcomp confs
af781ed 
This is needed for sv-benchmarks Juliet no-overflow tasks involving sqrt.
We used this at SV-COMP 2024, before the option existed.
@sim642
Add tests for imaxabs
3ff00ae
@sim642
Add hacky imaxabs support
2653e2e
@sim642
Add hacky imaxabs sqrt refine support
f9765da
@sim642
Find intmax_t for imaxabs from program
a1f0b35
@sim642
Add test for invariant_set widening tokens (issue #1299)
67f8fe9
@sim642
Add optional int indices to widening tokens
7ec6b05
@sim642
Add invariant_set index to widening token
21c000c
@sim642
Rename widening token modules
57a0447
@sim642
Improve widening token output
a281744
@sim642
Merge branch 'master' into imaxabs
85cbda6
@sim642
Revert "Add hacky imaxabs sqrt refine support"
2f5b50f 
This reverts commit f9765da.
@sim642
Add 39-signed-overflows/13-imaxabs-macos test
f7a5afa
@sim642
Unroll cast type in BaseInvariant
6283468
@sim642
Merge branch 'svcomp25-no-exclude-vars' into svcomp25-dev
3b7edf4
@sim642
Merge branch 'imaxabs' into svcomp25-dev
59f5633
@sim642
Copy svcomp confs to svcomp25
e12d6df
@sim642
Update sv-comp/archive.sh for 2025
6a97380
@sim642 sim642 added in progress sv-comp SV-COMP (analyses, results), witnesses pr-dependency Depends or builds on another PR, which should be merged before labels Oct 17, 2024
@sim642 sim642 added this to the SV-COMP 2025 milestone Oct 17, 2024
@sim642 sim642 self-assigned this Oct 17, 2024
@sim642 sim642 removed in progress pr-dependency Depends or builds on another PR, which should be merged before labels Nov 28, 2024
@sim642 sim642 marked this pull request as ready for review November 28, 2024 08:22
@sim642 sim642 merged commit 55de434 into master Nov 28, 2024
19 of 21 checks passed
@sim642 sim642 deleted the svcomp25-dev branch November 28, 2024 08:26
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees

@sim642 sim642

Labels
sv-comp SV-COMP (analyses, results), witnesses
Projects
None yet
Milestone
SV-COMP 2025
Development

Successfully merging this pull request may close these issues.
1 participant
@sim642