[new release] goblint (2.6.0)

[sim642]

Static analysis framework for C

• Project page: https://goblint.in.tum.de
• Documentation: https://goblint.readthedocs.io/en/latest/

CHANGES:

• Add division by zero analysis (Division by zero messages goblint/analyzer#1764).
• Add bitfield domain (Bitfield Domain goblint/analyzer#1623).
• Add weakly-relational C-2PO pointer analysis (C-2PO: Thesis About a Weakly-Relational Pointer Analysis goblint/analyzer#1485).
• Add widening delay (Solver TD3-💨 with Side-Effect Gas goblint/analyzer#1358, Widening gas goblint/analyzer#1442, Implement delayed widening goblint/analyzer#1483).
• Add narrowing of globals to top-down solver (Narrowing of globals in TD goblint/analyzer#1636).
• Add weak dependencies to top-down solver (Introduce demand in constraint system goblint/analyzer#1746, Add weak dependencies to TD3 (rebased) goblint/analyzer#1747).
• Add YAML ghost witness generation (Generate flow-insensitive YAML witness invariants with ghosts for privatized variables goblint/analyzer#1394).
• Remove GraphML witness generation (Remove support for GraphML witnesses? goblint/analyzer#1732, Disable graphml witnesses in svcomp.json goblint/analyzer#1733, Remove GraphML witness export goblint/analyzer#1738).
• Use C standard option for preprocessing (Use C standard option also for preprocessing goblint/analyzer#1807).
• Add bash completion for array options (Update bash-completion for arg-complete 0.2.x, remove Arg_complete.Rest_all_compat goblint/analyzer#1670, Add bash completion for array element addition and removal goblint/analyzer#1705, Fix bash completion for booleans goblint/analyzer#1750).
• Make malloc(0) semantics configurable (Unsoundness for malloc(0) goblint/analyzer#1418, Consider option that malloc(0) may return NULL goblint/analyzer#1777).
• Update path-sensitive analyses (Turn malloc_null into an analysis serving as path-sens hint only & Fix enter goblint/analyzer#1785, Allow for path-sensitive base analysis goblint/analyzer#1791, BranchSet analysis tracking set of taken branches goblint/analyzer#1792).
• Fix evaluation of library function arguments (Printf arguments are not evaluated goblint/analyzer#1758, Fix for #1758 goblint/analyzer#1761).
• Optimize affine equalities analysis using sparse matrices (Affine Equalities Mostly Contain Only Small Portions of Actual Information goblint/analyzer#1459, Sparsification of Affine Equality Matrix  goblint/analyzer#1625).
• Prepare for parallelism (Introduce backwards compatible infrastructure for parallelism goblint/analyzer#1708, Remove some usages of MyCFG.current_node goblint/analyzer#1744, Parallelism: Add data utils goblint/analyzer#1748, SV-COMP Errors: exception Sys_error("Mutex.lock: Resource deadlock avoided") goblint/analyzer#1781, Pin CIL with global state removed from Pretty goblint/analyzer#1790).

[sim642]

The failures on archlinux and fedora-42 are due to newer GCC by default nowadays, as in #28433 (comment).
I hoped to have the fix for goblint 2.6.0, but that doesn't seem to cover everything yet.

[shonfeder]

Thanks for the updates and the CI analysis!