[new release] goblint (2.3.0)

[sim642]

Static analysis framework for C

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

CHANGES:

Functionally equivalent to Goblint in SV-COMP 2024.

• Add termination analysis for loops (TUM Practical Course Summer 2023: Termination Analyses goblint/analyzer#1093).
• Add memory out-of-bounds analysis (Memory Out-Of-Bounds Access Analysis goblint/analyzer#1094, Add out-of-bounds check for memset and memcpy goblint/analyzer#1197).
• Add memory leak analysis (Memory Leak Analysis goblint/analyzer#1127, Account for allocated heap memory which is unreachable from globals goblint/analyzer#1241, Improve multi-threaded valid-memcleanup goblint/analyzer#1246).
• Add SV-COMP termination, valid-memsafety and valid-memcleanup properties support (Proper multi-property SV-COMP specification goblint/analyzer#1220, Support multi-property SV-COMP specifications goblint/analyzer#1228, SV-COMP "Memory Safety" benchmark additions goblint/analyzer#1201, SV-Comp: Fix unsoundness in MemSafety category caused by limitations due to scope goblint/analyzer#1199, MemSafety Low-Hanging Fruit goblint/analyzer#1259, Fix BlobSize for calloc goblint/analyzer#1262).
• Add YAML witness version 2.0 support (YAML witness entry type invariant_set goblint/analyzer#1238, Add support for YAML witness entry type invariant_set goblint/analyzer#1240, Integrate YAML witnesses with SV-COMP mode goblint/analyzer#1217, Refactor GraphML witness options goblint/analyzer#1226, Witness invariants for unrolled loops are incorrect goblint/analyzer#1225, Fix YAML witness invariants for unrolled loops goblint/analyzer#1248).
• Add final warnings about unsound results (Final errors about unsound results goblint/analyzer#1190, Add final messages about unsound results goblint/analyzer#1191).
• Add many library function specifications (Add zlib and liblzma functions used in The Silver Searcher to LibraryFunctions goblint/analyzer#1167, Add and fix library functions for Concrat benchmarks goblint/analyzer#1174, Some ~15 more library functions goblint/analyzer#1203, Add some library functions for zstd goblint/analyzer#1205, Add missing library functions for large Concrat benchmarks goblint/analyzer#1212, Proper multi-property SV-COMP specification goblint/analyzer#1220, Calls to unknown functions in SV-COMP goblint/analyzer#1239, Add some library functions from SV-COMP goblint/analyzer#1242, Low-Hanging Fruits in SV-COMP No-Overflow: CWE190-*-square*.i goblint/analyzer#1244, Handle sqrt & Some Bodged Solution for computing through abs goblint/analyzer#1254, Add unknown functions from SV-COMP goblint/analyzer#1269).
• Adapt automatic configuration tuning (Enable constant loop unrolling for small files goblint/analyzer#912, Autotuner: Do not activate Apron for val variables from Goblint header for __VERIFIER_nondet_* goblint/analyzer#921, Autotuner: Do not activate Apron for val variables from Goblint header for __VERIFIER_nondet_* goblint/analyzer#987, Re-evaluate defaults for ana.malloc.unique_address_count in SV-Comp goblint/analyzer#1168, Enable a path-sensitive memory leak analysis in autoTune for small programs goblint/analyzer#1214, Experiment with path- and context-sensitivity for memLeak analysis goblint/analyzer#1234).

[sim642]

CI failures:

1. freebsd:

   #=== ERROR while compiling conf-ruby.1.0.0 ====================================#
   "ruby": command not found.
   

   I guess conf-ruby doesn't have a depext for FreeBSD.

2. macos-homebrew: (from goblint-cil)

   # /usr/local/Cellar/gcc/13.2.0/lib/gcc/current/gcc/x86_64-apple-darwin23/13/include-fixed/stdio.h:78:10: fatal error: _stdio.h: No such file or directory
   #    78 | #include <_stdio.h>
   #       |          ^~~~~~~~~~
   

   Same failure as mentioned in [new release] goblint-cil (2.0.3) #24812 (comment).

[haochenx]

All looks good to me and CI failures are not blocks (as explained by the author)

[mseri]

Thanks