[pkgsrc/trunk]: pkgsrc/devel/frama-c Update devel/frama-c to 25.0

[tonio <tonio%pkgsrc.org@localhost>]

details:   https://anonhg.NetBSD.org/pkgsrc/rev/c02934e0cfdb
branches:  trunk
changeset: 386450:c02934e0cfdb
user:      tonio <tonio%pkgsrc.org@localhost>
date:      Sun Oct 09 07:02:47 2022 +0000

description:
Update devel/frama-c to 25.0

-   Kernel    [2022-10-05] Support for ghost VLA and calls to builtins with
              ghost arguments.
-   Eva       [2022-09-16] Numerors now needs MLMPFR 4.1.0+bugfix2
-   Kernel    [2022-09-07] Improve error message for invalid options -D/-I/-U.
o!  Configure [2022-07-28] Removed autoconf and configure
o!  Makefile  [2022-07-11] Removed Makefile, Frama-C is now built using Dune 3.x
o!  Pdg       [2022-07-01] Removed from Db. Use proper Pdg API instead.
-!  Kernel    [2022-06-06] Remove journalisation.

####################################
Open Source Release 25.0 (Manganese)
####################################

o   Kernel    [2022-05-03] Prototype of AST comparison between two versions
              of the same program, via the new option -ast-diff.
-   Eva       [2022-05-02] Fixes stack overflow errors on very large C functions.
-   Eva       [2022-04-25] Improve the multidim abstract domain: it is now
              more precise and more robust, it is able to infer simple array
              invariants on some loops without unrolling, and has a new option
              -eva-multidim-disjunctive-invariants to infer structures
              disjunctive invariants.
o   Kernel    [2022-03-07] Known compiler builtins are no longer hardcoded in
              OCaml, but defined via JSON files (in share/compliance).
o   Kernel    [2022-02-23] New visitor functions visitFramacFileFunctions
              and visitCilFileFunctions to visit only function definitions,
              for better performance.
o!  Kernel    [2022-02-23] Remove State_selection.Static (deprecated since
              10 years, use directly State_selection instead)
-*  Kernel    [2022-02-22] Fix list of potential types for decimal
              integer literal constants
*   Kernel    [2022-02-17] Reject programs using unsupported
              vector_size attribute (fixes ##2573)
o   Eva       [2022-02-15] New API to run the analysis and access its results,
              intended to replace the old API in Db.Value. It is more precise
              as it uses all available domains to evaluate values and locations.
              See file Eva.mli for more details.
*   Kernel    [2022-02-08] Reject array whose size is too big with a proper
              error message instead of a crash (fixes ##2590)
o!  Kernel    [2022-02-19] Removed obsolete AST nodes IndexPI and Info
*   Kernel    [2022-02-08] Reject array whose size is too big with a proper
              error message instead of a crash (fixes ##2590)
o!  Kernel    [2021-12-03] Remove unused AST node Dcustom_annot and field
              fpadding_in_bits. Do not cache size of types in the AST but in
              a dedicated table.
-*  Logic     [2021-11-30] Fix type of expressions whose value are functions
o!  Kernel    [2021-11-29] Integer.pretty does not have the optional argument
              hexa anymore. Use Integer.pretty_hex or Integer.pp_hex if you
              want to print integers in hexadecimal format.

diffstat:

 devel/frama-c/Makefile                                         |    13 +-
 devel/frama-c/PLIST                                            |  1089 +++++----
 devel/frama-c/distinfo                                         |    18 +-
 devel/frama-c/options.mk                                       |     5 +-
 devel/frama-c/patches/patch-Makefile                           |    60 +-
 devel/frama-c/patches/patch-configure                          |    15 -
 devel/frama-c/patches/patch-src_libraries_utils_c__bindings.c  |    38 +-
 devel/frama-c/patches/patch-src_plugins_e-acsl_Makefile.in     |    64 -
 devel/frama-c/patches/patch-src_plugins_gui_gtk__helper.ml     |    17 -
 devel/frama-c/patches/patch-src_plugins_wp_configure           |    15 -
 devel/frama-c/patches/patch-src_plugins_wp_configure.ac        |    15 -
 devel/frama-c/patches/patch-src_plugins_wp_share_coqwp_Zbits.v |    24 -
 12 files changed, 690 insertions(+), 683 deletions(-)

diffs (truncated from 2295 to 300 lines):

diff -r 970eb40bc11f -r c02934e0cfdb devel/frama-c/Makefile
--- a/devel/frama-c/Makefile    Sun Oct 09 06:47:13 2022 +0000
+++ b/devel/frama-c/Makefile    Sun Oct 09 07:02:47 2022 +0000
@@ -1,9 +1,8 @@
-# $NetBSD: Makefile,v 1.104 2022/08/29 16:14:41 wiz Exp $
+# $NetBSD: Makefile,v 1.105 2022/10/09 07:02:47 tonio Exp $
 #
 
-DISTNAME=      frama-c-Phosphorus-20170501
-PKGNAME=       ${DISTNAME:S/-Phosphorus//}
-PKGREVISION=   35
+DISTNAME=      frama-c-25.0-Manganese
+PKGNAME=       ${DISTNAME:S/-Manganese//}
 CATEGORIES=    devel
 MASTER_SITES=  https://frama-c.com/download/
 
@@ -14,6 +13,8 @@
 
 USE_TOOLS+=    gmake autoconf
 GNU_CONFIGURE= yes
+REPLACE_SH=    src/plugins/e-acsl/scripts/e-acsl-gcc.sh
+REPLACE_PYTHON=        share/analysis-scripts/*.py
 
 OCAML_USE_FINDLIB=     yes
 
@@ -23,8 +24,12 @@
 # (not the default) or the build fails with missing module "Dgraph".
 
 .include "../../devel/ocamlgraph/buildlink3.mk"
+.include "../../devel/ocaml-yojson/buildlink3.mk"
+.include "../../devel/ocaml-ppx_import/buildlink3.mk"
+.include "../../devel/ocaml-ppx_deriving/buildlink3.mk"
 .include "../../math/ocaml-num/buildlink3.mk"
 .include "../../math/ocaml-zarith/buildlink3.mk"
 
 .include "../../lang/ocaml/ocaml.mk"
+.include "../../lang/python/application.mk"
 .include "../../mk/bsd.pkg.mk"
diff -r 970eb40bc11f -r c02934e0cfdb devel/frama-c/PLIST
--- a/devel/frama-c/PLIST       Sun Oct 09 06:47:13 2022 +0000
+++ b/devel/frama-c/PLIST       Sun Oct 09 07:02:47 2022 +0000
@@ -1,574 +1,631 @@
-@comment $NetBSD: PLIST,v 1.6 2017/09/05 07:41:35 dholland Exp $
+@comment $NetBSD: PLIST,v 1.7 2022/10/09 07:02:47 tonio Exp $
 bin/e-acsl-gcc.sh
 bin/frama-c
 bin/frama-c-config
 ${PLIST.gui}bin/frama-c-gui
 ${PLIST.gui}bin/frama-c-gui.byte
+bin/frama-c-script
 bin/frama-c.byte
-@comment bin/ptests.byte
 bin/ptests.opt
-lib/frama-c/FCBuffer.cmi
-lib/frama-c/FCBuffer.cmo
-lib/frama-c/FCBuffer.cmx
-lib/frama-c/FCBuffer.o
 lib/frama-c/FCHashtbl.cmi
 lib/frama-c/FCHashtbl.cmo
-lib/frama-c/FCHashtbl.cmx
+${PLIST.ocaml-opt}lib/frama-c/FCHashtbl.cmx
 lib/frama-c/FCHashtbl.o
-lib/frama-c/FCMap.cmi
-lib/frama-c/FCMap.cmo
-lib/frama-c/FCMap.cmx
-lib/frama-c/FCMap.o
-lib/frama-c/FCSet.cmi
-lib/frama-c/FCSet.cmo
-lib/frama-c/FCSet.cmx
-lib/frama-c/FCSet.o
-lib/frama-c/Qed.cmi
-lib/frama-c/Qed.cmo
-lib/frama-c/Qed.cmx
-lib/frama-c/Qed.o
+${PLIST.gui}lib/frama-c/GSourceView.cmi
+${PLIST.gui}lib/frama-c/GSourceView.cmo
+${PLIST.gui}${PLIST.ocaml-opt}lib/frama-c/GSourceView.cmx
+${PLIST.gui}lib/frama-c/GSourceView.o
+lib/frama-c/META.frama-c
 lib/frama-c/abstract_interp.cmi
 lib/frama-c/abstract_interp.cmo
-lib/frama-c/abstract_interp.cmx
+${PLIST.ocaml-opt}lib/frama-c/abstract_interp.cmx
 lib/frama-c/abstract_interp.o
-@comment lib/frama-c/abstract_value.cmi
-@comment lib/frama-c/abstract_value.cmo
-@comment lib/frama-c/abstract_value.cmx
-@comment lib/frama-c/abstract_value.o
+lib/frama-c/acsl_extension.cmi
+lib/frama-c/acsl_extension.cmo
+${PLIST.ocaml-opt}lib/frama-c/acsl_extension.cmx
+lib/frama-c/acsl_extension.o
 lib/frama-c/alarms.cmi
 lib/frama-c/alarms.cmo
-lib/frama-c/alarms.cmx
+${PLIST.ocaml-opt}lib/frama-c/alarms.cmx
 lib/frama-c/alarms.o
 lib/frama-c/allocates.cmi
 lib/frama-c/allocates.cmo
-lib/frama-c/allocates.cmx
+${PLIST.ocaml-opt}lib/frama-c/allocates.cmx
 lib/frama-c/allocates.o
 lib/frama-c/alpha.cmi
 lib/frama-c/alpha.cmo
-lib/frama-c/alpha.cmx
+${PLIST.ocaml-opt}lib/frama-c/alpha.cmx
 lib/frama-c/alpha.o
 ${PLIST.gui}lib/frama-c/analyses_manager.cmi
 ${PLIST.gui}lib/frama-c/analyses_manager.cmo
-${PLIST.gui}lib/frama-c/analyses_manager.cmx
+${PLIST.gui}${PLIST.ocaml-opt}lib/frama-c/analyses_manager.cmx
 ${PLIST.gui}lib/frama-c/analyses_manager.o
 lib/frama-c/annotations.cmi
 lib/frama-c/annotations.cmo
-lib/frama-c/annotations.cmx
+${PLIST.ocaml-opt}lib/frama-c/annotations.cmx
 lib/frama-c/annotations.o
 lib/frama-c/asm_contracts.cmi
 lib/frama-c/asm_contracts.cmo
-lib/frama-c/asm_contracts.cmx
+${PLIST.ocaml-opt}lib/frama-c/asm_contracts.cmx
 lib/frama-c/asm_contracts.o
 lib/frama-c/ast.cmi
 lib/frama-c/ast.cmo
-lib/frama-c/ast.cmx
+${PLIST.ocaml-opt}lib/frama-c/ast.cmx
 lib/frama-c/ast.o
+lib/frama-c/ast_diff.cmi
+lib/frama-c/ast_diff.cmo
+${PLIST.ocaml-opt}lib/frama-c/ast_diff.cmx
+lib/frama-c/ast_diff.o
 lib/frama-c/ast_info.cmi
 lib/frama-c/ast_info.cmo
-lib/frama-c/ast_info.cmx
+${PLIST.ocaml-opt}lib/frama-c/ast_info.cmx
 lib/frama-c/ast_info.o
 lib/frama-c/bag.cmi
 lib/frama-c/bag.cmo
-lib/frama-c/bag.cmx
+${PLIST.ocaml-opt}lib/frama-c/bag.cmx
 lib/frama-c/bag.o
 lib/frama-c/base.cmi
 lib/frama-c/base.cmo
-lib/frama-c/base.cmx
+${PLIST.ocaml-opt}lib/frama-c/base.cmx
 lib/frama-c/base.o
 lib/frama-c/binary_cache.cmi
 lib/frama-c/binary_cache.cmo
-lib/frama-c/binary_cache.cmx
+${PLIST.ocaml-opt}lib/frama-c/binary_cache.cmx
 lib/frama-c/binary_cache.o
 lib/frama-c/bit_utils.cmi
 lib/frama-c/bit_utils.cmo
-lib/frama-c/bit_utils.cmx
+${PLIST.ocaml-opt}lib/frama-c/bit_utils.cmx
 lib/frama-c/bit_utils.o
 lib/frama-c/bitvector.cmi
 lib/frama-c/bitvector.cmo
-lib/frama-c/bitvector.cmx
+${PLIST.ocaml-opt}lib/frama-c/bitvector.cmx
 lib/frama-c/bitvector.o
 ${PLIST.gui}lib/frama-c/book_manager.cmi
 ${PLIST.gui}lib/frama-c/book_manager.cmo
-${PLIST.gui}lib/frama-c/book_manager.cmx
+${PLIST.gui}${PLIST.ocaml-opt}lib/frama-c/book_manager.cmx
 ${PLIST.gui}lib/frama-c/book_manager.o
 lib/frama-c/boot.cmi
 lib/frama-c/boot.cmo
-lib/frama-c/boot.cmx
+${PLIST.ocaml-opt}lib/frama-c/boot.cmx
 lib/frama-c/boot.o
-lib/frama-c/bottom.cmi
-lib/frama-c/bottom.cmo
-lib/frama-c/bottom.cmx
-lib/frama-c/bottom.o
 lib/frama-c/c_bindings.o
 lib/frama-c/cabs.cmi
-lib/frama-c/cabs.cmo
-lib/frama-c/cabs.cmx
-lib/frama-c/cabs.o
 lib/frama-c/cabs2cil.cmi
 lib/frama-c/cabs2cil.cmo
-lib/frama-c/cabs2cil.cmx
+${PLIST.ocaml-opt}lib/frama-c/cabs2cil.cmx
 lib/frama-c/cabs2cil.o
 lib/frama-c/cabs_debug.cmi
 lib/frama-c/cabs_debug.cmo
-lib/frama-c/cabs_debug.cmx
+${PLIST.ocaml-opt}lib/frama-c/cabs_debug.cmx
 lib/frama-c/cabs_debug.o
 lib/frama-c/cabshelper.cmi
 lib/frama-c/cabshelper.cmo
-lib/frama-c/cabshelper.cmx
+${PLIST.ocaml-opt}lib/frama-c/cabshelper.cmx
 lib/frama-c/cabshelper.o
 lib/frama-c/cabsvisit.cmi
 lib/frama-c/cabsvisit.cmo
-lib/frama-c/cabsvisit.cmx
+${PLIST.ocaml-opt}lib/frama-c/cabsvisit.cmx
 lib/frama-c/cabsvisit.o
 lib/frama-c/cfg.cmi
 lib/frama-c/cfg.cmo
-lib/frama-c/cfg.cmx
+${PLIST.ocaml-opt}lib/frama-c/cfg.cmx
 lib/frama-c/cfg.o
 lib/frama-c/cil.cmi
 lib/frama-c/cil.cmo
-lib/frama-c/cil.cmx
+${PLIST.ocaml-opt}lib/frama-c/cil.cmx
 lib/frama-c/cil.o
 lib/frama-c/cilE.cmi
 lib/frama-c/cilE.cmo
-lib/frama-c/cilE.cmx
+${PLIST.ocaml-opt}lib/frama-c/cilE.cmx
 lib/frama-c/cilE.o
+lib/frama-c/cil_builder.cmi
+lib/frama-c/cil_builder.cmo
+${PLIST.ocaml-opt}lib/frama-c/cil_builder.cmx
+lib/frama-c/cil_builder.o
+lib/frama-c/cil_builtins.cmi
+lib/frama-c/cil_builtins.cmo
+${PLIST.ocaml-opt}lib/frama-c/cil_builtins.cmx
+lib/frama-c/cil_builtins.o
 lib/frama-c/cil_const.cmi
 lib/frama-c/cil_const.cmo
-lib/frama-c/cil_const.cmx
+${PLIST.ocaml-opt}lib/frama-c/cil_const.cmx
 lib/frama-c/cil_const.o
 lib/frama-c/cil_datatype.cmi
 lib/frama-c/cil_datatype.cmo
-lib/frama-c/cil_datatype.cmx
+${PLIST.ocaml-opt}lib/frama-c/cil_datatype.cmx
 lib/frama-c/cil_datatype.o
 lib/frama-c/cil_descriptive_printer.cmi
 lib/frama-c/cil_descriptive_printer.cmo
-lib/frama-c/cil_descriptive_printer.cmx
+${PLIST.ocaml-opt}lib/frama-c/cil_descriptive_printer.cmx
 lib/frama-c/cil_descriptive_printer.o
 lib/frama-c/cil_printer.cmi
 lib/frama-c/cil_printer.cmo
-lib/frama-c/cil_printer.cmx
+${PLIST.ocaml-opt}lib/frama-c/cil_printer.cmx
 lib/frama-c/cil_printer.o
 lib/frama-c/cil_state_builder.cmi
 lib/frama-c/cil_state_builder.cmo
-lib/frama-c/cil_state_builder.cmx
+${PLIST.ocaml-opt}lib/frama-c/cil_state_builder.cmx
 lib/frama-c/cil_state_builder.o
 lib/frama-c/cil_types.cmi
 lib/frama-c/cil_types_debug.cmi
 lib/frama-c/cil_types_debug.cmo
-lib/frama-c/cil_types_debug.cmx
+${PLIST.ocaml-opt}lib/frama-c/cil_types_debug.cmx
 lib/frama-c/cil_types_debug.o
 lib/frama-c/cilconfig.cmi
 lib/frama-c/cilconfig.cmo
-lib/frama-c/cilconfig.cmx
+${PLIST.ocaml-opt}lib/frama-c/cilconfig.cmx
 lib/frama-c/cilconfig.o
 lib/frama-c/clexer.cmi
 lib/frama-c/clexer.cmo
-lib/frama-c/clexer.cmx
+${PLIST.ocaml-opt}lib/frama-c/clexer.cmx
 lib/frama-c/clexer.o
 lib/frama-c/clone.cmi
 lib/frama-c/clone.cmo
-lib/frama-c/clone.cmx
+${PLIST.ocaml-opt}lib/frama-c/clone.cmx
 lib/frama-c/clone.o
 lib/frama-c/cmdline.cmi
 lib/frama-c/cmdline.cmo
-lib/frama-c/cmdline.cmx
+${PLIST.ocaml-opt}lib/frama-c/cmdline.cmx
 lib/frama-c/cmdline.o
 lib/frama-c/command.cmi
 lib/frama-c/command.cmo
-lib/frama-c/command.cmx
+${PLIST.ocaml-opt}lib/frama-c/command.cmx
 lib/frama-c/command.o
-lib/frama-c/config.cmi
-lib/frama-c/config.cmo
-lib/frama-c/config.cmx
-lib/frama-c/config.o
+lib/frama-c/contract_special_float.cmi
+lib/frama-c/contract_special_float.cmo
+${PLIST.ocaml-opt}lib/frama-c/contract_special_float.cmx
+lib/frama-c/contract_special_float.o
 lib/frama-c/cparser.cmi
 lib/frama-c/cparser.cmo
-lib/frama-c/cparser.cmx
+${PLIST.ocaml-opt}lib/frama-c/cparser.cmx
 lib/frama-c/cparser.o
 lib/frama-c/cprint.cmi
 lib/frama-c/cprint.cmo
-lib/frama-c/cprint.cmx
+${PLIST.ocaml-opt}lib/frama-c/cprint.cmx
 lib/frama-c/cprint.o
 lib/frama-c/cvalue.cmi
 lib/frama-c/cvalue.cmo
-lib/frama-c/cvalue.cmx