From: Daniel Dickman <didickman@gmail.com>
Subject: [update] devel/frama-c 19.0 -> 20.0
To: ports@openbsd.org
Date: Sun, 29 Jun 2025 20:14:48 -0400

I'd like to update frama-c from 19.0 -> 20.0.

ok on this update? The local patches were upstreamed and can go away.

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	27 Jun 2025 21:45:23 -0000
@@ -7,9 +7,8 @@ COMMENT =		extensible platform for analy
 CATEGORIES =		devel
 GH_ACCOUNT =		Frama-C
 GH_PROJECT =		Frama-C-snapshot
-GH_TAGNAME =		19.0
-REVISION =		8
-DISTNAME =		frama-c-${GH_TAGNAME}-Potassium
+GH_TAGNAME =		20.0
+DISTNAME =		frama-c-${GH_TAGNAME}-Calcium
 PKGNAME =		frama-c-${GH_TAGNAME}
 
 HOMEPAGE =		https://frama-c.com/
@@ -19,8 +18,8 @@ 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
 
 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	27 Jun 2025 21:45:23 -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-20.0-Calcium.tar.gz) = m5HuWGHgXgqaSkY6G9Mr7ttlN2H6uVAhskmmsHYwnfs=
+SIZE (frama-c-20.0-Calcium.tar.gz) = 5869359
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	27 Jun 2025 21:45:23 -0000
@@ -1,38 +1,37 @@
-@bin lib/frama-c/plugins/gui/Eva.cmxs
-@bin lib/frama-c/plugins/gui/From.cmxs
-@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/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/LoopAnalysis.cmxs
-@bin lib/frama-c/plugins/top/Metrics.cmxs
-@bin lib/frama-c/plugins/top/Nonterm.cmxs
-@bin lib/frama-c/plugins/top/Obfuscator.cmxs
-@bin lib/frama-c/plugins/top/Occurrence.cmxs
-@bin lib/frama-c/plugins/top/Pdg.cmxs
-@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/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/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
+lib/frama-c/plugins/gui/Eva.cmxs
+lib/frama-c/plugins/gui/From.cmxs
+lib/frama-c/plugins/gui/Impact.cmxs
+lib/frama-c/plugins/gui/Metrics.cmxs
+lib/frama-c/plugins/gui/Occurrence.cmxs
+lib/frama-c/plugins/gui/Qed.cmxs
+lib/frama-c/plugins/gui/Scope.cmxs
+lib/frama-c/plugins/gui/Security_slicing.cmxs
+lib/frama-c/plugins/gui/Slicing.cmxs
+lib/frama-c/plugins/gui/Studia.cmxs
+lib/frama-c/plugins/top/Aorai.cmxs
+lib/frama-c/plugins/top/Callgraph.cmxs
+lib/frama-c/plugins/top/Constant_Propagation.cmxs
+lib/frama-c/plugins/top/E_ACSL.cmxs
+lib/frama-c/plugins/top/Eva.cmxs
+lib/frama-c/plugins/top/From.cmxs
+lib/frama-c/plugins/top/Impact.cmxs
+lib/frama-c/plugins/top/Inout.cmxs
+lib/frama-c/plugins/top/LoopAnalysis.cmxs
+lib/frama-c/plugins/top/Metrics.cmxs
+lib/frama-c/plugins/top/Nonterm.cmxs
+lib/frama-c/plugins/top/Obfuscator.cmxs
+lib/frama-c/plugins/top/Occurrence.cmxs
+lib/frama-c/plugins/top/Pdg.cmxs
+lib/frama-c/plugins/top/Postdominators.cmxs
+lib/frama-c/plugins/top/Print_api.cmxs
+lib/frama-c/plugins/top/Qed.cmxs
+lib/frama-c/plugins/top/Report.cmxs
+lib/frama-c/plugins/top/RteGen.cmxs
+lib/frama-c/plugins/top/Scope.cmxs
+lib/frama-c/plugins/top/Security_slicing.cmxs
+lib/frama-c/plugins/top/Server.cmxs
+lib/frama-c/plugins/top/Slicing.cmxs
+lib/frama-c/plugins/top/Sparecode.cmxs
+lib/frama-c/plugins/top/Studia.cmxs
+lib/frama-c/plugins/top/Users.cmxs
+lib/frama-c/plugins/top/Variadic.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	27 Jun 2025 21:45:23 -0000
@@ -98,8 +98,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 +106,12 @@ 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/dynamic.cmx
 lib/frama-c/dynamic.o
 lib/frama-c/emitter.cmx
@@ -206,8 +206,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,6 +242,8 @@ 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
@@ -295,12 +295,12 @@ 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
@@ -393,6 +393,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	27 Jun 2025 21:45:23 -0000
@@ -108,8 +108,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,11 +116,13 @@ 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/dynamic.cmi
 lib/frama-c/dynamic.cmo
 lib/frama-c/emitter.cmi
@@ -221,11 +221,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,6 +260,8 @@ 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
@@ -327,12 +327,12 @@ 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
@@ -345,12 +345,12 @@ 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
@@ -372,8 +372,6 @@ 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
@@ -396,12 +394,12 @@ 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
@@ -494,6 +492,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 +521,7 @@ 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
+@static-lib lib/libeacsl-dlmalloc.a
 @man man/man1/e-acsl-gcc.sh.1
 @man man/man1/frama-c-gui.1
 @man man/man1/frama-c.1
@@ -553,13 +552,18 @@ share/frama-c/analysis-scripts/frama-c.m
 share/frama-c/analysis-scripts/frama_c_results.py
 share/frama-c/analysis-scripts/git_utils.py
 share/frama-c/analysis-scripts/list_files.py
+share/frama-c/analysis-scripts/make_template.py
 share/frama-c/analysis-scripts/make_wrapper.py
 share/frama-c/analysis-scripts/parse-coverage.sh
 share/frama-c/analysis-scripts/results_display.py
 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/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/
@@ -647,6 +651,7 @@ 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_machdep.h
 share/frama-c/libc/__fc_machdep_linux_shared.h
 share/frama-c/libc/__fc_runtime.c
@@ -672,6 +677,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
@@ -821,6 +827,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 +861,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 +879,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