From: Daniel Dickman Subject: [update] devel/frama-c 19.0 -> 24.0 To: ports@openbsd.org Date: Thu, 11 Jun 2026 21:23:46 -0400 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