[new release] goblint-cil (2.0.0)

[sim642]

A front-end for the C programming language that facilitates program analysis and transformation

• Project page: https://github.com/goblint/cil

CHANGES:

• Wrap library into GoblintCil module (Wrap library goblint/cil#107).
• Remove all MSVC support (RFC: Remove support for MSVC goblint/cil#52, Makefile still looking for Microsoft C compiler despite support for it removed goblint/cil#88).
• Port entire build process from configure/make to dune (Port entire build process from configure/make to dune goblint/cil#104).
• Add C11 _Generic support (Add C11 generic support goblint/cil#48).
• Add C11 _Noreturn support (Support for C11 _Noreturn goblint/cil#58).
• Add C11 _Static_assert support (Add support for _Static_assert goblint/cil#62).
• Add C11 _Alignof support (Support C11 _Alignof(...) goblint/cil#66).
• Add C11 _Alignas support (Frontc parse error due to _Alignas(...) goblint/cil#93, Support for _Alignas(...) goblint/cil#108).
• Add partial C11 _Atomic support (Support for _Atomic goblint/cil#61).
• Add _Float32, _Float64, _Float32x and _Float64x type support (C99 fixed-width integer and floating-point types goblint/cil#8, Add support for additional float types goblint/cil#60).
• Add Universal Character Names, char16_t and char32_t type support (Support for Universal Character Names, char16_t, and char32_t (part of C99/C11) goblint/cil#80).
• Change locations to location spans and add additional expression locations (Add end locations to statements goblint/cil#51).
• Add synthetic marking for CIL-inserted statement locations (Mark synthetic locations goblint/cil#98).
• Expose list of files from line control directives (Maintain a list of all input files that CIL encountered during lexing goblint/cil#73).
• Add parsed location transformation hook (Allow parsed location directive transformation goblint/cil#89).
• Use Zarith for integer constants (Use Cilint in CInt64 goblint/cil#47, Use Cilint in CInt64 goblint/cil#53).
• Fix constant folding overflows (Make constFold aware of overflows and prevent constant folding on overflows goblint/cil#59).
• Add option to disable constant branch removal (Add option removeBranchingOnConstants goblint/cil#103).
• Add standalone expression parsing and checking (Expose standalone expression parsing via Frontc goblint/cil#97, Add standalone expression AST checking goblint/cil#96).
• Improve inline function merging (Proposal: Do not attempt to merge inline functions by default goblint/cil#72, Rename functions with gnu_inline attribute when inline merging is off goblint/cil#85, Not merging inlines breaks fundec invariant goblint/cil#84, Merging: Treat inlines as if they were static when mergeInlines is off goblint/cil#86).
• Fix some attribute parsing cases (Warning: Ignoring un-named typedef that does not introduce a struct or enumeration type for __attribute__((fallthrough)); on null statement goblint/cil#71, Make __attribute__((__fallthrough__)); no longer parse as declaration goblint/cil#75, Support for comma-separated list of declarations with attributes in non-leading position goblint/cil#76, Support for comma-separated list of declarations with attributes in non-leading position goblint/cil#77).
• Fix global NaN initializers (__builtin_nanf("") in global initializers goblint/cil#78, Replace calls to __builtin_nanX with expression leading to NaN goblint/cil#79).
• Fix cilly binary installation (Where is cilly ? goblint/cil#99, Update Readme to clarify status of cilly goblint/cil#100, Add dune install of cilly goblint/cil#102).
• Remove batteries dependency to support OCaml 5 (Remove batteries dependency to support OCaml 5 goblint/cil#106).

[sim642]

Since they came up in the CI, I also made some related and unrelated fixes to the goblint packages. The failures for goblint.1.0.0 should probably be ignored: it's very ancient and the lower bound problem is something else.

The conf-gcc additions are because MacOS is a pain in the butt and symlinks gcc to its own clang, which goblint-cil and goblint don't work with. With conf-gcc it's depext forces homebrew to install a real gcc.

Sorry for the confusing debugging commits listed in this PR. The final force pushed commits should be clean enough to merge.

[mseri]

I have tried to figure out authors for v1.0.0 from the sources, please let me know if that is not correct

[sim642]

I have tried to figure out authors for v1.0.0 from the sources, please let me know if that is not correct

Close, I amended that based on what its own git history reflects.

[mseri]

The lower bound failure is unrelated:

#=== ERROR while installing omake.0.9.8.7 =====================================#
Cannot copy /home/opam/.opam/4.06/.opam-switch/build/omake.0.9.8.7/src/main/omake.opt to /home/opam/.opam/4.06/bin/omake (/usr/bin/opam: "open" failed on /home/opam/.opam/4.06/bin/omake: Permission denied).

[kit-ty-kate]

Thanks!