Download raw body.
[update] devel/frama-c 19.0 -> 20.0
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
[update] devel/frama-c 19.0 -> 20.0