Skip to content

Remove YAML witness 0.1 validation certificates#1817

Merged
sim642 merged 1 commit intomasterfrom
yaml-witness-certificates
Sep 29, 2025
Merged

Remove YAML witness 0.1 validation certificates#1817
sim642 merged 1 commit intomasterfrom
yaml-witness-certificates

Conversation

@sim642
Copy link
Copy Markdown
Member

@sim642 sim642 commented Sep 4, 2025

These were part of YAML witness 0.1 as special entries produced by validators, but they were never used for anything and were removed in YAML witness 2.0 format anyway.
It's not worth keeping the support around.

@sim642 sim642 added this to the v2.7.0 Bamboozled Buffalo milestone Sep 4, 2025
@sim642 sim642 added cleanup Refactoring, clean-up sv-comp SV-COMP (analyses, results), witnesses labels Sep 4, 2025
@sim642 sim642 merged commit a8d8866 into master Sep 29, 2025
17 of 19 checks passed
@sim642 sim642 deleted the yaml-witness-certificates branch September 29, 2025 07:03
sim642 added a commit to sim642/opam-repository that referenced this pull request Nov 27, 2025
CHANGES:

Functionally equivalent to Goblint in SV-COMP 2026.

* Add sequential portfolio for SV-COMP (goblint/analyzer#1845, goblint/analyzer#1867, goblint/analyzer#1877).
* Add struct bitfield support (goblint/analyzer#1739, goblint/analyzer#1823).
* Improve bitwise operations for integer domains (goblint/analyzer#1739).
* Reimplement HTML output in OCaml (goblint/analyzer#1752).
* Remove YAML witness version 0.1 support (goblint/analyzer#1812, goblint/analyzer#1817, goblint/analyzer#1852, goblint/analyzer#1853, goblint/analyzer#1855).
* Fix incorrect invariants in witnesses (goblint/analyzer#1818, goblint/analyzer#1876).
* Simplify relational invariants in witnesses (goblint/analyzer#1826, goblint/analyzer#1871, goblint/analyzer#1873).
* Fix argument types in Goblint stubs (goblint/analyzer#1684, goblint/analyzer#1814, goblint/analyzer#1779, goblint/analyzer#1820).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

cleanup Refactoring, clean-up sv-comp SV-COMP (analyses, results), witnesses

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant