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

Support multi-property SV-COMP specifications #1228

Merged

sim642 merged 5 commits into master from sv-comp-multiproperty

Nov 2, 2023

Member

sim642 commented Oct 31, 2023

Closes #1220.

sim642 added 3 commits

October 31, 2023 16:29


          Add type for SV-COMP multiproperty

4d6b570


          Remove special MemorySafety SV-COMP property, add full multiproperty …

…handling


          Fix witness determine_result for memsafety

5093b5d

sim642 added cleanup sv-comp labels

sim642 added this to the SV-COMP 2024 milestone

sim642 mentioned this pull request

Support for valid-memsafety-ub #1227

Closed

sim642 requested a review from michael-schwarz

October 31, 2023 17:01


          Deduplicate Svcomp.is_error_function

bb163a5

michael-schwarz approved these changes

View reviewed changes


          Remove unused [@@deriving ord] on SV-COMP spec

f147d9b

sim642 merged commit 417d5d3 into master

14 of 16 checks passed

sim642 deleted the sv-comp-multiproperty branch

November 2, 2023 08:06

sim642 mentioned this pull request

[new release] goblint (2.3.0) ocaml/opam-repository#24844

Merged

sim642 added a commit to sim642/opam-repository that referenced this pull request


          [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 pull request


          [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