Support multi-property SV-COMP specifications#1228

Merged

sim642 merged 5 commits intomasterfrom

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

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

Labels

cleanup sv-comp