Friday, August 30, 2019

Re: update devel/frama-c

On Thu, 29 Aug 2019 12:58:14 +0200
Jeremie Courreges-Anglas <jca@wxcvbn.org> wrote:

> On Thu, Aug 29 2019, Jeremie Courreges-Anglas <jca@wxcvbn.org> wrote:
> > On Thu, Aug 29 2019, Christopher Zimmermann <chrisz@openbsd.org>
> > wrote:
> >> On Sun, 25 Aug 2019 20:32:53 +0200
> >> Jeremie Courreges-Anglas <jca@wxcvbn.org> wrote:
> >>
> >>> On Fri, Aug 23 2019, Christopher Zimmermann <chrisz@openbsd.org>
> >>> wrote:
> >> Thank you again for testing. I managed to track down and fix
> >> several build problems for bytecode-only builds on amd64. So there
> >> is some reason to hope it will build successfully on sparc64, too.
> >> Could you have another try?
> >
> > It builds and packages fine! :)
> > Now running it in a loop to see if it's stable, but I see no reason
> > for hidden failures.
>
> That's 5 successful builds in a row, LGTM. I'm no frama-c user,
> though.

That's great. So any OKs to commit this update? It's building fine
on amd64 with and without nativecode as well as sparc64. It will still fail
on i386. The added patches will hopefully be merged upstream in the next
Frama-C release.

Christopher


Index: Makefile
===================================================================
RCS file: /cvs/ports/devel/frama-c/Makefile,v
retrieving revision 1.18
diff -u -p -r1.18 Makefile
--- Makefile 12 Jul 2019 20:44:08 -0000 1.18
+++ Makefile 29 Aug 2019 05:54:03 -0000
@@ -4,39 +4,35 @@ BROKEN-i386 = ld: error: undefined symbo

FIX_EXTRACT_PERMISSIONS = Yes

-COMMENT = an extensible platform for analysis of C software
+COMMENT = extensible platform for analysis of C software

-DISTNAME = frama-c-18.0-Argon
-PKGNAME = frama-c-18.0
-REVISION = 1
CATEGORIES = devel
+GH_ACCOUNT = Frama-C
+GH_PROJECT = Frama-C-snapshot
+GH_TAGNAME = 19.0
+DISTNAME = frama-c-${GH_TAGNAME}-Potassium
+PKGNAME = frama-c-${GH_TAGNAME}
+
HOMEPAGE = https://frama-c.com/

# LGPLv2
PERMIT_PACKAGE = Yes

-WANTLIB = X11 Xcomposite Xcursor Xdamage Xext Xfixes Xi Xinerama Xrandr
-WANTLIB += Xrender art_lgpl_2 atk-1.0 c cairo fontconfig freetype
-WANTLIB += gdk-x11-2.0 gdk_pixbuf-2.0 gio-2.0 glib-2.0 gnomecanvas-2
-WANTLIB += gobject-2.0 gtk-x11-2.0 gtksourceview-2.0 intl m gmp
-WANTLIB += pango-1.0 pangocairo-1.0 pangoft2-1.0 pthread z
-
-MASTER_SITES = https://frama-c.com/download/
+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

MODULES = lang/ocaml

-BUILD_DEPENDS = x11/lablgtk2 \
+RUN_DEPENDS = x11/lablgtk3 \
devel/ocaml-graph \
math/graphviz \
math/ocaml-zarith \
- sysutils/findlib
-RUN_DEPENDS = x11/lablgtk2 \
- math/graphviz \
- math/ocaml-zarith \
- sysutils/findlib
+ devel/ocaml-yojson

-LIB_DEPENDS = x11/gnome/libgnomecanvas \
- x11/gtksourceview
+BUILD_DEPENDS = ${RUN_DEPENDS} \
+ sysutils/findlib

USE_GMAKE = Yes
TEST_TARGET = oracles tests
Index: distinfo
===================================================================
RCS file: /cvs/ports/devel/frama-c/distinfo,v
retrieving revision 1.3
diff -u -p -r1.3 distinfo
--- distinfo 4 Mar 2019 12:51:12 -0000 1.3
+++ distinfo 29 Aug 2019 05:54:03 -0000
@@ -1,2 +1,2 @@
-SHA256 (frama-c-18.0-Argon.tar.gz) = QrElQMYI879swlimvO3t88WWWJ5Yv9/Gv0c6BauYCCk=
-SIZE (frama-c-18.0-Argon.tar.gz) = 5358960
+SHA256 (frama-c-19.0-Potassium.tar.gz) = JQLGITrB+V4E0qaPszAhcvpa9hV0+jD9gpWWI+SwgyY=
+SIZE (frama-c-19.0-Potassium.tar.gz) = 5615479
Index: patches/patch-Makefile
===================================================================
RCS file: /cvs/ports/devel/frama-c/patches/patch-Makefile,v
retrieving revision 1.1
diff -u -p -r1.1 patch-Makefile
--- patches/patch-Makefile 4 Mar 2019 12:51:12 -0000 1.1
+++ patches/patch-Makefile 29 Aug 2019 05:54:03 -0000
@@ -5,22 +5,51 @@ don't try to install cmx* files on bytec
Index: Makefile
--- Makefile.orig
+++ Makefile
-@@ -1863,14 +1863,16 @@ install:: install-lib
- if [ -d "$(FRAMAC_PLUGIN)" ]; then \
- $(CP) $(PLUGIN_DYN_CMI_LIST) $(PLUGIN_META_LIST) \
- $(FRAMAC_PLUGINDIR); \
-- $(CP) $(PLUGIN_DYN_CMO_LIST) $(PLUGIN_DYN_CMX_LIST) \
-+ $(CP) $(PLUGIN_DYN_CMO_LIST) \
-+ $(if $(filter opt, $(OCAMLBEST)), $(PLUGIN_DYN_CMX_LIST),) \
- $(FRAMAC_PLUGINDIR)/top; \
- fi
- $(PRINT_INSTALL) gui plug-ins
- if [ -d "$(FRAMAC_PLUGIN_GUI)" -a "$(PLUGIN_DYN_GUI_EXISTS)" = "yes" ]; \
- then \
- $(CP) $(patsubst %.cma,%.cmi,$(PLUGIN_DYN_GUI_CMO_LIST:.cmo=.cmi)) \
-- $(PLUGIN_DYN_GUI_CMO_LIST) $(PLUGIN_DYN_GUI_CMX_LIST) \
-+ $(PLUGIN_DYN_GUI_CMO_LIST) \
-+ $(if $(filter opt, $(OCAMLBEST)), $(PLUGIN_DYN_GUI_CMX_LIST),) \
- $(FRAMAC_PLUGINDIR)/gui; \
- fi
- $(PRINT_INSTALL) man pages
+@@ -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)
++ $(CP) $(addprefix frama-c.a frama-c.cmxa)
++
+ 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: /cvs/ports/devel/frama-c/patches/patch-configure_in,v
retrieving revision 1.1
diff -u -p -r1.1 patch-configure_in
--- patches/patch-configure_in 4 Mar 2019 12:51:12 -0000 1.1
+++ patches/patch-configure_in 29 Aug 2019 05:54:03 -0000
@@ -6,7 +6,7 @@ Vmthreads are broken and deprecated.
Index: configure.in
--- configure.in.orig
+++ configure.in
-@@ -436,23 +436,23 @@ else
+@@ -446,23 +446,19 @@ else
EXE=
fi

@@ -24,13 +24,9 @@ Index: configure.in
- AC_MSG_WARN([unsupported.]);
- fi
- rm -f test_native_threads*;
-+ # OCaml native threads
+ AC_MSG_CHECKING([OCaml native threads])
+ echo "let f = Thread.create (fun () -> ())" > test_native_threads.ml
+ if
-+ test "$OCAMLBEST" = opt &&
-+ ($OCAMLOPT -thread -o test_native_threads unix.cma threads.cma \
-+ test_native_threads.ml) 2> /dev/null ||
+ ($OCAMLC -thread -o test_native_threads unix.cma threads.cma \
+ test_native_threads.ml) 2> /dev/null
+ then
Index: pkg/PFRAG.dynlink-native
===================================================================
RCS file: /cvs/ports/devel/frama-c/pkg/PFRAG.dynlink-native,v
retrieving revision 1.3
diff -u -p -r1.3 PFRAG.dynlink-native
--- pkg/PFRAG.dynlink-native 4 Mar 2019 12:51:12 -0000 1.3
+++ pkg/PFRAG.dynlink-native 29 Aug 2019 05:54:03 -0000
@@ -1,5 +1,4 @@
@comment $OpenBSD: PFRAG.dynlink-native,v 1.3 2019/03/04 12:51:12 chrisz Exp $
-@bin lib/frama-c/plugins/gui/Callgraph.cmxs
@bin lib/frama-c/plugins/gui/Eva.cmxs
@bin lib/frama-c/plugins/gui/From.cmxs
@bin lib/frama-c/plugins/gui/Impact.cmxs
Index: pkg/PFRAG.native
===================================================================
RCS file: /cvs/ports/devel/frama-c/pkg/PFRAG.native,v
retrieving revision 1.4
diff -u -p -r1.4 PFRAG.native
--- pkg/PFRAG.native 4 Mar 2019 12:51:12 -0000 1.4
+++ pkg/PFRAG.native 29 Aug 2019 05:54:03 -0000
@@ -9,6 +9,8 @@ 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/alarms.cmx
@@ -107,6 +109,8 @@ 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/dominators.cmx
lib/frama-c/dominators.o
lib/frama-c/dynamic.cmx
@@ -139,6 +143,8 @@ lib/frama-c/float_interval.cmx
lib/frama-c/float_interval.o
lib/frama-c/floating_point.cmx
lib/frama-c/floating_point.o
+lib/frama-c/frama-c.a
+lib/frama-c/frama-c.cmxa
lib/frama-c/frama_c_init.cmx
lib/frama-c/frama_c_init.o
lib/frama-c/frontc.cmx
@@ -149,6 +155,8 @@ lib/frama-c/fval.cmx
lib/frama-c/fval.o
lib/frama-c/globals.cmx
lib/frama-c/globals.o
+lib/frama-c/gtk_compat.cmx
+lib/frama-c/gtk_compat.o
lib/frama-c/gtk_form.cmx
lib/frama-c/gtk_form.o
lib/frama-c/gtk_helper.cmx
@@ -304,6 +312,8 @@ lib/frama-c/printer.cmx
lib/frama-c/printer.o
lib/frama-c/printer_builder.cmx
lib/frama-c/printer_builder.o
+lib/frama-c/printer_tag.cmx
+lib/frama-c/printer_tag.o
lib/frama-c/project.cmx
lib/frama-c/project.o
lib/frama-c/project_manager.cmx
@@ -328,6 +338,8 @@ lib/frama-c/rich_text.cmx
lib/frama-c/rich_text.o
lib/frama-c/rmtmps.cmx
lib/frama-c/rmtmps.o
+lib/frama-c/sanitizer.cmx
+lib/frama-c/sanitizer.o
lib/frama-c/service_graph.cmx
lib/frama-c/service_graph.o
lib/frama-c/source_manager.cmx
@@ -406,3 +418,5 @@ lib/frama-c/wto_statement.cmx
lib/frama-c/wto_statement.o
lib/frama-c/wutil.cmx
lib/frama-c/wutil.o
+lib/frama-c/wutil_once.cmx
+lib/frama-c/wutil_once.o
Index: pkg/PLIST
===================================================================
RCS file: /cvs/ports/devel/frama-c/pkg/PLIST,v
retrieving revision 1.4
diff -u -p -r1.4 PLIST
--- pkg/PLIST 4 Mar 2019 12:51:12 -0000 1.4
+++ pkg/PLIST 29 Aug 2019 05:54:03 -0000
@@ -16,6 +16,9 @@ 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/alarms.cmi
@@ -116,6 +119,9 @@ 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/dominators.cmi
lib/frama-c/dominators.cmo
lib/frama-c/dynamic.cmi
@@ -150,6 +156,7 @@ lib/frama-c/float_interval_sig.cmi
lib/frama-c/float_sig.cmi
lib/frama-c/floating_point.cmi
lib/frama-c/floating_point.cmo
+lib/frama-c/frama-c.cma
lib/frama-c/frama_c_init.cmi
lib/frama-c/frama_c_init.cmo
lib/frama-c/frontc.cmi
@@ -160,6 +167,8 @@ lib/frama-c/fval.cmi
lib/frama-c/fval.cmo
lib/frama-c/globals.cmi
lib/frama-c/globals.cmo
+lib/frama-c/gtk_compat.cmi
+lib/frama-c/gtk_compat.cmo
lib/frama-c/gtk_form.cmi
lib/frama-c/gtk_form.cmo
lib/frama-c/gtk_helper.cmi
@@ -217,6 +226,7 @@ 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
lib/frama-c/lmap.cmi
lib/frama-c/lmap.cmo
lib/frama-c/lmap_bitwise.cmi
@@ -343,8 +353,6 @@ 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/Callgraph.cmi
-lib/frama-c/plugins/gui/Callgraph.cmo
lib/frama-c/plugins/gui/Eva.cmi
lib/frama-c/plugins/gui/Eva.cmo
lib/frama-c/plugins/gui/From.cmi
@@ -406,6 +414,8 @@ lib/frama-c/printer.cmo
lib/frama-c/printer_api.cmi
lib/frama-c/printer_builder.cmi
lib/frama-c/printer_builder.cmo
+lib/frama-c/printer_tag.cmi
+lib/frama-c/printer_tag.cmo
lib/frama-c/project.cmi
lib/frama-c/project.cmo
lib/frama-c/project_manager.cmi
@@ -429,6 +439,8 @@ lib/frama-c/rich_text.cmi
lib/frama-c/rich_text.cmo
lib/frama-c/rmtmps.cmi
lib/frama-c/rmtmps.cmo
+lib/frama-c/sanitizer.cmi
+lib/frama-c/sanitizer.cmo
lib/frama-c/service_graph.cmi
lib/frama-c/service_graph.cmo
lib/frama-c/source_manager.cmi
@@ -508,6 +520,8 @@ lib/frama-c/wto_statement.cmi
lib/frama-c/wto_statement.cmo
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
@@ -523,6 +537,8 @@ 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/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/
@@ -531,11 +547,17 @@ share/frama-c/analysis-scripts/examples/
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/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/git_utils.py
share/frama-c/analysis-scripts/list_files.py
+share/frama-c/analysis-scripts/make_wrapper.py
share/frama-c/analysis-scripts/parse-coverage.sh
-share/frama-c/analysis-scripts/summary.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
@@ -624,9 +646,11 @@ share/frama-c/libc/__fc_define_uid_and_g
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_machdep.h
-share/frama-c/libc/__fc_machdep_linux_gcc_shared.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
@@ -643,7 +667,6 @@ share/frama-c/libc/dlfcn.h
share/frama-c/libc/endian.h
share/frama-c/libc/errno.c
share/frama-c/libc/errno.h
-share/frama-c/libc/fc_runtime.c
share/frama-c/libc/fcntl.h
share/frama-c/libc/features.h
share/frama-c/libc/fenv.c
@@ -661,14 +684,7 @@ share/frama-c/libc/inttypes.c
share/frama-c/libc/inttypes.h
share/frama-c/libc/iso646.h
share/frama-c/libc/libgen.h
-share/frama-c/libc/libintl.h
share/frama-c/libc/limits.h
-share/frama-c/libc/linux/
-share/frama-c/libc/linux/fs.h
-share/frama-c/libc/linux/if_addr.h
-share/frama-c/libc/linux/if_netlink.h
-share/frama-c/libc/linux/netlink.h
-share/frama-c/libc/linux/rtnetlink.h
share/frama-c/libc/locale.c
share/frama-c/libc/locale.h
share/frama-c/libc/malloc.h
@@ -681,9 +697,6 @@ share/frama-c/libc/netdb.c
share/frama-c/libc/netdb.h
share/frama-c/libc/netinet/
share/frama-c/libc/netinet/in.h
-share/frama-c/libc/netinet/in_systm.h
-share/frama-c/libc/netinet/ip.h
-share/frama-c/libc/netinet/ip_icmp.h
share/frama-c/libc/netinet/tcp.h
share/frama-c/libc/nl_types.h
share/frama-c/libc/poll.h
@@ -694,6 +707,7 @@ share/frama-c/libc/resolv.h
share/frama-c/libc/sched.h
share/frama-c/libc/semaphore.h
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/stdbool.h
@@ -712,7 +726,6 @@ 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
@@ -720,7 +733,6 @@ 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/sysctl.h
share/frama-c/libc/sys/time.h
share/frama-c/libc/sys/times.h
share/frama-c/libc/sys/timex.h
@@ -732,8 +744,8 @@ 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/uchar.h
share/frama-c/libc/unistd.h
share/frama-c/libc/utime.h
share/frama-c/libc/utmpx.h
@@ -797,6 +809,7 @@ share/frama-c/wp/coqwp/Cfloat.v
share/frama-c/wp/coqwp/Cint.v
share/frama-c/wp/coqwp/Cmath.v
share/frama-c/wp/coqwp/ExpLog.v
+share/frama-c/wp/coqwp/HighOrd.v
share/frama-c/wp/coqwp/Memory.v
share/frama-c/wp/coqwp/Qed.v
share/frama-c/wp/coqwp/Qedlib.v
@@ -809,8 +822,10 @@ 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/Exponentiation.v
share/frama-c/wp/coqwp/int/Int.v
share/frama-c/wp/coqwp/int/MinMax.v
+share/frama-c/wp/coqwp/int/Power.v
share/frama-c/wp/coqwp/map/
share/frama-c/wp/coqwp/map/Const.v
share/frama-c/wp/coqwp/map/Map.v




--
http://gmerlin.de
OpenPGP: http://gmerlin.de/christopher.pub
CB07 DA40 B0B6 571D 35E2 0DEF 87E2 92A7 13E5 DEE1

No comments:

Post a Comment

Subscribe to: Post Comments (Atom)