On Thu, 29 Aug 2019 12:58:14 +0200 Jeremie Courreges-Anglas <j...@wxcvbn.org> wrote:
> On Thu, Aug 29 2019, Jeremie Courreges-Anglas <j...@wxcvbn.org> wrote: > > On Thu, Aug 29 2019, Christopher Zimmermann <chr...@openbsd.org> > > wrote: > >> On Sun, 25 Aug 2019 20:32:53 +0200 > >> Jeremie Courreges-Anglas <j...@wxcvbn.org> wrote: > >> > >>> On Fri, Aug 23 2019, Christopher Zimmermann <chr...@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
pgpdumvAe6J2v.pgp
Description: OpenPGP digital signature