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
-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
pgpqF8u65sMg4.pgp
Description: OpenPGP digital signature
