This builds and tests successfully for me. I needed to add an additional macro alias for a glibc rounding operation. I'll submit upstream soon. The existing ones are wrapped in an #ifdef __OpenBSD__, so presumably they'll accept it.
The PID-related fix is unchanged, but the source file moved. I also got this during make update-plist: > pkg/PFRAG.no-native empty fragment: NOT writing it Does that mean that pkg/PFRAG.no-native is no longer needed and should be removed? Or was it added manually? Make test succeeds aside from a few non-fatal mutex errors: > pthread_mutex_destroy on mutex with waiters! jca@ verified that those are present in the current port, though, so it doesn't seem like a regression. I also add myself as maintainer. Index: Makefile =================================================================== RCS file: /cvs/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 22 Jan 2016 20:58:16 -0000 @@ -6,10 +6,12 @@ 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/ + +MAINTAINER = Michael McConville <mm...@mykolab.com> # LGPLv2 PERMIT_PACKAGE_CDROM = Yes Index: distinfo =================================================================== RCS file: /cvs/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 22 Jan 2016 20:58:16 -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 22 Jan 2016 20:58:16 -0000 @@ -0,0 +1,22 @@ +$OpenBSD$ +--- src/libraries/utils/c_bindings.c.orig Thu Jan 14 11:30:26 2016 ++++ src/libraries/utils/c_bindings.c Fri Jan 22 00:53:06 2016 +@@ -41,6 +41,7 @@ + # define FE_DOWNWARD FP_RM + # define FE_UPWARD FP_RP + # define FE_TONEAREST FP_RN ++# define FE_TOWARDZERO FP_RZ + # define fegetround() fpgetround() + # define fesetround(RM) fpsetround(RM) + #else +@@ -242,8 +243,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.native =================================================================== RCS file: /cvs/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 22 Jan 2016 20:58:16 -0000 @@ -1,44 +1,16 @@ @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/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 +41,6 @@ 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/cabs.cmx lib/frama-c/cabs.o lib/frama-c/cabs2cil.cmx @@ -80,8 +51,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 +69,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 +107,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 @@ -374,8 +339,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 Index: pkg/PLIST =================================================================== RCS file: /cvs/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 22 Jan 2016 20:58:16 -0000 @@ -7,44 +7,20 @@ @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/FCDynlink.cmx +lib/frama-c/FCDynlink.o 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 @@ -75,6 +51,7 @@ lib/frama-c/book_manager.cmi lib/frama-c/book_manager.cmo lib/frama-c/boot.cmi lib/frama-c/boot.cmo +lib/frama-c/c_bindings.o lib/frama-c/cabs.cmi lib/frama-c/cabs.cmo lib/frama-c/cabs2cil.cmi @@ -85,8 +62,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 +81,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 +119,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 +133,48 @@ 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/filecheck.cmx +lib/frama-c/filecheck.o 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/fixpoint.cmx +lib/frama-c/fixpoint.o 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/fval.cmx +lib/frama-c/fval.o lib/frama-c/globals.cmi lib/frama-c/globals.cmo +lib/frama-c/graph.cmi +lib/frama-c/graph.cmo +lib/frama-c/graph.cmx +lib/frama-c/graph.o 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/gui_printers.cmx +lib/frama-c/gui_printers.o lib/frama-c/help_manager.cmi lib/frama-c/help_manager.cmo lib/frama-c/history.cmi @@ -194,6 +183,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 +207,10 @@ 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_messages.cmx +lib/frama-c/lattice_messages.o lib/frama-c/lattice_type.cmi lib/frama-c/launcher.cmi lib/frama-c/launcher.cmo @@ -293,7 +287,112 @@ lib/frama-c/pdgTypes.cmo lib/frama-c/plugin.cmi lib/frama-c/plugin.cmo lib/frama-c/plugins/ +lib/frama-c/plugins/Aorai.cmx +lib/frama-c/plugins/Callgraph.cmi +lib/frama-c/plugins/Callgraph.cmo +lib/frama-c/plugins/Callgraph.cmx +@bin lib/frama-c/plugins/Callgraph.cmxs +lib/frama-c/plugins/Callgraph_gui.cmi +lib/frama-c/plugins/Callgraph_gui.cmo +lib/frama-c/plugins/Callgraph_gui.cmx +@bin lib/frama-c/plugins/Callgraph_gui.cmxs +lib/frama-c/plugins/Constant_Propagation.cmi +lib/frama-c/plugins/Constant_Propagation.cmo +lib/frama-c/plugins/Constant_Propagation.cmx +@bin lib/frama-c/plugins/Constant_Propagation.cmxs +lib/frama-c/plugins/From.cmi +lib/frama-c/plugins/From.cmo +lib/frama-c/plugins/From.cmx +@bin lib/frama-c/plugins/From.cmxs +lib/frama-c/plugins/Impact.cmi +lib/frama-c/plugins/Impact.cmo +lib/frama-c/plugins/Impact.cmx +@bin lib/frama-c/plugins/Impact.cmxs +lib/frama-c/plugins/Inout.cmi +lib/frama-c/plugins/Inout.cmo +lib/frama-c/plugins/Inout.cmx +@bin lib/frama-c/plugins/Inout.cmxs +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/Metrics.cmx +@bin lib/frama-c/plugins/Metrics.cmxs +lib/frama-c/plugins/Obfuscator.cmx +lib/frama-c/plugins/Occurrence.cmi +lib/frama-c/plugins/Occurrence.cmo +lib/frama-c/plugins/Occurrence.cmx +@bin lib/frama-c/plugins/Occurrence.cmxs +lib/frama-c/plugins/Pdg.cmi +lib/frama-c/plugins/Pdg.cmo +lib/frama-c/plugins/Pdg.cmx +@bin lib/frama-c/plugins/Pdg.cmxs +lib/frama-c/plugins/Report.cmx +lib/frama-c/plugins/Scope.cmi +lib/frama-c/plugins/Scope.cmo +lib/frama-c/plugins/Scope.cmx +@bin lib/frama-c/plugins/Scope.cmxs +lib/frama-c/plugins/Security_slicing.cmx +lib/frama-c/plugins/Slicing.cmi +lib/frama-c/plugins/Slicing.cmo +lib/frama-c/plugins/Slicing.cmx +@bin lib/frama-c/plugins/Slicing.cmxs +lib/frama-c/plugins/Sparecode.cmi +lib/frama-c/plugins/Sparecode.cmo +lib/frama-c/plugins/Sparecode.cmx +@bin lib/frama-c/plugins/Sparecode.cmxs +lib/frama-c/plugins/Users.cmi +lib/frama-c/plugins/Users.cmo +lib/frama-c/plugins/Users.cmx +@bin lib/frama-c/plugins/Users.cmxs +lib/frama-c/plugins/Value.cmi +lib/frama-c/plugins/Value.cmo +lib/frama-c/plugins/Value.cmx +@bin lib/frama-c/plugins/Value.cmxs +lib/frama-c/plugins/Wp.cmx +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 +@bin lib/frama-c/plugins/gui/Callgraph_gui.cmxs +lib/frama-c/plugins/gui/From.cmi +lib/frama-c/plugins/gui/From.cmo +@bin lib/frama-c/plugins/gui/From.cmxs +lib/frama-c/plugins/gui/Impact.cmi +lib/frama-c/plugins/gui/Impact.cmo +@bin lib/frama-c/plugins/gui/Impact.cmxs +lib/frama-c/plugins/gui/Metrics.cmi +lib/frama-c/plugins/gui/Metrics.cmo +@bin lib/frama-c/plugins/gui/Metrics.cmxs +lib/frama-c/plugins/gui/Occurrence.cmi +lib/frama-c/plugins/gui/Occurrence.cmo +@bin lib/frama-c/plugins/gui/Occurrence.cmxs +lib/frama-c/plugins/gui/Scope.cmi +lib/frama-c/plugins/gui/Scope.cmo +@bin lib/frama-c/plugins/gui/Scope.cmxs +lib/frama-c/plugins/gui/Slicing.cmi +lib/frama-c/plugins/gui/Slicing.cmo +@bin lib/frama-c/plugins/gui/Slicing.cmxs +lib/frama-c/plugins/gui/Value.cmi +lib/frama-c/plugins/gui/Value.cmo +@bin lib/frama-c/plugins/gui/Value.cmxs lib/frama-c/precise_locs.cmi lib/frama-c/precise_locs.cmo lib/frama-c/pretty_source.cmi @@ -378,8 +477,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 +487,14 @@ 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.cmx +lib/frama-c/wto.o +lib/frama-c/wto_statement.cmi +lib/frama-c/wto_statement.cmo +lib/frama-c/wto_statement.cmx +lib/frama-c/wto_statement.o @man man/man1/frama-c-gui.1 @man man/man1/frama-c.1 share/frama-c/ @@ -401,7 +506,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 +523,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 +540,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 +632,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 +666,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
