Skip to content

Conversation

@sim642
Copy link
Member

@sim642 sim642 commented May 2, 2025

Closes #1732.

@sim642 sim642 added cleanup Refactoring, clean-up sv-comp SV-COMP (analyses, results), witnesses labels May 2, 2025
@sim642 sim642 added this to the SV-COMP 2026 milestone May 2, 2025
@michael-schwarz
Copy link
Member

michael-schwarz commented May 2, 2025

|> lift arg_enabled (module WitnessConstraints.PathSensitive3)

Should this module be renamed? Its connection to witnesses is only historical at this point.
Maybe one can make an ARG folder? Then things such as ArgTools and MyARG are also removed from the witness folder.

@michael-schwarz michael-schwarz self-requested a review May 2, 2025 10:38
Copy link
Member

@michael-schwarz michael-schwarz left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Other than my comments above, this looks good to go!

@sim642
Copy link
Member Author

sim642 commented May 2, 2025

|> lift arg_enabled (module WitnessConstraints.PathSensitive3)

Should this module be renamed? It's connection to witnesses is only historical at this point. Maybe one can make an ARG folder? Then things such as ArgTools and MyARG are also removed from the witness folder.

I now moved them around and renamed this module.
I also moved ARG things around in the documentation, which I thought about at one point but then forgot, so thanks for the reminder.

@michael-schwarz michael-schwarz self-requested a review May 5, 2025 11:38
@sim642 sim642 merged commit 57c94be into master May 5, 2025
21 checks passed
@sim642 sim642 deleted the rm-graphml-witness branch May 5, 2025 14:57
sim642 added a commit to sim642/opam-repository that referenced this pull request Sep 5, 2025
CHANGES:

* Add division by zero analysis (goblint/analyzer#1764).
* Add bitfield domain (goblint/analyzer#1623).
* Add weakly-relational C-2PO pointer analysis (goblint/analyzer#1485).
* Add widening delay (goblint/analyzer#1358, goblint/analyzer#1442, goblint/analyzer#1483).
* Add narrowing of globals to top-down solver (goblint/analyzer#1636).
* Add weak dependencies to top-down solver (goblint/analyzer#1746, goblint/analyzer#1747).
* Add YAML ghost witness generation (goblint/analyzer#1394).
* Remove GraphML witness generation (goblint/analyzer#1732, goblint/analyzer#1733, goblint/analyzer#1738).
* Use C standard option for preprocessing (goblint/analyzer#1807).
* Add bash completion for array options (goblint/analyzer#1670, goblint/analyzer#1705, goblint/analyzer#1750).
* Make `malloc(0)` semantics configurable (goblint/analyzer#1418, goblint/analyzer#1777).
* Update path-sensitive analyses (goblint/analyzer#1785, goblint/analyzer#1791, goblint/analyzer#1792).
* Fix evaluation of library function arguments (goblint/analyzer#1758, goblint/analyzer#1761).
* Optimize affine equalities analysis using sparse matrices (goblint/analyzer#1459, goblint/analyzer#1625).
* Prepare for parallelism (goblint/analyzer#1708, goblint/analyzer#1744, goblint/analyzer#1748, goblint/analyzer#1781, goblint/analyzer#1790).
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.

Remove support for GraphML witnesses?

3 participants