diff --git a/Makefile.generating b/Makefile.generating index 47aab1767ad438df8ea431ab2196b900f0fad2c1..44b7af581e1ccfaf2fa40040a8b30562fa6f8df5 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 865bb2a1a3cc44937501df3a1e1c3bcc48ca35a7..3b5c67342df7f34eab75292e36574b0abc286672 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 5bcf5b6934d16d734977e0ceaf9ead9c3750d7a3..fc11f04b2a3dc4796e8ac70d30df72e550d4ba4e 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 d9d2df2f8410bc17975771451c8e078f4d6b2943..9bf91c20b57b44cc8b5384ef788d8dc6e9d9bf85 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 64d0d6886f4089dde66bc6db57644974ef5ba324..a3b9d3aef19d9e3d46e4db36c8db4e00d93d6438 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} *) (* ************************************************************************* *)