[new release] goblint (2.4.0)

[sim642]

Static analysis framework for C

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

CHANGES:

• Remove unmaintained analyses: spec, file (RFC: Remove spec & file analyses goblint/analyzer#1281).
• Add linear two-variable equalities analysis (Linear Two-Variable Equalities Analysis goblint/analyzer#1297, Lin2var relations fine-tuning - switching from array to map goblint/analyzer#1412, Extending Linear Two-Variable Equalities with Coefficients goblint/analyzer#1466).
• Add callstring, loopfree callstring and context gas analyses (Support for k-callstring & Evaluate different approaches to context-sensitivity goblint/analyzer#1038, master thesis: Taming Recursion with Three Context-Sensitive Analyses (Callstring, LoopfreeCallstring, Context Gas) goblint/analyzer#1340, First-Class Support for Callstring-derived Contexts goblint/analyzer#1379, Pass ctx to context & Simplify callstring-based approaches goblint/analyzer#1427, Fix context gas in g2html goblint/analyzer#1439).
• Add non-relational thread-modular value analyses with thread IDs (Define Missing TID Variants of Non-Relational Privatizations goblint/analyzer#1366, Ego-Lane-Derived-Digests for Privatizations: ProtectionBasedTIDPriv goblint/analyzer#1398, Ego-Lane-Derived-Digests for Privatizations: Lock- & Write-Centered Privatizations goblint/analyzer#1399).
• Add NULL byte array domain (Null Byte Array Domain goblint/analyzer#1076).
• Fix spurious overflow warnings from internal evaluations (Suppress Overflow Warnings for Computations Not in the Program goblint/analyzer#1406, Add flag AnalysisState.executing_speculative_computations to avoid flagging overflows during invariant goblint/analyzer#1411, Binary operations on pointers should not generate overflow warnings in SV-COMP goblint/analyzer#1511).
• Refactor non-definite mutex handling to fix unsoundness (Refactor must-locksets to use definite mvals instead of addresses goblint/analyzer#1430, Fix privatization unsoundness due to non-definite and unknown mutexes goblint/analyzer#1500, Continue refactoring of must-locksets to use definite mvals instead of addresses goblint/analyzer#1503, Check semantic indices of unlocked mutex goblint/analyzer#1409).
• Fix non-relational thread-modular value analysis unsoundness with ambiguous points-to sets (All Non-Relational Privatizations except Miné-W unsound goblint/analyzer#1457, BaseAnalysis: For non-definite AD, join over **all** components not just cpa in set goblint/analyzer#1458).
• Fix mutex type analysis unsoundness and enable it by default (PTHREAD_MUTEX_DEFAULT handling is unsound goblint/analyzer#1414, Fix pthread mutex type from initializer on OSX goblint/analyzer#1416, Enable pthreadMutexType analysis by default goblint/analyzer#1510).
• Add points-to set refinement on mutex path splitting (Refine Points-to-Sets in Base when Splitting Paths for Mutex Analysis goblint/analyzer#1287, Refine Points-To set on locking a mutex goblint/analyzer#1343, Reflexive pointer literal equality not understood goblint/analyzer#1374, Avoid base invariant fallback not understood message on reflexive pointer literal equality goblint/analyzer#1396, Avoid emitting reflexive pointer refines for locking goblint/analyzer#1407).
• Improve narrowing operators (Narrowing from widening thresholds goblint/analyzer#1502, Narrowing with bottom does not produce bottom goblint/analyzer#1540, Propagate bottom through narrowing operators of lattice lifters goblint/analyzer#1543).
• Extract automatic configuration tuning for soundness (Fix and refactor syntactic loop unrolling goblint/analyzer#1369).
• Fix many locations in witnesses (for loop invariant location in YAML witness goblint/analyzer#1355, Location fixes for YAML witness generation/validation goblint/analyzer#1372, Change YAML witness columns to 1-indexed goblint/analyzer#1400, Record statement copies during loop unrolling goblint/analyzer#1403).
• Improve output readability (Improve readability of global invariants goblint/analyzer#1294, Small output readability improvements goblint/analyzer#1312, Improve output for NullByte goblint/analyzer#1405, Improve output for component of blob indicating whether it was created with malloc or calloc goblint/analyzer#1497).
• Refactor logging (Replace direct stdout printing with logging goblint/analyzer#1117).
• Modernize all library function specifications (Convert all library functions to new specifications goblint/analyzer#1029, Klever concurrency safety support goblint/analyzer#688, Add and fix library functions for Concrat benchmarks goblint/analyzer#1174, Port 16 more library functions goblint/analyzer#1289, Port all remaining library functions  goblint/analyzer#1447, Remove library functions old specification mechanisms goblint/analyzer#1487).
• Remove OCaml 4.10, 4.11, 4.12 and 4.13 support (Bump OCaml lower bound to 4.14 goblint/analyzer#1448).

[shonfeder]

LGTM

Test failures on windows are from a dependency:

  #=== ERROR while compiling cpu.2.0.0 ==========================================#
  "autoconf": command not found.
  
  
  <><> Error report <><><><><><><><><><><><><><><><><><><><><><><><><><><><><><><>
  +- The following actions failed
  | - build catapult 0.2
  | - build cppo     1.6.9
  | - build cpu      2.0.0
  +- 

[mseri]

Thanks