Simple upgrade from Sodium to Magnesium, which now builds with our <fenv.h>.
Index: Makefile =================================================================== RCS file: /OpenBSD/ports/devel/frama-c/Makefile,v retrieving revision 1.7 diff -u -p -r1.7 Makefile --- Makefile 30 Aug 2015 16:22:15 -0000 1.7 +++ Makefile 9 Apr 2016 21:53:29 -0000 @@ -6,8 +6,8 @@ COMMENT = an extensible platform for an BROKEN-powerpc = Error while linking /usr/local/lib/ocaml/vmthreads/stdlib.cma BROKEN-alpha = Error while linking /usr/local/lib/ocaml/vmthreads/stdlib.cma -DISTNAME = frama-c-Sodium-20150201 -PKGNAME = frama-c-1.11 +DISTNAME = frama-c-Magnesium-20151002 +PKGNAME = frama-c-1.12 CATEGORIES = devel HOMEPAGE = http://www.frama-c.com/ Index: distinfo =================================================================== RCS file: /OpenBSD/ports/devel/frama-c/distinfo,v retrieving revision 1.2 diff -u -p -r1.2 distinfo --- distinfo 30 Aug 2015 16:22:15 -0000 1.2 +++ distinfo 9 Apr 2016 21:53:29 -0000 @@ -1,2 +1,2 @@ -SHA256 (frama-c-Sodium-20150201.tar.gz) = WHXYawwmnTSK+kYC8Mp/5raFYZH9twPY6wvJDUyYWn0= -SIZE (frama-c-Sodium-20150201.tar.gz) = 6155507 +SHA256 (frama-c-Magnesium-20151002.tar.gz) = Fh9lvWbtX+ECBUYtU00bOHrHJ2Zs2XTM1J0UpQSSaB4= +SIZE (frama-c-Magnesium-20151002.tar.gz) = 6330931 Index: patches/patch-src_buckx_buckx_c_c =================================================================== RCS file: patches/patch-src_buckx_buckx_c_c diff -N patches/patch-src_buckx_buckx_c_c --- patches/patch-src_buckx_buckx_c_c 21 Apr 2014 16:02:26 -0000 1.1.1.1 +++ /dev/null 1 Jan 1970 00:00:00 -0000 @@ -1,14 +0,0 @@ -$OpenBSD: patch-src_buckx_buckx_c_c,v 1.1.1.1 2014/04/21 16:02:26 jca Exp $ ---- src/buckx/buckx_c.c.orig Fri Apr 18 10:56:21 2014 -+++ src/buckx/buckx_c.c Fri Apr 18 10:57:30 2014 -@@ -153,8 +153,8 @@ value single_precision_of_string(value str) - value terminate_process(value v) - { - long pid = Long_val(v); --#if _POSIX_C_SOURCE >= 1 || _XOPEN_SOURCE || _POSIX_SOURCE || __ENVIRONMENT_MAC_OS_X_VERSION_MIN_REQUIRED__ -- kill(pid,9); -+#if 1 || _POSIX_C_SOURCE >= 1 || _XOPEN_SOURCE || _POSIX_SOURCE || __ENVIRONMENT_MAC_OS_X_VERSION_MIN_REQUIRED__ -+ kill(pid,15); - #else - #ifdef _WIN32 - TerminateProcess((HANDLE)pid,9); Index: patches/patch-src_libraries_utils_c_bindings_c =================================================================== RCS file: patches/patch-src_libraries_utils_c_bindings_c diff -N patches/patch-src_libraries_utils_c_bindings_c --- /dev/null 1 Jan 1970 00:00:00 -0000 +++ patches/patch-src_libraries_utils_c_bindings_c 9 Apr 2016 21:53:29 -0000 @@ -0,0 +1,23 @@ +$OpenBSD$ +--- src/libraries/utils/c_bindings.c.orig Thu Jan 14 16:30:26 2016 ++++ src/libraries/utils/c_bindings.c Sat Apr 9 21:11:25 2016 +@@ -36,7 +36,7 @@ + #include <unistd.h> + + // Some BSD flavors do not implement all of C99 +-#if defined(__OpenBSD__) || defined(__NetBSD__) ++#if defined(__NetBSD__) + # include <ieeefp.h> + # define FE_DOWNWARD FP_RM + # define FE_UPWARD FP_RP +@@ -242,8 +242,8 @@ value single_precision_of_string(value str) + value terminate_process(value v) + { + long pid = Long_val(v); +-#if _POSIX_C_SOURCE >= 1 || _XOPEN_SOURCE || _POSIX_SOURCE || __ENVIRONMENT_MAC_OS_X_VERSION_MIN_REQUIRED__ +- kill(pid,9); ++#if 1 || _POSIX_C_SOURCE >= 1 || _XOPEN_SOURCE || _POSIX_SOURCE || __ENVIRONMENT_MAC_OS_X_VERSION_MIN_REQUIRED__ ++ kill(pid,15); + #else + #ifdef _WIN32 + TerminateProcess((HANDLE)pid,9); Index: pkg/PFRAG.dynlink-native =================================================================== RCS file: /OpenBSD/ports/devel/frama-c/pkg/PFRAG.dynlink-native,v retrieving revision 1.2 diff -u -p -r1.2 PFRAG.dynlink-native --- pkg/PFRAG.dynlink-native 23 Apr 2014 14:12:28 -0000 1.2 +++ pkg/PFRAG.dynlink-native 9 Apr 2016 21:53:29 -0000 @@ -1,8 +1,30 @@ @comment $OpenBSD: PFRAG.dynlink-native,v 1.2 2014/04/23 14:12:28 jca Exp $ @bin lib/frama-c/plugins/Aorai.cmxs +@bin lib/frama-c/plugins/Callgraph.cmxs +@bin lib/frama-c/plugins/Callgraph_gui.cmxs +@bin lib/frama-c/plugins/Constant_Propagation.cmxs +@bin lib/frama-c/plugins/From.cmxs +@bin lib/frama-c/plugins/Impact.cmxs +@bin lib/frama-c/plugins/Inout.cmxs +@bin lib/frama-c/plugins/Metrics.cmxs @bin lib/frama-c/plugins/Obfuscator.cmxs +@bin lib/frama-c/plugins/Occurrence.cmxs +@bin lib/frama-c/plugins/Pdg.cmxs @bin lib/frama-c/plugins/Report.cmxs +@bin lib/frama-c/plugins/Scope.cmxs @bin lib/frama-c/plugins/Security_slicing.cmxs +@bin lib/frama-c/plugins/Slicing.cmxs +@bin lib/frama-c/plugins/Sparecode.cmxs +@bin lib/frama-c/plugins/Users.cmxs +@bin lib/frama-c/plugins/Value.cmxs @bin lib/frama-c/plugins/Wp.cmxs +@bin lib/frama-c/plugins/gui/Callgraph_gui.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/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/Value.cmxs @bin lib/frama-c/plugins/gui/Wp.cmxs Index: pkg/PFRAG.native =================================================================== RCS file: /OpenBSD/ports/devel/frama-c/pkg/PFRAG.native,v retrieving revision 1.3 diff -u -p -r1.3 PFRAG.native --- pkg/PFRAG.native 30 Aug 2015 16:22:15 -0000 1.3 +++ pkg/PFRAG.native 9 Apr 2016 21:53:29 -0000 @@ -1,44 +1,18 @@ @comment $OpenBSD: PFRAG.native,v 1.3 2015/08/30 16:22:15 avsm Exp $ %%dynlink%% @bin bin/ptests.opt -lib/frama-c/Constant_Propagation.cmx -lib/frama-c/Constant_Propagation.o +lib/frama-c/FCDynlink.cmx +lib/frama-c/FCDynlink.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/From.cmx -lib/frama-c/From.o -lib/frama-c/Impact.cmx -lib/frama-c/Impact.o -lib/frama-c/Inout.cmx -lib/frama-c/Inout.o -lib/frama-c/Metrics.cmx -lib/frama-c/Metrics.o -lib/frama-c/Occurrence.cmx -lib/frama-c/Occurrence.o -lib/frama-c/Pdg.cmx -lib/frama-c/Pdg.o lib/frama-c/Postdominators.cmx lib/frama-c/Postdominators.o lib/frama-c/RteGen.cmx lib/frama-c/RteGen.o -lib/frama-c/Scope.cmx -lib/frama-c/Scope.o -lib/frama-c/Semantic_callgraph.cmx -lib/frama-c/Semantic_callgraph.o -lib/frama-c/Slicing.cmx -lib/frama-c/Slicing.o -lib/frama-c/Sparecode.cmx -lib/frama-c/Sparecode.o -lib/frama-c/Syntactic_callgraph.cmx -lib/frama-c/Syntactic_callgraph.o -lib/frama-c/Users.cmx -lib/frama-c/Users.o -lib/frama-c/Value.cmx -lib/frama-c/Value.o lib/frama-c/abstract_interp.cmx lib/frama-c/abstract_interp.o lib/frama-c/alarms.cmx @@ -69,7 +43,7 @@ lib/frama-c/book_manager.cmx lib/frama-c/book_manager.o lib/frama-c/boot.cmx lib/frama-c/boot.o -lib/frama-c/buckx_c.o +lib/frama-c/c_bindings.o lib/frama-c/cabs.cmx lib/frama-c/cabs.o lib/frama-c/cabs2cil.cmx @@ -80,8 +54,6 @@ lib/frama-c/cabshelper.cmx lib/frama-c/cabshelper.o lib/frama-c/cabsvisit.cmx lib/frama-c/cabsvisit.o -lib/frama-c/callgraph.cmx -lib/frama-c/callgraph.o lib/frama-c/cfg.cmx lib/frama-c/cfg.o lib/frama-c/cil.cmx @@ -100,8 +72,6 @@ lib/frama-c/cil_state_builder.cmx lib/frama-c/cil_state_builder.o lib/frama-c/cilconfig.cmx lib/frama-c/cilconfig.o -lib/frama-c/cilmsg.cmx -lib/frama-c/cilmsg.o lib/frama-c/clexer.cmx lib/frama-c/clexer.o lib/frama-c/clone.cmx @@ -140,8 +110,6 @@ lib/frama-c/dominators.cmx lib/frama-c/dominators.o lib/frama-c/dynamic.cmx lib/frama-c/dynamic.o -lib/frama-c/dynlink_common_interface.cmx -lib/frama-c/dynlink_common_interface.o lib/frama-c/emitter.cmx lib/frama-c/emitter.o lib/frama-c/errorloc.cmx @@ -156,12 +124,16 @@ lib/frama-c/file.cmx lib/frama-c/file.o lib/frama-c/file_manager.cmx lib/frama-c/file_manager.o +lib/frama-c/filecheck.cmx +lib/frama-c/filecheck.o lib/frama-c/filepath.cmx lib/frama-c/filepath.o lib/frama-c/filetree.cmx lib/frama-c/filetree.o lib/frama-c/filter.cmx lib/frama-c/filter.o +lib/frama-c/fixpoint.cmx +lib/frama-c/fixpoint.o lib/frama-c/floating_point.cmx lib/frama-c/floating_point.o lib/frama-c/frama_c_init.cmx @@ -170,14 +142,20 @@ lib/frama-c/frontc.cmx lib/frama-c/frontc.o 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/globals.cmx lib/frama-c/globals.o +lib/frama-c/graph.cmx +lib/frama-c/graph.o lib/frama-c/gtk_form.cmx lib/frama-c/gtk_form.o lib/frama-c/gtk_helper.cmx lib/frama-c/gtk_helper.o lib/frama-c/gui_parameters.cmx lib/frama-c/gui_parameters.o +lib/frama-c/gui_printers.cmx +lib/frama-c/gui_printers.o lib/frama-c/help_manager.cmx lib/frama-c/help_manager.o lib/frama-c/history.cmx @@ -208,6 +186,8 @@ lib/frama-c/kernel.cmx lib/frama-c/kernel.o lib/frama-c/kernel_function.cmx lib/frama-c/kernel_function.o +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/lexerhack.cmx @@ -278,14 +258,33 @@ lib/frama-c/plugin.cmx lib/frama-c/plugin.o lib/frama-c/plugins/Aorai.cmi lib/frama-c/plugins/Aorai.cmo +lib/frama-c/plugins/Aorai.cmx +lib/frama-c/plugins/Callgraph.cmx +lib/frama-c/plugins/Callgraph_gui.cmx +lib/frama-c/plugins/Constant_Propagation.cmx +lib/frama-c/plugins/From.cmx +lib/frama-c/plugins/Impact.cmx +lib/frama-c/plugins/Inout.cmx +lib/frama-c/plugins/Metrics.cmx lib/frama-c/plugins/Obfuscator.cmi lib/frama-c/plugins/Obfuscator.cmo +lib/frama-c/plugins/Obfuscator.cmx +lib/frama-c/plugins/Occurrence.cmx +lib/frama-c/plugins/Pdg.cmx lib/frama-c/plugins/Report.cmi lib/frama-c/plugins/Report.cmo +lib/frama-c/plugins/Report.cmx +lib/frama-c/plugins/Scope.cmx lib/frama-c/plugins/Security_slicing.cmi lib/frama-c/plugins/Security_slicing.cmo +lib/frama-c/plugins/Security_slicing.cmx +lib/frama-c/plugins/Slicing.cmx +lib/frama-c/plugins/Sparecode.cmx +lib/frama-c/plugins/Users.cmx +lib/frama-c/plugins/Value.cmx lib/frama-c/plugins/Wp.cma lib/frama-c/plugins/Wp.cmi +lib/frama-c/plugins/Wp.cmx lib/frama-c/plugins/gui/Security_slicing.cmi lib/frama-c/plugins/gui/Security_slicing.cmo lib/frama-c/plugins/gui/Wp.cma @@ -374,8 +373,6 @@ lib/frama-c/unroll_loops.cmx lib/frama-c/unroll_loops.o lib/frama-c/utf8_logic.cmx lib/frama-c/utf8_logic.o -lib/frama-c/value_messages.cmx -lib/frama-c/value_messages.o lib/frama-c/value_types.cmx lib/frama-c/value_types.o lib/frama-c/vector.cmx @@ -386,3 +383,7 @@ lib/frama-c/warning_manager.cmx lib/frama-c/warning_manager.o lib/frama-c/widen_type.cmx lib/frama-c/widen_type.o +lib/frama-c/wto.cmx +lib/frama-c/wto.o +lib/frama-c/wto_statement.cmx +lib/frama-c/wto_statement.o Index: pkg/PLIST =================================================================== RCS file: /OpenBSD/ports/devel/frama-c/pkg/PLIST,v retrieving revision 1.3 diff -u -p -r1.3 PLIST --- pkg/PLIST 30 Aug 2015 16:22:15 -0000 1.3 +++ pkg/PLIST 9 Apr 2016 21:53:29 -0000 @@ -7,44 +7,18 @@ @bin bin/frama-c-gui.byte @bin bin/frama-c.byte lib/frama-c/ -lib/frama-c/Constant_Propagation.cmi -lib/frama-c/Constant_Propagation.cmo +lib/frama-c/FCDynlink.cmi +lib/frama-c/FCDynlink.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/From.cmi -lib/frama-c/From.cmo -lib/frama-c/Impact.cmi -lib/frama-c/Impact.cmo -lib/frama-c/Inout.cmi -lib/frama-c/Inout.cmo -lib/frama-c/Metrics.cmi -lib/frama-c/Metrics.cmo -lib/frama-c/Occurrence.cmi -lib/frama-c/Occurrence.cmo -lib/frama-c/Pdg.cmi -lib/frama-c/Pdg.cmo lib/frama-c/Postdominators.cmi lib/frama-c/Postdominators.cmo lib/frama-c/RteGen.cmi lib/frama-c/RteGen.cmo -lib/frama-c/Scope.cmi -lib/frama-c/Scope.cmo -lib/frama-c/Semantic_callgraph.cmi -lib/frama-c/Semantic_callgraph.cmo -lib/frama-c/Slicing.cmi -lib/frama-c/Slicing.cmo -lib/frama-c/Sparecode.cmi -lib/frama-c/Sparecode.cmo -lib/frama-c/Syntactic_callgraph.cmi -lib/frama-c/Syntactic_callgraph.cmo -lib/frama-c/Users.cmi -lib/frama-c/Users.cmo -lib/frama-c/Value.cmi -lib/frama-c/Value.cmo lib/frama-c/abstract_interp.cmi lib/frama-c/abstract_interp.cmo lib/frama-c/alarms.cmi @@ -85,8 +59,6 @@ lib/frama-c/cabshelper.cmi lib/frama-c/cabshelper.cmo lib/frama-c/cabsvisit.cmi lib/frama-c/cabsvisit.cmo -lib/frama-c/callgraph.cmi -lib/frama-c/callgraph.cmo lib/frama-c/cfg.cmi lib/frama-c/cfg.cmo lib/frama-c/cil.cmi @@ -106,8 +78,6 @@ lib/frama-c/cil_state_builder.cmo lib/frama-c/cil_types.cmi lib/frama-c/cilconfig.cmi lib/frama-c/cilconfig.cmo -lib/frama-c/cilmsg.cmi -lib/frama-c/cilmsg.cmo lib/frama-c/clexer.cmi lib/frama-c/clexer.cmo lib/frama-c/clone.cmi @@ -146,8 +116,6 @@ lib/frama-c/dominators.cmi lib/frama-c/dominators.cmo lib/frama-c/dynamic.cmi lib/frama-c/dynamic.cmo -lib/frama-c/dynlink_common_interface.cmi -lib/frama-c/dynlink_common_interface.cmo lib/frama-c/emitter.cmi lib/frama-c/emitter.cmo lib/frama-c/errorloc.cmi @@ -162,30 +130,38 @@ lib/frama-c/file.cmi lib/frama-c/file.cmo lib/frama-c/file_manager.cmi lib/frama-c/file_manager.cmo +lib/frama-c/filecheck.cmi +lib/frama-c/filecheck.cmo lib/frama-c/filepath.cmi lib/frama-c/filepath.cmo lib/frama-c/filetree.cmi lib/frama-c/filetree.cmo lib/frama-c/filter.cmi lib/frama-c/filter.cmo +lib/frama-c/fixpoint.cmi +lib/frama-c/fixpoint.cmo lib/frama-c/floating_point.cmi lib/frama-c/floating_point.cmo -lib/frama-c/frama_c_config.cmi lib/frama-c/frama_c_init.cmi lib/frama-c/frama_c_init.cmo lib/frama-c/frontc.cmi lib/frama-c/frontc.cmo 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/globals.cmi lib/frama-c/globals.cmo +lib/frama-c/graph.cmi +lib/frama-c/graph.cmo lib/frama-c/gtk_form.cmi lib/frama-c/gtk_form.cmo lib/frama-c/gtk_helper.cmi lib/frama-c/gtk_helper.cmo -lib/frama-c/gui_init.cmi lib/frama-c/gui_parameters.cmi lib/frama-c/gui_parameters.cmo +lib/frama-c/gui_printers.cmi +lib/frama-c/gui_printers.cmo lib/frama-c/help_manager.cmi lib/frama-c/help_manager.cmo lib/frama-c/history.cmi @@ -194,6 +170,7 @@ lib/frama-c/hook.cmi lib/frama-c/hook.cmo lib/frama-c/hptmap.cmi lib/frama-c/hptmap.cmo +lib/frama-c/hptmap_sig.cmi lib/frama-c/hptset.cmi lib/frama-c/hptset.cmo lib/frama-c/indexer.cmi @@ -217,6 +194,8 @@ lib/frama-c/kernel.cmi lib/frama-c/kernel.cmo lib/frama-c/kernel_function.cmi lib/frama-c/kernel_function.cmo +lib/frama-c/lattice_messages.cmi +lib/frama-c/lattice_messages.cmo lib/frama-c/lattice_type.cmi lib/frama-c/launcher.cmi lib/frama-c/launcher.cmo @@ -293,7 +272,71 @@ lib/frama-c/pdgTypes.cmo lib/frama-c/plugin.cmi lib/frama-c/plugin.cmo lib/frama-c/plugins/ +lib/frama-c/plugins/Callgraph.cmi +lib/frama-c/plugins/Callgraph.cmo +lib/frama-c/plugins/Callgraph_gui.cmi +lib/frama-c/plugins/Callgraph_gui.cmo +lib/frama-c/plugins/Constant_Propagation.cmi +lib/frama-c/plugins/Constant_Propagation.cmo +lib/frama-c/plugins/From.cmi +lib/frama-c/plugins/From.cmo +lib/frama-c/plugins/Impact.cmi +lib/frama-c/plugins/Impact.cmo +lib/frama-c/plugins/Inout.cmi +lib/frama-c/plugins/Inout.cmo +lib/frama-c/plugins/META.frama-c-aorai +lib/frama-c/plugins/META.frama-c-callgraph +lib/frama-c/plugins/META.frama-c-callgraph_gui +lib/frama-c/plugins/META.frama-c-constant_propagation +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-metrics +lib/frama-c/plugins/META.frama-c-obfuscator +lib/frama-c/plugins/META.frama-c-occurrence +lib/frama-c/plugins/META.frama-c-pdg +lib/frama-c/plugins/META.frama-c-report +lib/frama-c/plugins/META.frama-c-scope +lib/frama-c/plugins/META.frama-c-security_slicing +lib/frama-c/plugins/META.frama-c-slicing +lib/frama-c/plugins/META.frama-c-sparecode +lib/frama-c/plugins/META.frama-c-users +lib/frama-c/plugins/META.frama-c-value +lib/frama-c/plugins/META.frama-c-wp +lib/frama-c/plugins/Metrics.cmi +lib/frama-c/plugins/Metrics.cmo +lib/frama-c/plugins/Occurrence.cmi +lib/frama-c/plugins/Occurrence.cmo +lib/frama-c/plugins/Pdg.cmi +lib/frama-c/plugins/Pdg.cmo +lib/frama-c/plugins/Scope.cmi +lib/frama-c/plugins/Scope.cmo +lib/frama-c/plugins/Slicing.cmi +lib/frama-c/plugins/Slicing.cmo +lib/frama-c/plugins/Sparecode.cmi +lib/frama-c/plugins/Sparecode.cmo +lib/frama-c/plugins/Users.cmi +lib/frama-c/plugins/Users.cmo +lib/frama-c/plugins/Value.cmi +lib/frama-c/plugins/Value.cmo +lib/frama-c/plugins/Wp.cmxa lib/frama-c/plugins/gui/ +lib/frama-c/plugins/gui/Callgraph_gui.cmi +lib/frama-c/plugins/gui/Callgraph_gui.cmo +lib/frama-c/plugins/gui/From.cmi +lib/frama-c/plugins/gui/From.cmo +lib/frama-c/plugins/gui/Impact.cmi +lib/frama-c/plugins/gui/Impact.cmo +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/Scope.cmi +lib/frama-c/plugins/gui/Scope.cmo +lib/frama-c/plugins/gui/Slicing.cmi +lib/frama-c/plugins/gui/Slicing.cmo +lib/frama-c/plugins/gui/Value.cmi +lib/frama-c/plugins/gui/Value.cmo lib/frama-c/precise_locs.cmi lib/frama-c/precise_locs.cmo lib/frama-c/pretty_source.cmi @@ -378,8 +421,6 @@ lib/frama-c/unroll_loops.cmi lib/frama-c/unroll_loops.cmo lib/frama-c/utf8_logic.cmi lib/frama-c/utf8_logic.cmo -lib/frama-c/value_messages.cmi -lib/frama-c/value_messages.cmo lib/frama-c/value_types.cmi lib/frama-c/value_types.cmo lib/frama-c/vector.cmi @@ -390,6 +431,10 @@ lib/frama-c/warning_manager.cmi lib/frama-c/warning_manager.cmo lib/frama-c/widen_type.cmi lib/frama-c/widen_type.cmo +lib/frama-c/wto.cmi +lib/frama-c/wto.cmo +lib/frama-c/wto_statement.cmi +lib/frama-c/wto_statement.cmo @man man/man1/frama-c-gui.1 @man man/man1/frama-c.1 share/frama-c/ @@ -401,7 +446,6 @@ share/frama-c/Makefile.generic share/frama-c/Makefile.kernel share/frama-c/Makefile.plugin share/frama-c/acsl.el -share/frama-c/builtin.c share/frama-c/builtin.h share/frama-c/configure.ac share/frama-c/doc/ @@ -419,7 +463,6 @@ share/frama-c/frama-c.ico share/frama-c/frama-c.rc share/frama-c/libc/ share/frama-c/libc.c -share/frama-c/libc.h share/frama-c/libc/__fc_builtin.h share/frama-c/libc/__fc_builtin_for_normalization.i share/frama-c/libc/__fc_define_blkcnt_t.h @@ -437,7 +480,6 @@ share/frama-c/libc/__fc_define_nlink_t.h share/frama-c/libc/__fc_define_null.h share/frama-c/libc/__fc_define_off_t.h share/frama-c/libc/__fc_define_pid_t.h -share/frama-c/libc/__fc_define_restrict.h share/frama-c/libc/__fc_define_sa_family_t.h share/frama-c/libc/__fc_define_seek_macros.h share/frama-c/libc/__fc_define_sigset_t.h @@ -530,9 +572,7 @@ share/frama-c/libc/uchar.h share/frama-c/libc/unistd.h share/frama-c/libc/wchar.h share/frama-c/libc/wctype.h -share/frama-c/machine.h -share/frama-c/math.c -share/frama-c/math.h +share/frama-c/machdep.c share/frama-c/theme/ share/frama-c/theme/colorblind/ share/frama-c/theme/colorblind/considered_valid.png @@ -566,32 +606,55 @@ share/frama-c/unmark.png share/frama-c/wp/ share/frama-c/wp/coqwp/ share/frama-c/wp/coqwp/Bits.v +share/frama-c/wp/coqwp/Bits.vo share/frama-c/wp/coqwp/BuiltIn.v +share/frama-c/wp/coqwp/BuiltIn.vo share/frama-c/wp/coqwp/Cbits.v +share/frama-c/wp/coqwp/Cbits.vo share/frama-c/wp/coqwp/Cfloat.v +share/frama-c/wp/coqwp/Cfloat.vo share/frama-c/wp/coqwp/Cint.v +share/frama-c/wp/coqwp/Cint.vo share/frama-c/wp/coqwp/Cmath.v +share/frama-c/wp/coqwp/Cmath.vo share/frama-c/wp/coqwp/Memory.v +share/frama-c/wp/coqwp/Memory.vo share/frama-c/wp/coqwp/Qed.v +share/frama-c/wp/coqwp/Qed.vo share/frama-c/wp/coqwp/Qedlib.v +share/frama-c/wp/coqwp/Qedlib.vo share/frama-c/wp/coqwp/Vset.v +share/frama-c/wp/coqwp/Vset.vo share/frama-c/wp/coqwp/Zbits.v +share/frama-c/wp/coqwp/Zbits.vo share/frama-c/wp/coqwp/bool/ share/frama-c/wp/coqwp/bool/Bool.v +share/frama-c/wp/coqwp/bool/Bool.vo share/frama-c/wp/coqwp/int/ share/frama-c/wp/coqwp/int/Abs.v +share/frama-c/wp/coqwp/int/Abs.vo share/frama-c/wp/coqwp/int/ComputerDivision.v +share/frama-c/wp/coqwp/int/ComputerDivision.vo share/frama-c/wp/coqwp/int/Int.v +share/frama-c/wp/coqwp/int/Int.vo share/frama-c/wp/coqwp/int/MinMax.v +share/frama-c/wp/coqwp/int/MinMax.vo share/frama-c/wp/coqwp/map/ share/frama-c/wp/coqwp/map/Map.v +share/frama-c/wp/coqwp/map/Map.vo share/frama-c/wp/coqwp/real/ share/frama-c/wp/coqwp/real/Abs.v +share/frama-c/wp/coqwp/real/Abs.vo share/frama-c/wp/coqwp/real/FromInt.v +share/frama-c/wp/coqwp/real/FromInt.vo share/frama-c/wp/coqwp/real/MinMax.v +share/frama-c/wp/coqwp/real/MinMax.vo share/frama-c/wp/coqwp/real/Real.v +share/frama-c/wp/coqwp/real/Real.vo share/frama-c/wp/coqwp/real/RealInfix.v +share/frama-c/wp/coqwp/real/RealInfix.vo share/frama-c/wp/coqwp/real/Square.v +share/frama-c/wp/coqwp/real/Square.vo share/frama-c/wp/ergo/ share/frama-c/wp/ergo/Cbits.mlw share/frama-c/wp/ergo/Cfloat.mlw
