Main changes from 23.1:


  • support C11's _Static_assert
  • support for flexible array members in nested struct (gcc machdeps only)
  • fixes unsound reuse of recursive functions


  • new options for more precise reporting in case of failed assertion
  • support for \sum, \prod and \numof


  • new experimental taint domain for taint analysis
  • new experimental multidim domain to improve analysis precision on arrays of structures and multidimensional arrays.
  • new options for interprocedural states partitioning
  • new dynamic_split annotation
  • fixes soundness bugs in octagon and bitwise domains
  • improve precision for octagon and symbolic-locations domains


  • translation of printf/scanf calls with non-constant formatting string (assuming arguments match the format)
  • falls back to a generic translation if specialized one fails, to guarantee the absence of variadic calls after the plugin has run


  • removed -wp-overflows option, which was unsound
  • experimental support for terminates clauses