From 03afadb267d63abf76cbb6b9e31766cc67231b68 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Wed, 1 Apr 2020 18:23:14 +0200
Subject: [PATCH] [debug] more robust bin/frama-c.debug script across OCaml
versions
- 4.08.0 messes up dynlink, which is needed by extlib for semi-good reasons:
it is currently impossible to load the printers in this version.
- 4.09.0 and upwards directly load dynlink, and will complain if we try to
do that again.
---
bin/frama-c.debug | 22 ++++++++++++++++++++--
1 file changed, 20 insertions(+), 2 deletions(-)
diff --git a/bin/frama-c.debug b/bin/frama-c.debug
index 89d9b58a603..39667bbb3b5 100755
--- a/bin/frama-c.debug
+++ b/bin/frama-c.debug
@@ -24,12 +24,29 @@
. $(dirname $0)/local_export.sh
+if ! command -v ocamlc > /dev/null; then
+ echo "ocamlc not found" && exit 1;
+fi
+if ! command -v ocamldebug > /dev/null; then
+ echo "ocamldebug not found" && exit 1;
+fi
+
+OCAML_VERSION=$(ocamlc -version)
+case $OCAML_VERSION in
+4.05*|4.06*|4.07*) DYNLINK='load_printer "dynlink.cma"';;
+4.08*)
+ echo "impossible to load dynlink in ocamldebug for version $OCAML_VERSION";
+ echo "pretty-printers will not be loaded";
+ if test ! -e .ocamldebug; then GEN_OCAMLDEBUG=yes; touch .ocamldebug; fi;;
+*) DYNLINK=;;
+esac
+
if test ! -e .ocamldebug; then
GEN_OCAMLDEBUG=yes;
cat <<EOF > .ocamldebug;
load_printer "str.cma"
load_printer "zarith.cma"
-load_printer "dynlink.cma"
+$DYNLINK
load_printer "extlib.cmo"
load_printer "filepath.cmo"
load_printer "integer.cmo"
@@ -161,10 +178,11 @@ install_printer Cabs_debug.pp_attrs
install_printer Cabs_debug.pp_file
EOF
else
-GEN_OCAMLDEBUG=no;
+GEN_OCAMLDEBUG=${GEN_OCAMLDEBUG:-no};
fi
ocamldebug -I $(ocamlfind query zarith) -I $(ocamlfind query ocamlgraph) \
+ -I $(ocamlfind query compiler-libs) \
-I $FRAMAC_LIB $BINDIR/toplevel.byte "$@"
if test "$GEN_OCAMLDEBUG" = "yes"; then
--
GitLab