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

Proper multi-property SV-COMP specification #1220

Closed
sim642 opened this issue Oct 20, 2023 · 1 comment · Fixed by #1228
Closed

Proper multi-property SV-COMP specification #1220

sim642 opened this issue Oct 20, 2023 · 1 comment · Fixed by #1228
Assignees
@sim642
Labels
cleanup sv-comp
Milestone
SV-COMP 2024

Comments

@sim642
Copy link
Member

sim642 commented Oct 20, 2023

In #1201 (and maybe something earlier as well), preliminary and hacky support for SV-COMP MemSafety was added. That category uses a specification file with multiple properties but our implementation only does one at a time. It should be cleaned up.

Since our analysis isn't property-directed anyway, we can just be very general and allow other combinations just as well.
@sim642 sim642 added this to the SV-COMP 2024 milestone Oct 20, 2023
@sim642 sim642 self-assigned this Oct 20, 2023
@sim642
Copy link
Member Author

sim642 commented Oct 31, 2023

This is blocked by the MemSafety analyses not working at all: #1201 (comment).

This was referenced Oct 31, 2023
Merged
Closed
@sim642 sim642 mentioned this issue Nov 24, 2023
Merged
sim642 added a commit to sim642/opam-repository that referenced this issue Nov 24, 2023
@sim642
[new release] goblint (2.3.0)
34ad5a7 
CHANGES:

Functionally equivalent to Goblint in SV-COMP 2024.

* Add termination analysis for loops (goblint/analyzer#1093).
* Add memory out-of-bounds analysis (goblint/analyzer#1094, goblint/analyzer#1197).
* Add memory leak analysis (goblint/analyzer#1127, goblint/analyzer#1241, goblint/analyzer#1246).
* Add SV-COMP `termination`, `valid-memsafety` and `valid-memcleanup` properties support (goblint/analyzer#1220, goblint/analyzer#1228, goblint/analyzer#1201, goblint/analyzer#1199, goblint/analyzer#1259, goblint/analyzer#1262).
* Add YAML witness version 2.0 support (goblint/analyzer#1238, goblint/analyzer#1240, goblint/analyzer#1217, goblint/analyzer#1226, goblint/analyzer#1225, goblint/analyzer#1248).
* Add final warnings about unsound results (goblint/analyzer#1190, goblint/analyzer#1191).
* Add many library function specifications (goblint/analyzer#1167, goblint/analyzer#1174, goblint/analyzer#1203, goblint/analyzer#1205, goblint/analyzer#1212, goblint/analyzer#1220, goblint/analyzer#1239, goblint/analyzer#1242, goblint/analyzer#1244, goblint/analyzer#1254, goblint/analyzer#1269).
* Adapt automatic configuration tuning (goblint/analyzer#912, goblint/analyzer#921, goblint/analyzer#987, goblint/analyzer#1168, goblint/analyzer#1214, goblint/analyzer#1234).
nberth pushed a commit to nberth/opam-repository that referenced this issue Jun 18, 2024
@sim642 @nberth
[new release] goblint (2.3.0)
8f8e773 
CHANGES:

Functionally equivalent to Goblint in SV-COMP 2024.

* Add termination analysis for loops (goblint/analyzer#1093).
* Add memory out-of-bounds analysis (goblint/analyzer#1094, goblint/analyzer#1197).
* Add memory leak analysis (goblint/analyzer#1127, goblint/analyzer#1241, goblint/analyzer#1246).
* Add SV-COMP `termination`, `valid-memsafety` and `valid-memcleanup` properties support (goblint/analyzer#1220, goblint/analyzer#1228, goblint/analyzer#1201, goblint/analyzer#1199, goblint/analyzer#1259, goblint/analyzer#1262).
* Add YAML witness version 2.0 support (goblint/analyzer#1238, goblint/analyzer#1240, goblint/analyzer#1217, goblint/analyzer#1226, goblint/analyzer#1225, goblint/analyzer#1248).
* Add final warnings about unsound results (goblint/analyzer#1190, goblint/analyzer#1191).
* Add many library function specifications (goblint/analyzer#1167, goblint/analyzer#1174, goblint/analyzer#1203, goblint/analyzer#1205, goblint/analyzer#1212, goblint/analyzer#1220, goblint/analyzer#1239, goblint/analyzer#1242, goblint/analyzer#1244, goblint/analyzer#1254, goblint/analyzer#1269).
* Adapt automatic configuration tuning (goblint/analyzer#912, goblint/analyzer#921, goblint/analyzer#987, goblint/analyzer#1168, goblint/analyzer#1214, goblint/analyzer#1234).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@sim642 sim642

Labels
cleanup sv-comp
Projects
None yet
Milestone
SV-COMP 2024
Development

Successfully merging a pull request may close this issue.

Support multi-property SV-COMP specifications goblint/analyzer
1 participant
@sim642