Skip to content

Conversation

sim642
Copy link
Member

@sim642 sim642 commented Jul 29, 2025

Updates CIL pin with goblint/cil#187.

TODO

@sim642 sim642 added this to the SV-COMP 2026 milestone Jul 29, 2025
@sim642 sim642 added bug sv-comp SV-COMP (analyses, results), witnesses parallel Parallel Goblint labels Jul 29, 2025
@sim642
Copy link
Member Author

sim642 commented Jul 29, 2025

@michael-schwarz It might be a good idea for you to do a sv-benchmarks run with this first to see if this is enough to fix #1781 before merging this.

@sim642 sim642 added the pr-dependency Depends or builds on another PR, which should be merged before label Jul 29, 2025
@michael-schwarz
Copy link
Member

I can do a run as soon as the multishot things are done, currently both servers are busy.

@michael-schwarz
Copy link
Member

The instances of #1781 are all gone.

@michael-schwarz michael-schwarz merged commit 44ba988 into master Jul 30, 2025
17 checks passed
@michael-schwarz michael-schwarz deleted the cil-pretty-state branch July 30, 2025 14:31
@sim642 sim642 removed the pr-dependency Depends or builds on another PR, which should be merged before label Jul 30, 2025
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

bug parallel Parallel Goblint sv-comp SV-COMP (analyses, results), witnesses

Projects

None yet

Development

Successfully merging this pull request may close these issues.

SV-COMP Errors: exception Sys_error("Mutex.lock: Resource deadlock avoided")

2 participants