From 5a7fb46852afdfe70e4d7980fb3a69af06b86b71 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Thu, 4 Jan 2018 19:51:23 +0100
Subject: [PATCH] do not set -json-compilation-database when Yojson is not
present
---
Makefile.generating | 1 +
src/kernel_internals/runtime/config.ml.in | 2 ++
src/kernel_internals/runtime/config.mli | 5 ++++
.../json_compilation_database.ko.ml | 13 +++++++---
.../plugin_entry_points/kernel.ml | 25 ++++++++++++++-----
5 files changed, 36 insertions(+), 10 deletions(-)
diff --git a/Makefile.generating b/Makefile.generating
index 47aab1767ad..44b7af581e1 100644
--- a/Makefile.generating
+++ b/Makefile.generating
@@ -61,6 +61,7 @@ $(CONFIG_FILE): $(CONFIG_FILE).in VERSION share/Makefile.config Makefile.generat
-e "s|@COMPILATION_UNITS@|$(COMPILATION_UNITS)|" \
-e "s|@LIBRARY_NAMES@|$(foreach p,$(ALL_LIBRARY_NAMES),\"$p\";)|" \
-e "s|@OPTDOT@|$(OPTDOT)|" \
+ -e "s|@HAS_YOJSON@|$(if $(filter yes,$(HAS_YOJSON)),true,false)|" \
-e "s|@EXE@|$(EXE)|" \
$< > $@.tmp
@touch -r $@.tmp $<
diff --git a/src/kernel_internals/runtime/config.ml.in b/src/kernel_internals/runtime/config.ml.in
index 865bb2a1a3c..3b5c67342df 100644
--- a/src/kernel_internals/runtime/config.ml.in
+++ b/src/kernel_internals/runtime/config.ml.in
@@ -78,4 +78,6 @@ let preprocessor_keep_comments =
let compilation_unit_names = [@COMPILATION_UNITS@]
let library_names = [@LIBRARY_NAMES@]
+let has_yojson = @HAS_YOJSON@
+
let dot = @OPTDOT@
diff --git a/src/kernel_internals/runtime/config.mli b/src/kernel_internals/runtime/config.mli
index 5bcf5b6934d..fc11f04b2a3 100644
--- a/src/kernel_internals/runtime/config.mli
+++ b/src/kernel_internals/runtime/config.mli
@@ -104,6 +104,11 @@ val dot: string option
@return [None] if `dot' is not installed.
@since Carbon-20101201 *)
+val has_yojson: bool
+(** [true] if Frama-C has been compiled with yojson support.
+ @since Frama-C+dev
+*)
+
(*
Local Variables:
compile-command: "make -C ../../.."
diff --git a/src/kernel_services/ast_queries/json_compilation_database.ko.ml b/src/kernel_services/ast_queries/json_compilation_database.ko.ml
index d9d2df2f841..9bf91c20b57 100644
--- a/src/kernel_services/ast_queries/json_compilation_database.ko.ml
+++ b/src/kernel_services/ast_queries/json_compilation_database.ko.ml
@@ -21,9 +21,14 @@
(**************************************************************************)
let get_flags _ =
- if Kernel.JsonCompilationDatabase.get () <> "" then begin
- Kernel.warning ~once:true "ignoring option %s: Frama-C was not compiled \
- with the required libraries (yojson)"
- Kernel.JsonCompilationDatabase.option_name;
+ let db = Kernel.JsonCompilationDatabase.get () in
+ if db <> "" then begin
+ (* If Yojson is disabled, JsonCompilationDatabase prevents any attempt
+ to set the option to a non-empty string. If someone bypasses the
+ mechanism with an unsafe_set, they deserve a fatal error.
+ *)
+ Kernel.fatal
+ "Attempt to parse json compilation database %s \
+ with a Frama-C compiled without Yojson support." db
end;
""
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 64d0d6886f4..a3b9d3aef19 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -864,14 +864,27 @@ module JsonCompilationDatabase =
let option_name = "-json-compilation-database"
let default = ""
let arg_name = "path"
- let help = "when set, preprocessing of each file will include \
- corresponding flags (e.g. -I, -D) from the JSON compilation \
- database specified by <path>. If <path> is a directory, \
- use '<path>/compile_commands.json'. Disabled by default. \
- NOTE: this requires Frama-C to have been compiled with \
- yojson support."
+ let help =
+ if Fc_config.has_yojson then
+ "when set, preprocessing of each file will include corresponding \
+ flags (e.g. -I, -D) from the JSON compilation database \
+ specified by <path>. If <path> is a directory, use \
+ '<path>/compile_commands.json'. Disabled by default. \
+ NOTE: this requires Frama-C to be compiled with yojson support."
+ else
+ "Unsupported: recompile Frama-C with Yojson library to enable it"
end)
+let () =
+ if not Fc_config.has_yojson then begin
+ JsonCompilationDatabase.add_set_hook
+ (fun _ _ ->
+ warning ~once:true
+ "trying to set -json-compilation-database even though Yojson \
+ is not available. Ignoring argument.";
+ JsonCompilationDatabase.clear ())
+ end
+
(* ************************************************************************* *)
(** {2 Customizing Normalization} *)
(* ************************************************************************* *)
--
GitLab