Download raw body.
[update] devel/frama-c 19.0 -> 24.0
This is the newest update before frama-c needs various ppx* packages to be
imported.
ok?
Index: Makefile
===================================================================
RCS file: /cvs/ports/devel/frama-c/Makefile,v
diff -u -p -u -r1.31 Makefile
--- Makefile 24 Apr 2024 17:09:54 -0000 1.31
+++ Makefile 12 Jun 2026 01:22:29 -0000
@@ -4,13 +4,13 @@ FIX_EXTRACT_PERMISSIONS = Yes
COMMENT = extensible platform for analysis of C software
+# XXX: 25+ needs ppx_import and more
+# XXX: 26+ switches to dune
+V = 24.0
+DISTNAME = frama-c-${V}-Chromium
+PKGNAME = frama-c-${V}
+
CATEGORIES = devel
-GH_ACCOUNT = Frama-C
-GH_PROJECT = Frama-C-snapshot
-GH_TAGNAME = 19.0
-REVISION = 8
-DISTNAME = frama-c-${GH_TAGNAME}-Potassium
-PKGNAME = frama-c-${GH_TAGNAME}
HOMEPAGE = https://frama-c.com/
@@ -19,8 +19,10 @@ PERMIT_PACKAGE = Yes
WANTLIB += atk-1.0 c cairo cairo-gobject fontconfig freetype gdk-3
WANTLIB += gdk_pixbuf-2.0 gio-2.0 glib-2.0 gmp gobject-2.0 gtk-3
-WANTLIB += gtksourceview-3.0 intl m pango-1.0 pangocairo-1.0 pthread
-WANTLIB += z
+WANTLIB += gtksourceview-3.0 harfbuzz intl m pango-1.0 pangocairo-1.0
+WANTLIB += pthread
+
+SITES = https://frama-c.com/download/
MODULES = lang/ocaml
Index: distinfo
===================================================================
RCS file: /cvs/ports/devel/frama-c/distinfo,v
diff -u -p -u -r1.4 distinfo
--- distinfo 7 Sep 2019 17:11:53 -0000 1.4
+++ distinfo 12 Jun 2026 01:22:29 -0000
@@ -1,2 +1,2 @@
-SHA256 (frama-c-19.0-Potassium.tar.gz) = JQLGITrB+V4E0qaPszAhcvpa9hV0+jD9gpWWI+SwgyY=
-SIZE (frama-c-19.0-Potassium.tar.gz) = 5615479
+SHA256 (frama-c-24.0-Chromium.tar.gz) = TurxMheAqNiPSS+1CoOFmiKVheM/p6XhDb9JUG58PXQ=
+SIZE (frama-c-24.0-Chromium.tar.gz) = 7495244
Index: patches/patch-Makefile
===================================================================
RCS file: patches/patch-Makefile
diff -N patches/patch-Makefile
--- patches/patch-Makefile 11 Mar 2022 18:50:03 -0000 1.3
+++ /dev/null 1 Jan 1970 00:00:00 -0000
@@ -1,53 +0,0 @@
-don't try to build or install cmx* files on bytecode builds.
-
-Index: Makefile
---- Makefile.orig
-+++ Makefile
-@@ -1234,12 +1234,15 @@ bin/toplevel.opt$(EXE): $(ALL_BATCH_CMX) $(GEN_OPT_LIB
- LIB_KERNEL_CMO= $(filter-out src/kernel_internals/runtime/gui_init.cmo, $(CMO))
- LIB_KERNEL_CMX= $(filter-out src/kernel_internals/runtime/gui_init.cmx, $(CMX))
-
--lib/fc/frama-c.cma: $(LIB_KERNEL_CMO) $(GEN_OPT_LIBS) $(LIB_KERNEL_CMX) lib/fc/META.frama-c
-- $(PRINT_LINKING) $@ and lib/fc/frama-c.cmxa
-+lib/fc/frama-c.cma: $(LIB_KERNEL_CMO) $(GEN_OPT_LIBS) lib/fc/META.frama-c
-+ $(PRINT_LINKING) $@
- $(MKDIR) $(FRAMAC_LIB)
-- $(OCAMLMKLIB) -o lib/fc/frama-c $(OPT_LIBS) $(LIB_KERNEL_CMO) $(LIB_KERNEL_CMX)
-+ $(OCAMLMKLIB) -o lib/fc/frama-c $(OPT_LIBS) $(LIB_KERNEL_CMO)
-
- lib/fc/frama-c.cmxa: lib/fc/frama-c.cma
-+ $(MKDIR) $(FRAMAC_LIB)
-+ $(PRINT_LINKING) $@
-+ $(OCAMLMKLIB) -o lib/fc/frama-c $(OPT_LIBS) $(LIB_KERNEL_CMX)
-
- ####################
- # (Ocaml) Toplevel #
-@@ -1863,12 +1866,16 @@ clean-install:
- $(PRINT_RM) "Installation directory"
- $(RM) -r $(FRAMAC_LIBDIR)
-
--install-lib: clean-install
-+install-lib-byte: clean-install
- $(PRINT_INSTALL) kernel API
- $(MKDIR) $(FRAMAC_LIBDIR)
-- $(CP) $(LIB_BYTE_TO_INSTALL) $(LIB_OPT_TO_INSTALL) $(FRAMAC_LIBDIR)
-- $(CP) $(addprefix lib/fc/,dllframa-c.so libframa-c.a frama-c.cma frama-c.a frama-c.cmxa META.frama-c) $(FRAMAC_LIBDIR)
-+ $(CP) $(LIB_BYTE_TO_INSTALL) $(FRAMAC_LIBDIR)
-+ $(CP) $(addprefix lib/fc/,dllframa-c.so libframa-c.a frama-c.cma META.frama-c) $(FRAMAC_LIBDIR)
-
-+install-lib-opt: install-lib-byte
-+ $(CP) $(LIB_OPT_TO_INSTALL) $(FRAMAC_LIBDIR)
-+ $(CP) $(addprefix lib/fc/,frama-c.a frama-c.cmxa) $(FRAMAC_LIBDIR)
-+
- install-doc-code:
- $(PRINT_INSTALL) API documentation
- $(MKDIR) $(FRAMAC_DATADIR)/doc/code
-@@ -1879,7 +1886,7 @@ install-doc-code:
- | (cd $(FRAMAC_DATADIR)/doc ; tar xf -))
-
- .PHONY: install
--install:: install-lib
-+install:: install-lib-$(OCAMLBEST)
- $(PRINT_MAKING) destination directories
- $(MKDIR) $(BINDIR)
- $(MKDIR) $(MANDIR)/man1
Index: patches/patch-configure_in
===================================================================
RCS file: patches/patch-configure_in
diff -N patches/patch-configure_in
--- patches/patch-configure_in 11 Mar 2022 18:50:03 -0000 1.3
+++ /dev/null 1 Jan 1970 00:00:00 -0000
@@ -1,41 +0,0 @@
-Use system threads if available - even on bytecode builds.
-Vmthreads are broken and deprecated.
-
-Index: configure.in
---- configure.in.orig
-+++ configure.in
-@@ -446,23 +446,19 @@ else
- EXE=
- fi
-
-- if test "$OCAMLBEST" = opt; then
-- # OCaml native threads
-- AC_MSG_CHECKING([OCaml native threads])
-- echo "let f = Thread.create (fun () -> ())" > test_native_threads.ml
-- if ($OCAMLOPT -thread -o test_native_threads unix.cmxa threads.cmxa \
-- test_native_threads.ml) 2> /dev/null ;
-- then
-- HAS_NATIVE_THREADS=yes
-- AC_MSG_RESULT([ok.]);
-- else
-- HAS_NATIVE_THREADS=no
-- AC_MSG_WARN([unsupported.]);
-- fi
-- rm -f test_native_threads*;
-+ AC_MSG_CHECKING([OCaml native threads])
-+ echo "let f = Thread.create (fun () -> ())" > test_native_threads.ml
-+ if
-+ ($OCAMLC -thread -o test_native_threads unix.cma threads.cma \
-+ test_native_threads.ml) 2> /dev/null
-+ then
-+ HAS_NATIVE_THREADS=yes
-+ AC_MSG_RESULT([ok.]);
- else
-- HAS_NATIVE_THREADS=no; # no native compilation anyway
-+ HAS_NATIVE_THREADS=no
-+ AC_MSG_WARN([unsupported.]);
- fi
-+ rm -f test_native_threads*;
- fi
-
- # C and POSIX standard headers used by C bindings.
Index: pkg/PFRAG.dynlink-native
===================================================================
RCS file: /cvs/ports/devel/frama-c/pkg/PFRAG.dynlink-native,v
diff -u -p -u -r1.5 PFRAG.dynlink-native
--- pkg/PFRAG.dynlink-native 11 Mar 2022 18:50:03 -0000 1.5
+++ pkg/PFRAG.dynlink-native 12 Jun 2026 01:22:29 -0000
@@ -3,20 +3,20 @@
@bin lib/frama-c/plugins/gui/Impact.cmxs
@bin lib/frama-c/plugins/gui/Metrics.cmxs
@bin lib/frama-c/plugins/gui/Occurrence.cmxs
-@bin lib/frama-c/plugins/gui/Qed.cmxs
@bin lib/frama-c/plugins/gui/Scope.cmxs
@bin lib/frama-c/plugins/gui/Security_slicing.cmxs
@bin lib/frama-c/plugins/gui/Slicing.cmxs
@bin lib/frama-c/plugins/gui/Studia.cmxs
-@bin lib/frama-c/plugins/gui/Wp.cmxs
@bin lib/frama-c/plugins/top/Aorai.cmxs
@bin lib/frama-c/plugins/top/Callgraph.cmxs
@bin lib/frama-c/plugins/top/Constant_Propagation.cmxs
+@bin lib/frama-c/plugins/top/Dive.cmxs
@bin lib/frama-c/plugins/top/E_ACSL.cmxs
@bin lib/frama-c/plugins/top/Eva.cmxs
@bin lib/frama-c/plugins/top/From.cmxs
@bin lib/frama-c/plugins/top/Impact.cmxs
@bin lib/frama-c/plugins/top/Inout.cmxs
+@bin lib/frama-c/plugins/top/Instantiate.cmxs
@bin lib/frama-c/plugins/top/LoopAnalysis.cmxs
@bin lib/frama-c/plugins/top/Metrics.cmxs
@bin lib/frama-c/plugins/top/Nonterm.cmxs
@@ -26,13 +26,14 @@
@bin lib/frama-c/plugins/top/Postdominators.cmxs
@bin lib/frama-c/plugins/top/Print_api.cmxs
@bin lib/frama-c/plugins/top/Qed.cmxs
+@bin lib/frama-c/plugins/top/Reduc.cmxs
@bin lib/frama-c/plugins/top/Report.cmxs
@bin lib/frama-c/plugins/top/RteGen.cmxs
@bin lib/frama-c/plugins/top/Scope.cmxs
@bin lib/frama-c/plugins/top/Security_slicing.cmxs
+@bin lib/frama-c/plugins/top/Server.cmxs
@bin lib/frama-c/plugins/top/Slicing.cmxs
@bin lib/frama-c/plugins/top/Sparecode.cmxs
@bin lib/frama-c/plugins/top/Studia.cmxs
@bin lib/frama-c/plugins/top/Users.cmxs
@bin lib/frama-c/plugins/top/Variadic.cmxs
-@bin lib/frama-c/plugins/top/Wp.cmxs
Index: pkg/PFRAG.native
===================================================================
RCS file: /cvs/ports/devel/frama-c/pkg/PFRAG.native,v
diff -u -p -u -r1.6 PFRAG.native
--- pkg/PFRAG.native 11 Mar 2022 18:50:03 -0000 1.6
+++ pkg/PFRAG.native 12 Jun 2026 01:22:29 -0000
@@ -1,17 +1,17 @@
%%dynlink%%
@bin bin/ptests.opt
-lib/frama-c/FCBuffer.cmx
-lib/frama-c/FCBuffer.o
lib/frama-c/FCHashtbl.cmx
lib/frama-c/FCHashtbl.o
-lib/frama-c/FCMap.cmx
-lib/frama-c/FCMap.o
-lib/frama-c/FCSet.cmx
-lib/frama-c/FCSet.o
lib/frama-c/GSourceView.cmx
lib/frama-c/GSourceView.o
lib/frama-c/abstract_interp.cmx
lib/frama-c/abstract_interp.o
+lib/frama-c/abstract_memory.cmx
+lib/frama-c/abstract_memory.o
+lib/frama-c/abstract_offset.cmx
+lib/frama-c/abstract_offset.o
+lib/frama-c/acsl_extension.cmx
+lib/frama-c/acsl_extension.o
lib/frama-c/alarms.cmx
lib/frama-c/alarms.o
lib/frama-c/allocates.cmx
@@ -44,8 +44,6 @@ lib/frama-c/boot.cmx
lib/frama-c/boot.o
lib/frama-c/bottom.cmx
lib/frama-c/bottom.o
-lib/frama-c/cabs.cmx
-lib/frama-c/cabs.o
lib/frama-c/cabs2cil.cmx
lib/frama-c/cabs2cil.o
lib/frama-c/cabs_debug.cmx
@@ -60,6 +58,10 @@ lib/frama-c/cil.cmx
lib/frama-c/cil.o
lib/frama-c/cilE.cmx
lib/frama-c/cilE.o
+lib/frama-c/cil_builder.cmx
+lib/frama-c/cil_builder.o
+lib/frama-c/cil_builtins.cmx
+lib/frama-c/cil_builtins.o
lib/frama-c/cil_const.cmx
lib/frama-c/cil_const.o
lib/frama-c/cil_datatype.cmx
@@ -82,8 +84,8 @@ lib/frama-c/cmdline.cmx
lib/frama-c/cmdline.o
lib/frama-c/command.cmx
lib/frama-c/command.o
-lib/frama-c/config.cmx
-lib/frama-c/config.o
+lib/frama-c/contract_special_float.cmx
+lib/frama-c/contract_special_float.o
lib/frama-c/cparser.cmx
lib/frama-c/cparser.o
lib/frama-c/cprint.cmx
@@ -98,8 +100,6 @@ lib/frama-c/datatype.cmx
lib/frama-c/datatype.o
lib/frama-c/db.cmx
lib/frama-c/db.o
-lib/frama-c/debug_manager.cmx
-lib/frama-c/debug_manager.o
lib/frama-c/descr.cmx
lib/frama-c/descr.o
lib/frama-c/description.cmx
@@ -108,10 +108,14 @@ lib/frama-c/design.cmx
lib/frama-c/design.o
lib/frama-c/destructors.cmx
lib/frama-c/destructors.o
-lib/frama-c/dgraph.cmx
-lib/frama-c/dgraph.o
+lib/frama-c/dgraph_helper.cmx
+lib/frama-c/dgraph_helper.o
lib/frama-c/dominators.cmx
lib/frama-c/dominators.o
+lib/frama-c/dotgraph.cmx
+lib/frama-c/dotgraph.o
+lib/frama-c/dump_config.cmx
+lib/frama-c/dump_config.o
lib/frama-c/dynamic.cmx
lib/frama-c/dynamic.o
lib/frama-c/emitter.cmx
@@ -124,6 +128,8 @@ lib/frama-c/exn_flow.cmx
lib/frama-c/exn_flow.o
lib/frama-c/extlib.cmx
lib/frama-c/extlib.o
+lib/frama-c/fc_config.cmx
+lib/frama-c/fc_config.o
lib/frama-c/fc_float.cmx
lib/frama-c/fc_float.o
lib/frama-c/file.cmx
@@ -152,6 +158,10 @@ lib/frama-c/function_Froms.cmx
lib/frama-c/function_Froms.o
lib/frama-c/fval.cmx
lib/frama-c/fval.o
+lib/frama-c/ghost_accesses.cmx
+lib/frama-c/ghost_accesses.o
+lib/frama-c/ghost_cfg.cmx
+lib/frama-c/ghost_cfg.o
lib/frama-c/globals.cmx
lib/frama-c/globals.o
lib/frama-c/gtk_compat.cmx
@@ -186,6 +196,12 @@ lib/frama-c/int_Base.cmx
lib/frama-c/int_Base.o
lib/frama-c/int_Intervals.cmx
lib/frama-c/int_Intervals.o
+lib/frama-c/int_interval.cmx
+lib/frama-c/int_interval.o
+lib/frama-c/int_set.cmx
+lib/frama-c/int_set.o
+lib/frama-c/int_val.cmx
+lib/frama-c/int_val.o
lib/frama-c/integer.cmx
lib/frama-c/integer.o
lib/frama-c/interpreted_automata.cmx
@@ -206,8 +222,6 @@ lib/frama-c/lattice_messages.cmx
lib/frama-c/lattice_messages.o
lib/frama-c/launcher.cmx
lib/frama-c/launcher.o
-lib/frama-c/leftistheap.cmx
-lib/frama-c/leftistheap.o
lib/frama-c/lexerhack.cmx
lib/frama-c/lexerhack.o
lib/frama-c/lmap.cmx
@@ -244,12 +258,16 @@ lib/frama-c/machdeps.cmx
lib/frama-c/machdeps.o
lib/frama-c/map_lattice.cmx
lib/frama-c/map_lattice.o
+lib/frama-c/markdown.cmx
+lib/frama-c/markdown.o
lib/frama-c/menu_manager.cmx
lib/frama-c/menu_manager.o
lib/frama-c/mergecil.cmx
lib/frama-c/mergecil.o
lib/frama-c/messages.cmx
lib/frama-c/messages.o
+lib/frama-c/multidim.cmx
+lib/frama-c/multidim.o
lib/frama-c/offsetmap.cmx
lib/frama-c/offsetmap.o
lib/frama-c/oneret.cmx
@@ -277,11 +295,13 @@ lib/frama-c/plugin.o
lib/frama-c/plugins/top/Aorai.cmx
lib/frama-c/plugins/top/Callgraph.cmx
lib/frama-c/plugins/top/Constant_Propagation.cmx
+lib/frama-c/plugins/top/Dive.cmx
lib/frama-c/plugins/top/E_ACSL.cmx
lib/frama-c/plugins/top/Eva.cmx
lib/frama-c/plugins/top/From.cmx
lib/frama-c/plugins/top/Impact.cmx
lib/frama-c/plugins/top/Inout.cmx
+lib/frama-c/plugins/top/Instantiate.cmx
lib/frama-c/plugins/top/LoopAnalysis.cmx
lib/frama-c/plugins/top/Metrics.cmx
lib/frama-c/plugins/top/Nonterm.cmx
@@ -291,16 +311,17 @@ lib/frama-c/plugins/top/Pdg.cmx
lib/frama-c/plugins/top/Postdominators.cmx
lib/frama-c/plugins/top/Print_api.cmx
lib/frama-c/plugins/top/Qed.cmx
+lib/frama-c/plugins/top/Reduc.cmx
lib/frama-c/plugins/top/Report.cmx
lib/frama-c/plugins/top/RteGen.cmx
lib/frama-c/plugins/top/Scope.cmx
lib/frama-c/plugins/top/Security_slicing.cmx
+lib/frama-c/plugins/top/Server.cmx
lib/frama-c/plugins/top/Slicing.cmx
lib/frama-c/plugins/top/Sparecode.cmx
lib/frama-c/plugins/top/Studia.cmx
lib/frama-c/plugins/top/Users.cmx
lib/frama-c/plugins/top/Variadic.cmx
-lib/frama-c/plugins/top/Wp.cmx
lib/frama-c/precise_locs.cmx
lib/frama-c/precise_locs.o
lib/frama-c/pretty_source.cmx
@@ -363,6 +384,8 @@ lib/frama-c/stmts_graph.cmx
lib/frama-c/stmts_graph.o
lib/frama-c/structural_descr.cmx
lib/frama-c/structural_descr.o
+lib/frama-c/substitute_const_globals.cmx
+lib/frama-c/substitute_const_globals.o
lib/frama-c/task.cmx
lib/frama-c/task.o
lib/frama-c/tr_offset.cmx
@@ -393,6 +416,8 @@ lib/frama-c/vector.cmx
lib/frama-c/vector.o
lib/frama-c/visitor.cmx
lib/frama-c/visitor.o
+lib/frama-c/visitor_behavior.cmx
+lib/frama-c/visitor_behavior.o
lib/frama-c/warning_manager.cmx
lib/frama-c/warning_manager.o
lib/frama-c/wbox.cmx
Index: pkg/PLIST
===================================================================
RCS file: /cvs/ports/devel/frama-c/pkg/PLIST,v
diff -u -p -u -r1.6 PLIST
--- pkg/PLIST 11 Mar 2022 18:50:03 -0000 1.6
+++ pkg/PLIST 12 Jun 2026 01:22:29 -0000
@@ -1,25 +1,25 @@
%%native%%
bin/e-acsl-gcc.sh
@bin bin/frama-c
-@bin bin/frama-c-config
+bin/frama-c-config
@bin bin/frama-c-gui
@bin bin/frama-c-gui.byte
bin/frama-c-script
@bin bin/frama-c.byte
lib/frama-c/
-lib/frama-c/FCBuffer.cmi
-lib/frama-c/FCBuffer.cmo
lib/frama-c/FCHashtbl.cmi
lib/frama-c/FCHashtbl.cmo
-lib/frama-c/FCMap.cmi
-lib/frama-c/FCMap.cmo
-lib/frama-c/FCSet.cmi
-lib/frama-c/FCSet.cmo
lib/frama-c/GSourceView.cmi
lib/frama-c/GSourceView.cmo
lib/frama-c/META.frama-c
lib/frama-c/abstract_interp.cmi
lib/frama-c/abstract_interp.cmo
+lib/frama-c/abstract_memory.cmi
+lib/frama-c/abstract_memory.cmo
+lib/frama-c/abstract_offset.cmi
+lib/frama-c/abstract_offset.cmo
+lib/frama-c/acsl_extension.cmi
+lib/frama-c/acsl_extension.cmo
lib/frama-c/alarms.cmi
lib/frama-c/alarms.cmo
lib/frama-c/allocates.cmi
@@ -54,7 +54,6 @@ lib/frama-c/bottom.cmi
lib/frama-c/bottom.cmo
lib/frama-c/c_bindings.o
lib/frama-c/cabs.cmi
-lib/frama-c/cabs.cmo
lib/frama-c/cabs2cil.cmi
lib/frama-c/cabs2cil.cmo
lib/frama-c/cabs_debug.cmi
@@ -69,6 +68,10 @@ lib/frama-c/cil.cmi
lib/frama-c/cil.cmo
lib/frama-c/cilE.cmi
lib/frama-c/cilE.cmo
+lib/frama-c/cil_builder.cmi
+lib/frama-c/cil_builder.cmo
+lib/frama-c/cil_builtins.cmi
+lib/frama-c/cil_builtins.cmo
lib/frama-c/cil_const.cmi
lib/frama-c/cil_const.cmo
lib/frama-c/cil_datatype.cmi
@@ -92,8 +95,8 @@ lib/frama-c/cmdline.cmi
lib/frama-c/cmdline.cmo
lib/frama-c/command.cmi
lib/frama-c/command.cmo
-lib/frama-c/config.cmi
-lib/frama-c/config.cmo
+lib/frama-c/contract_special_float.cmi
+lib/frama-c/contract_special_float.cmo
lib/frama-c/cparser.cmi
lib/frama-c/cparser.cmo
lib/frama-c/cprint.cmi
@@ -108,8 +111,6 @@ lib/frama-c/datatype.cmi
lib/frama-c/datatype.cmo
lib/frama-c/db.cmi
lib/frama-c/db.cmo
-lib/frama-c/debug_manager.cmi
-lib/frama-c/debug_manager.cmo
lib/frama-c/descr.cmi
lib/frama-c/descr.cmo
lib/frama-c/description.cmi
@@ -118,23 +119,32 @@ lib/frama-c/design.cmi
lib/frama-c/design.cmo
lib/frama-c/destructors.cmi
lib/frama-c/destructors.cmo
-lib/frama-c/dgraph.cmi
-lib/frama-c/dgraph.cmo
-lib/frama-c/dllframa-c.so
+lib/frama-c/dgraph_helper.cmi
+lib/frama-c/dgraph_helper.cmo
+@so lib/frama-c/dllframa-c.so
lib/frama-c/dominators.cmi
lib/frama-c/dominators.cmo
+lib/frama-c/dotgraph.cmi
+lib/frama-c/dotgraph.cmo
+lib/frama-c/dump_config.cmi
+lib/frama-c/dump_config.cmo
lib/frama-c/dynamic.cmi
lib/frama-c/dynamic.cmo
+lib/frama-c/e-acsl/
+@static-lib lib/frama-c/e-acsl/libeacsl-dlmalloc.a
lib/frama-c/emitter.cmi
lib/frama-c/emitter.cmo
lib/frama-c/errorloc.cmi
lib/frama-c/errorloc.cmo
lib/frama-c/escape.cmi
lib/frama-c/escape.cmo
+lib/frama-c/eva_lattice_type.cmi
lib/frama-c/exn_flow.cmi
lib/frama-c/exn_flow.cmo
lib/frama-c/extlib.cmi
lib/frama-c/extlib.cmo
+lib/frama-c/fc_config.cmi
+lib/frama-c/fc_config.cmo
lib/frama-c/fc_float.cmi
lib/frama-c/fc_float.cmo
lib/frama-c/file.cmi
@@ -164,6 +174,10 @@ lib/frama-c/function_Froms.cmi
lib/frama-c/function_Froms.cmo
lib/frama-c/fval.cmi
lib/frama-c/fval.cmo
+lib/frama-c/ghost_accesses.cmi
+lib/frama-c/ghost_accesses.cmo
+lib/frama-c/ghost_cfg.cmi
+lib/frama-c/ghost_cfg.cmo
lib/frama-c/globals.cmi
lib/frama-c/globals.cmo
lib/frama-c/gtk_compat.cmi
@@ -200,6 +214,12 @@ lib/frama-c/int_Base.cmo
lib/frama-c/int_Intervals.cmi
lib/frama-c/int_Intervals.cmo
lib/frama-c/int_Intervals_sig.cmi
+lib/frama-c/int_interval.cmi
+lib/frama-c/int_interval.cmo
+lib/frama-c/int_set.cmi
+lib/frama-c/int_set.cmo
+lib/frama-c/int_val.cmi
+lib/frama-c/int_val.cmo
lib/frama-c/integer.cmi
lib/frama-c/integer.cmo
lib/frama-c/interpreted_automata.cmi
@@ -221,11 +241,9 @@ lib/frama-c/lattice_messages.cmo
lib/frama-c/lattice_type.cmi
lib/frama-c/launcher.cmi
lib/frama-c/launcher.cmo
-lib/frama-c/leftistheap.cmi
-lib/frama-c/leftistheap.cmo
lib/frama-c/lexerhack.cmi
lib/frama-c/lexerhack.cmo
-lib/frama-c/libframa-c.a
+@static-lib lib/frama-c/libframa-c.a
lib/frama-c/lmap.cmi
lib/frama-c/lmap.cmo
lib/frama-c/lmap_bitwise.cmi
@@ -262,12 +280,16 @@ lib/frama-c/machdeps.cmi
lib/frama-c/machdeps.cmo
lib/frama-c/map_lattice.cmi
lib/frama-c/map_lattice.cmo
+lib/frama-c/markdown.cmi
+lib/frama-c/markdown.cmo
lib/frama-c/menu_manager.cmi
lib/frama-c/menu_manager.cmo
lib/frama-c/mergecil.cmi
lib/frama-c/mergecil.cmo
lib/frama-c/messages.cmi
lib/frama-c/messages.cmo
+lib/frama-c/multidim.cmi
+lib/frama-c/multidim.cmo
lib/frama-c/offsetmap.cmi
lib/frama-c/offsetmap.cmo
lib/frama-c/offsetmap_bitwise_sig.cmi
@@ -300,20 +322,24 @@ lib/frama-c/plugins/
lib/frama-c/plugins/Aorai.cmi
lib/frama-c/plugins/Callgraph.cmi
lib/frama-c/plugins/Constant_Propagation.cmi
+lib/frama-c/plugins/Dive.cmi
lib/frama-c/plugins/E_ACSL.cmi
lib/frama-c/plugins/Eva.cmi
lib/frama-c/plugins/From.cmi
lib/frama-c/plugins/Impact.cmi
lib/frama-c/plugins/Inout.cmi
+lib/frama-c/plugins/Instantiate.cmi
lib/frama-c/plugins/LoopAnalysis.cmi
lib/frama-c/plugins/META.frama-c-aorai
lib/frama-c/plugins/META.frama-c-callgraph
lib/frama-c/plugins/META.frama-c-constant_propagation
+lib/frama-c/plugins/META.frama-c-dive
lib/frama-c/plugins/META.frama-c-e_acsl
lib/frama-c/plugins/META.frama-c-eva
lib/frama-c/plugins/META.frama-c-from
lib/frama-c/plugins/META.frama-c-impact
lib/frama-c/plugins/META.frama-c-inout
+lib/frama-c/plugins/META.frama-c-instantiate
lib/frama-c/plugins/META.frama-c-loopanalysis
lib/frama-c/plugins/META.frama-c-metrics
lib/frama-c/plugins/META.frama-c-nonterm
@@ -323,16 +349,17 @@ lib/frama-c/plugins/META.frama-c-pdg
lib/frama-c/plugins/META.frama-c-postdominators
lib/frama-c/plugins/META.frama-c-print_api
lib/frama-c/plugins/META.frama-c-qed
+lib/frama-c/plugins/META.frama-c-reduc
lib/frama-c/plugins/META.frama-c-report
lib/frama-c/plugins/META.frama-c-rtegen
lib/frama-c/plugins/META.frama-c-scope
lib/frama-c/plugins/META.frama-c-security_slicing
+lib/frama-c/plugins/META.frama-c-server
lib/frama-c/plugins/META.frama-c-slicing
lib/frama-c/plugins/META.frama-c-sparecode
lib/frama-c/plugins/META.frama-c-studia
lib/frama-c/plugins/META.frama-c-users
lib/frama-c/plugins/META.frama-c-variadic
-lib/frama-c/plugins/META.frama-c-wp
lib/frama-c/plugins/Metrics.cmi
lib/frama-c/plugins/Nonterm.cmi
lib/frama-c/plugins/Obfuscator.cmi
@@ -341,16 +368,17 @@ lib/frama-c/plugins/Pdg.cmi
lib/frama-c/plugins/Postdominators.cmi
lib/frama-c/plugins/Print_api.cmi
lib/frama-c/plugins/Qed.cmi
+lib/frama-c/plugins/Reduc.cmi
lib/frama-c/plugins/Report.cmi
lib/frama-c/plugins/RteGen.cmi
lib/frama-c/plugins/Scope.cmi
lib/frama-c/plugins/Security_slicing.cmi
+lib/frama-c/plugins/Server.cmi
lib/frama-c/plugins/Slicing.cmi
lib/frama-c/plugins/Sparecode.cmi
lib/frama-c/plugins/Studia.cmi
lib/frama-c/plugins/Users.cmi
lib/frama-c/plugins/Variadic.cmi
-lib/frama-c/plugins/Wp.cmi
lib/frama-c/plugins/gui/
lib/frama-c/plugins/gui/Eva.cmi
lib/frama-c/plugins/gui/Eva.cmo
@@ -362,8 +390,6 @@ lib/frama-c/plugins/gui/Metrics.cmi
lib/frama-c/plugins/gui/Metrics.cmo
lib/frama-c/plugins/gui/Occurrence.cmi
lib/frama-c/plugins/gui/Occurrence.cmo
-lib/frama-c/plugins/gui/Qed.cmi
-lib/frama-c/plugins/gui/Qed.cmo
lib/frama-c/plugins/gui/Scope.cmi
lib/frama-c/plugins/gui/Scope.cmo
lib/frama-c/plugins/gui/Security_slicing.cmi
@@ -372,17 +398,17 @@ lib/frama-c/plugins/gui/Slicing.cmi
lib/frama-c/plugins/gui/Slicing.cmo
lib/frama-c/plugins/gui/Studia.cmi
lib/frama-c/plugins/gui/Studia.cmo
-lib/frama-c/plugins/gui/Wp.cmi
-lib/frama-c/plugins/gui/Wp.cmo
lib/frama-c/plugins/top/
lib/frama-c/plugins/top/Aorai.cmo
lib/frama-c/plugins/top/Callgraph.cmo
lib/frama-c/plugins/top/Constant_Propagation.cmo
+lib/frama-c/plugins/top/Dive.cmo
lib/frama-c/plugins/top/E_ACSL.cmo
lib/frama-c/plugins/top/Eva.cmo
lib/frama-c/plugins/top/From.cmo
lib/frama-c/plugins/top/Impact.cmo
lib/frama-c/plugins/top/Inout.cmo
+lib/frama-c/plugins/top/Instantiate.cmo
lib/frama-c/plugins/top/LoopAnalysis.cmo
lib/frama-c/plugins/top/Metrics.cmo
lib/frama-c/plugins/top/Nonterm.cmo
@@ -392,16 +418,17 @@ lib/frama-c/plugins/top/Pdg.cmo
lib/frama-c/plugins/top/Postdominators.cmo
lib/frama-c/plugins/top/Print_api.cmo
lib/frama-c/plugins/top/Qed.cmo
+lib/frama-c/plugins/top/Reduc.cmo
lib/frama-c/plugins/top/Report.cmo
lib/frama-c/plugins/top/RteGen.cmo
lib/frama-c/plugins/top/Scope.cmo
lib/frama-c/plugins/top/Security_slicing.cmo
+lib/frama-c/plugins/top/Server.cmo
lib/frama-c/plugins/top/Slicing.cmo
lib/frama-c/plugins/top/Sparecode.cmo
lib/frama-c/plugins/top/Studia.cmo
lib/frama-c/plugins/top/Users.cmo
lib/frama-c/plugins/top/Variadic.cmo
-lib/frama-c/plugins/top/Wp.cmo
lib/frama-c/precise_locs.cmi
lib/frama-c/precise_locs.cmo
lib/frama-c/pretty_source.cmi
@@ -464,6 +491,8 @@ lib/frama-c/stmts_graph.cmi
lib/frama-c/stmts_graph.cmo
lib/frama-c/structural_descr.cmi
lib/frama-c/structural_descr.cmo
+lib/frama-c/substitute_const_globals.cmi
+lib/frama-c/substitute_const_globals.cmo
lib/frama-c/task.cmi
lib/frama-c/task.cmo
lib/frama-c/tr_offset.cmi
@@ -494,6 +523,8 @@ lib/frama-c/vector.cmi
lib/frama-c/vector.cmo
lib/frama-c/visitor.cmi
lib/frama-c/visitor.cmo
+lib/frama-c/visitor_behavior.cmi
+lib/frama-c/visitor_behavior.cmo
lib/frama-c/warning_manager.cmi
lib/frama-c/warning_manager.cmo
lib/frama-c/wbox.cmi
@@ -521,8 +552,6 @@ lib/frama-c/wutil.cmi
lib/frama-c/wutil.cmo
lib/frama-c/wutil_once.cmi
lib/frama-c/wutil_once.cmo
-lib/libeacsl-dlmalloc.a
-lib/libeacsl-gmp.a
@man man/man1/e-acsl-gcc.sh.1
@man man/man1/frama-c-gui.1
@man man/man1/frama-c.1
@@ -536,30 +565,38 @@ share/frama-c/Makefile.plugin.template
share/frama-c/_frama-c
share/frama-c/analysis-scripts/
share/frama-c/analysis-scripts/README.md
+share/frama-c/analysis-scripts/analysis.mk
share/frama-c/analysis-scripts/benchmark_database.py
share/frama-c/analysis-scripts/clone.sh
share/frama-c/analysis-scripts/cmd-dep.sh
share/frama-c/analysis-scripts/concat-csv.sh
-share/frama-c/analysis-scripts/examples/
-share/frama-c/analysis-scripts/examples/Makefile
-share/frama-c/analysis-scripts/examples/example-multi.mk
-share/frama-c/analysis-scripts/examples/example-slevel.mk
-share/frama-c/analysis-scripts/examples/example.c
-share/frama-c/analysis-scripts/examples/example.mk
+share/frama-c/analysis-scripts/creduce.sh
+share/frama-c/analysis-scripts/epilogue.mk
share/frama-c/analysis-scripts/fc_stubs.c
share/frama-c/analysis-scripts/find_fun.py
share/frama-c/analysis-scripts/flamegraph.pl
-share/frama-c/analysis-scripts/frama-c.mk
share/frama-c/analysis-scripts/frama_c_results.py
+share/frama-c/analysis-scripts/function_finder.py
share/frama-c/analysis-scripts/git_utils.py
share/frama-c/analysis-scripts/list_files.py
+share/frama-c/analysis-scripts/list_functions.ml
+share/frama-c/analysis-scripts/make_template.py
share/frama-c/analysis-scripts/make_wrapper.py
+share/frama-c/analysis-scripts/normalize_jcdb.py
share/frama-c/analysis-scripts/parse-coverage.sh
+share/frama-c/analysis-scripts/prologue.mk
share/frama-c/analysis-scripts/results_display.py
+share/frama-c/analysis-scripts/script_for_creduce_fatal.sh
+share/frama-c/analysis-scripts/script_for_creduce_non_fatal.sh
share/frama-c/analysis-scripts/summary.py
share/frama-c/analysis-scripts/template.mk
share/frama-c/autocomplete_frama-c
-share/frama-c/builtin.h
+share/frama-c/compliance/
+share/frama-c/compliance/c11_functions.json
+share/frama-c/compliance/c11_headers.json
+share/frama-c/compliance/glibc_functions.json
+share/frama-c/compliance/nonstandard_identifiers.json
+share/frama-c/compliance/posix_identifiers.json
share/frama-c/configure.ac
share/frama-c/doc/
share/frama-c/doc/code/
@@ -571,33 +608,76 @@ share/frama-c/doc/code/style.css
share/frama-c/doc/code/toc_head.htm
share/frama-c/doc/code/toc_tail.htm
share/frama-c/e-acsl/
-share/frama-c/e-acsl/bittree_model/
-share/frama-c/e-acsl/bittree_model/e_acsl_bittree.h
-share/frama-c/e-acsl/bittree_model/e_acsl_bittree_api.h
-share/frama-c/e-acsl/bittree_model/e_acsl_bittree_mmodel.c
+share/frama-c/e-acsl/contrib/
+share/frama-c/e-acsl/contrib/libdlmalloc/
+share/frama-c/e-acsl/contrib/libdlmalloc/dlmalloc.c
share/frama-c/e-acsl/e_acsl.h
-share/frama-c/e-acsl/e_acsl_alias.h
-share/frama-c/e-acsl/e_acsl_assert.h
-share/frama-c/e-acsl/e_acsl_bits.h
-share/frama-c/e-acsl/e_acsl_debug.h
-share/frama-c/e-acsl/e_acsl_floating_point.h
-share/frama-c/e-acsl/e_acsl_format.h
-share/frama-c/e-acsl/e_acsl_gmp_api.h
-share/frama-c/e-acsl/e_acsl_leak.h
-share/frama-c/e-acsl/e_acsl_libc_replacements.h
-share/frama-c/e-acsl/e_acsl_malloc.h
-share/frama-c/e-acsl/e_acsl_printf.h
share/frama-c/e-acsl/e_acsl_rtl.c
-share/frama-c/e-acsl/e_acsl_safe_locations.h
-share/frama-c/e-acsl/e_acsl_shexec.h
-share/frama-c/e-acsl/e_acsl_string.h
-share/frama-c/e-acsl/e_acsl_temporal.h
-share/frama-c/e-acsl/e_acsl_temporal_timestamp.h
-share/frama-c/e-acsl/e_acsl_trace.h
-share/frama-c/e-acsl/segment_model/
-share/frama-c/e-acsl/segment_model/e_acsl_segment_mmodel.c
-share/frama-c/e-acsl/segment_model/e_acsl_segment_tracking.h
-share/frama-c/e-acsl/segment_model/e_acsl_shadow_layout.h
+share/frama-c/e-acsl/instrumentation_model/
+share/frama-c/e-acsl/instrumentation_model/e_acsl_assert.c
+share/frama-c/e-acsl/instrumentation_model/e_acsl_assert.h
+share/frama-c/e-acsl/instrumentation_model/e_acsl_assert_data.h
+share/frama-c/e-acsl/instrumentation_model/e_acsl_assert_data_api.c
+share/frama-c/e-acsl/instrumentation_model/e_acsl_assert_data_api.h
+share/frama-c/e-acsl/instrumentation_model/e_acsl_contract.c
+share/frama-c/e-acsl/instrumentation_model/e_acsl_contract.h
+share/frama-c/e-acsl/instrumentation_model/e_acsl_temporal.c
+share/frama-c/e-acsl/instrumentation_model/e_acsl_temporal.h
+share/frama-c/e-acsl/instrumentation_model/e_acsl_temporal_timestamp.h
+share/frama-c/e-acsl/internals/
+share/frama-c/e-acsl/internals/e_acsl_alias.h
+share/frama-c/e-acsl/internals/e_acsl_bits.c
+share/frama-c/e-acsl/internals/e_acsl_bits.h
+share/frama-c/e-acsl/internals/e_acsl_config.h
+share/frama-c/e-acsl/internals/e_acsl_debug.c
+share/frama-c/e-acsl/internals/e_acsl_debug.h
+share/frama-c/e-acsl/internals/e_acsl_malloc.c
+share/frama-c/e-acsl/internals/e_acsl_malloc.h
+share/frama-c/e-acsl/internals/e_acsl_private_assert.c
+share/frama-c/e-acsl/internals/e_acsl_private_assert.h
+share/frama-c/e-acsl/internals/e_acsl_rtl_io.c
+share/frama-c/e-acsl/internals/e_acsl_rtl_io.h
+share/frama-c/e-acsl/internals/e_acsl_rtl_string.c
+share/frama-c/e-acsl/internals/e_acsl_rtl_string.h
+share/frama-c/e-acsl/internals/e_acsl_shexec.c
+share/frama-c/e-acsl/internals/e_acsl_shexec.h
+share/frama-c/e-acsl/internals/e_acsl_trace.c
+share/frama-c/e-acsl/internals/e_acsl_trace.h
+share/frama-c/e-acsl/libc_replacements/
+share/frama-c/e-acsl/libc_replacements/e_acsl_stdio.c
+share/frama-c/e-acsl/libc_replacements/e_acsl_stdio.h
+share/frama-c/e-acsl/libc_replacements/e_acsl_string.c
+share/frama-c/e-acsl/libc_replacements/e_acsl_string.h
+share/frama-c/e-acsl/numerical_model/
+share/frama-c/e-acsl/numerical_model/e_acsl_floating_point.c
+share/frama-c/e-acsl/numerical_model/e_acsl_floating_point.h
+share/frama-c/e-acsl/numerical_model/e_acsl_gmp_api.h
+share/frama-c/e-acsl/observation_model/
+share/frama-c/e-acsl/observation_model/bittree_model/
+share/frama-c/e-acsl/observation_model/bittree_model/e_acsl_bittree.c
+share/frama-c/e-acsl/observation_model/bittree_model/e_acsl_bittree.h
+share/frama-c/e-acsl/observation_model/bittree_model/e_acsl_bittree_observation_model.c
+share/frama-c/e-acsl/observation_model/bittree_model/e_acsl_bittree_omodel_debug.c
+share/frama-c/e-acsl/observation_model/bittree_model/e_acsl_bittree_timestamp_retrieval.c
+share/frama-c/e-acsl/observation_model/e_acsl_heap.c
+share/frama-c/e-acsl/observation_model/e_acsl_heap.h
+share/frama-c/e-acsl/observation_model/e_acsl_observation_model.c
+share/frama-c/e-acsl/observation_model/e_acsl_observation_model.h
+share/frama-c/e-acsl/observation_model/internals/
+share/frama-c/e-acsl/observation_model/internals/e_acsl_heap_tracking.c
+share/frama-c/e-acsl/observation_model/internals/e_acsl_heap_tracking.h
+share/frama-c/e-acsl/observation_model/internals/e_acsl_omodel_debug.h
+share/frama-c/e-acsl/observation_model/internals/e_acsl_safe_locations.c
+share/frama-c/e-acsl/observation_model/internals/e_acsl_safe_locations.h
+share/frama-c/e-acsl/observation_model/internals/e_acsl_timestamp_retrieval.h
+share/frama-c/e-acsl/observation_model/segment_model/
+share/frama-c/e-acsl/observation_model/segment_model/e_acsl_segment_observation_model.c
+share/frama-c/e-acsl/observation_model/segment_model/e_acsl_segment_omodel_debug.c
+share/frama-c/e-acsl/observation_model/segment_model/e_acsl_segment_timestamp_retrieval.c
+share/frama-c/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.c
+share/frama-c/e-acsl/observation_model/segment_model/e_acsl_segment_tracking.h
+share/frama-c/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.c
+share/frama-c/e-acsl/observation_model/segment_model/e_acsl_shadow_layout.h
share/frama-c/emacs/
share/frama-c/emacs/acsl.el
share/frama-c/emacs/frama-c-dev.el
@@ -617,13 +697,16 @@ share/frama-c/libc/__fc_define_clockid_t
share/frama-c/libc/__fc_define_dev_t.h
share/frama-c/libc/__fc_define_eof.h
share/frama-c/libc/__fc_define_fd_set_t.h
+share/frama-c/libc/__fc_define_fds.h
share/frama-c/libc/__fc_define_file.h
share/frama-c/libc/__fc_define_fpos_t.h
+share/frama-c/libc/__fc_define_fs_cnt.h
share/frama-c/libc/__fc_define_id_t.h
share/frama-c/libc/__fc_define_ino_t.h
share/frama-c/libc/__fc_define_intptr_t.h
share/frama-c/libc/__fc_define_iovec.h
share/frama-c/libc/__fc_define_key_t.h
+share/frama-c/libc/__fc_define_max_open_files.h
share/frama-c/libc/__fc_define_mode_t.h
share/frama-c/libc/__fc_define_nlink_t.h
share/frama-c/libc/__fc_define_null.h
@@ -641,18 +724,23 @@ share/frama-c/libc/__fc_define_suseconds
share/frama-c/libc/__fc_define_time_t.h
share/frama-c/libc/__fc_define_timer_t.h
share/frama-c/libc/__fc_define_timespec.h
+share/frama-c/libc/__fc_define_timeval.h
share/frama-c/libc/__fc_define_uid_and_gid.h
share/frama-c/libc/__fc_define_useconds_t.h
share/frama-c/libc/__fc_define_wchar_t.h
share/frama-c/libc/__fc_define_wint_t.h
share/frama-c/libc/__fc_gcc_builtins.h
share/frama-c/libc/__fc_inet.h
+share/frama-c/libc/__fc_integer.h
+share/frama-c/libc/__fc_libc.h
share/frama-c/libc/__fc_machdep.h
share/frama-c/libc/__fc_machdep_linux_shared.h
share/frama-c/libc/__fc_runtime.c
share/frama-c/libc/__fc_select.h
share/frama-c/libc/__fc_string_axiomatic.h
share/frama-c/libc/alloca.h
+share/frama-c/libc/argz.c
+share/frama-c/libc/argz.h
share/frama-c/libc/arpa/
share/frama-c/libc/arpa/inet.h
share/frama-c/libc/assert.c
@@ -672,6 +760,7 @@ share/frama-c/libc/fenv.c
share/frama-c/libc/fenv.h
share/frama-c/libc/float.h
share/frama-c/libc/fnmatch.h
+share/frama-c/libc/ftw.h
share/frama-c/libc/getopt.c
share/frama-c/libc/getopt.h
share/frama-c/libc/glob.c
@@ -695,7 +784,9 @@ share/frama-c/libc/net/if.h
share/frama-c/libc/netdb.c
share/frama-c/libc/netdb.h
share/frama-c/libc/netinet/
+share/frama-c/libc/netinet/in.c
share/frama-c/libc/netinet/in.h
+share/frama-c/libc/netinet/ip.h
share/frama-c/libc/netinet/tcp.h
share/frama-c/libc/nl_types.h
share/frama-c/libc/poll.h
@@ -709,6 +800,8 @@ share/frama-c/libc/setjmp.h
share/frama-c/libc/signal.c
share/frama-c/libc/signal.h
share/frama-c/libc/stdarg.h
+share/frama-c/libc/stdatomic.c
+share/frama-c/libc/stdatomic.h
share/frama-c/libc/stdbool.h
share/frama-c/libc/stddef.h
share/frama-c/libc/stdint.h
@@ -725,13 +818,16 @@ share/frama-c/libc/sys/file.h
share/frama-c/libc/sys/ioctl.h
share/frama-c/libc/sys/ipc.h
share/frama-c/libc/sys/mman.h
+share/frama-c/libc/sys/param.h
share/frama-c/libc/sys/random.h
share/frama-c/libc/sys/resource.h
share/frama-c/libc/sys/select.h
+share/frama-c/libc/sys/sendfile.h
share/frama-c/libc/sys/shm.h
share/frama-c/libc/sys/signal.h
share/frama-c/libc/sys/socket.h
share/frama-c/libc/sys/stat.h
+share/frama-c/libc/sys/statvfs.h
share/frama-c/libc/sys/time.h
share/frama-c/libc/sys/times.h
share/frama-c/libc/sys/timex.h
@@ -739,14 +835,17 @@ share/frama-c/libc/sys/types.h
share/frama-c/libc/sys/uio.h
share/frama-c/libc/sys/un.h
share/frama-c/libc/sys/utsname.h
+share/frama-c/libc/sys/vfs.h
share/frama-c/libc/sys/wait.h
share/frama-c/libc/syslog.h
share/frama-c/libc/termios.h
share/frama-c/libc/tgmath.h
share/frama-c/libc/time.c
share/frama-c/libc/time.h
+share/frama-c/libc/unistd.c
share/frama-c/libc/unistd.h
share/frama-c/libc/utime.h
+share/frama-c/libc/utmp.h
share/frama-c/libc/utmpx.h
share/frama-c/libc/wchar.c
share/frama-c/libc/wchar.h
@@ -821,6 +920,8 @@ share/frama-c/wp/coqwp/bool/Bool.v
share/frama-c/wp/coqwp/int/
share/frama-c/wp/coqwp/int/Abs.v
share/frama-c/wp/coqwp/int/ComputerDivision.v
+share/frama-c/wp/coqwp/int/ComputerOfEuclideanDivision.v
+share/frama-c/wp/coqwp/int/EuclideanDivision.v
share/frama-c/wp/coqwp/int/Exponentiation.v
share/frama-c/wp/coqwp/int/Int.v
share/frama-c/wp/coqwp/int/MinMax.v
@@ -853,6 +954,7 @@ share/frama-c/wp/ergo/Vset.mlw
share/frama-c/wp/ergo/bool.Bool.mlw
share/frama-c/wp/ergo/int.Abs.mlw
share/frama-c/wp/ergo/int.ComputerDivision.mlw
+share/frama-c/wp/ergo/int.ComputerOfEuclideanDivision.mlw
share/frama-c/wp/ergo/int.Int.mlw
share/frama-c/wp/ergo/int.MinMax.mlw
share/frama-c/wp/ergo/map.Const.mlw
@@ -870,31 +972,13 @@ share/frama-c/wp/ergo/real.Square.mlw
share/frama-c/wp/ergo/real.Trigonometry.mlw
share/frama-c/wp/ergo/real.Truncate.mlw
share/frama-c/wp/why3/
-share/frama-c/wp/why3/ArcTrigo.v
-share/frama-c/wp/why3/ArcTrigo.why
-share/frama-c/wp/why3/Bits.v
-share/frama-c/wp/why3/Cbits.v
-share/frama-c/wp/why3/Cbits.why
-share/frama-c/wp/why3/Cfloat.v
-share/frama-c/wp/why3/Cfloat.why
-share/frama-c/wp/why3/Cint.v
-share/frama-c/wp/why3/Cint.why
-share/frama-c/wp/why3/Cmath.v
-share/frama-c/wp/why3/Cmath.why
-share/frama-c/wp/why3/ExpLog.v
-share/frama-c/wp/why3/ExpLog.why
-share/frama-c/wp/why3/Memory.v
-share/frama-c/wp/why3/Memory.why
-share/frama-c/wp/why3/Qed.v
-share/frama-c/wp/why3/Qed.why
-share/frama-c/wp/why3/Qedlib.v
-share/frama-c/wp/why3/Square.v
-share/frama-c/wp/why3/Square.why
-share/frama-c/wp/why3/Vlist.v
-share/frama-c/wp/why3/Vlist.why
-share/frama-c/wp/why3/Vset.v
-share/frama-c/wp/why3/Vset.why
-share/frama-c/wp/why3/Zbits.v
-share/frama-c/wp/why3/coq.drv
-share/frama-c/wp/why3/why3.conf
+share/frama-c/wp/why3/frama_c_wp/
+share/frama-c/wp/why3/frama_c_wp/cbits.mlw
+share/frama-c/wp/why3/frama_c_wp/cfloat.mlw
+share/frama-c/wp/why3/frama_c_wp/cint.mlw
+share/frama-c/wp/why3/frama_c_wp/cmath.mlw
+share/frama-c/wp/why3/frama_c_wp/memory.mlw
+share/frama-c/wp/why3/frama_c_wp/qed.mlw
+share/frama-c/wp/why3/frama_c_wp/vlist.mlw
+share/frama-c/wp/why3/frama_c_wp/vset.mlw
share/frama-c/wp/wp.driver
[update] devel/frama-c 19.0 -> 24.0