Re: update devel/frama-c

On Fri, Aug 23, 2019 at 10:25:44PM +0200, Christopher Zimmermann wrote:
> Hi,
>
> this Frama-C release is compatible with OCaml 4.08. It builds and runs
> fine on amd64. I cannot build a bytecode-only version on amd64.
> I would welcome OKs and tests on real bytecode-only archs and i386,
> which is currently broken.
>
> 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 23 Aug 2019 20:20:13 -0000
> @@ -6,37 +6,33 @@ FIX_EXTRACT_PERMISSIONS = Yes
>
> COMMENT = an extensible platform for analysis of C software

While here, drop the 'an' ;-)


>
> -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 23 Aug 2019 20:20:13 -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: patches/patch-Makefile
> diff -N patches/patch-Makefile
> --- patches/patch-Makefile 4 Mar 2019 12:51:12 -0000 1.1
> +++ /dev/null 1 Jan 1970 00:00:00 -0000
> @@ -1,26 +0,0 @@
> -$OpenBSD: patch-Makefile,v 1.1 2019/03/04 12:51:12 chrisz Exp $
> -
> -don't try to install cmx* files on bytecode builds.
> -
> -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
> Index: patches/patch-configure_in
> ===================================================================
> RCS file: patches/patch-configure_in
> diff -N patches/patch-configure_in
> --- patches/patch-configure_in 4 Mar 2019 12:51:12 -0000 1.1
> +++ /dev/null 1 Jan 1970 00:00:00 -0000
> @@ -1,47 +0,0 @@
> -$OpenBSD: patch-configure_in,v 1.1 2019/03/04 12:51:12 chrisz Exp $
> -
> -Use system threads if available - even on bytecode builds.
> -Vmthreads are broken and deprecated.
> -
> -Index: configure.in
> ---- configure.in.orig
> -+++ configure.in
> -@@ -436,23 +436,23 @@ 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*;
> -+ # 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
> -+ 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
> 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 23 Aug 2019 20:20:13 -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 23 Aug 2019 20:20:13 -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 23 Aug 2019 20:20:14 -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



--
Antoine