From 244f9a3dda247adbfb569ca06d20f0b4bbbd1552 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Mon, 21 Jan 2019 11:16:22 +0100
Subject: [PATCH] [Kernel] make yojson a mandatory dependence
---
INSTALL.md | 2 +-
Makefile | 14 -------
Makefile.generating | 1 -
configure.in | 27 +++++--------
doc/userman/user-sources.tex | 5 +--
headers/header_spec.txt | 3 +-
man/frama-c.1 | 2 -
man/frama-c.1.md | 3 +-
nix/default.nix | 2 +-
opam/opam | 4 +-
share/Makefile.config.in | 11 +----
src/kernel_internals/runtime/config.ml.in | 2 -
src/kernel_internals/runtime/config.mli | 5 ---
.../json_compilation_database.ko.ml | 34 ----------------
...ase.ok.ml => json_compilation_database.ml} | 2 +-
.../plugin_entry_points/kernel.ml | 40 +++----------------
.../plugin_entry_points/kernel.mli | 2 +-
17 files changed, 27 insertions(+), 132 deletions(-)
delete mode 100644 src/kernel_services/ast_queries/json_compilation_database.ko.ml
rename src/kernel_services/ast_queries/{json_compilation_database.ok.ml => json_compilation_database.ml} (99%)
diff --git a/INSTALL.md b/INSTALL.md
index 4fdc7fd8b30..a23be4576a5 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -88,7 +88,7 @@ Frama-C 18 (Argon):
- mlgmpidl.1.2.7 (optional)
- ocamlgraph.1.8.8
- why3.0.88.3
-- yojson.1.4.1 (optional)
+- yojson.1.4.1
- zarith.1.7
Note: *pin recommended* indicates packages likely to become incompatible in
diff --git a/Makefile b/Makefile
index 5d51fd0d81a..1d64170d82c 100644
--- a/Makefile
+++ b/Makefile
@@ -646,20 +646,6 @@ GENERATED += $(addprefix src/kernel_internals/parsing/,\
logic_parser.mli logic_preprocess.ml)
-ifeq ($(HAS_YOJSON),yes)
-src/kernel_services/ast_queries/json_compilation_database.ml: \
- src/kernel_services/ast_queries/json_compilation_database.ok.ml share/Makefile.config
- $(CP_IF_DIFF) $< $@
- $(CHMOD_RO) $@
-else
-src/kernel_services/ast_queries/json_compilation_database.ml: \
- src/kernel_services/ast_queries/json_compilation_database.ko.ml share/Makefile.config
- $(CP_IF_DIFF) $< $@
- $(CHMOD_RO) $@
-endif
-GENERATED += src/kernel_services/ast_queries/json_compilation_database.ml
-
-
.PHONY: check-logic-parser-wildcard
check-logic-parser-wildcard:
cd src/kernel_internals/parsing && ocaml check_logic_parser.ml
diff --git a/Makefile.generating b/Makefile.generating
index 568a02af72e..04faf2bbc7a 100644
--- a/Makefile.generating
+++ b/Makefile.generating
@@ -64,7 +64,6 @@ $(CONFIG_FILE): $(CONFIG_FILE).in VERSION VERSION_CODENAME share/Makefile.config
-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)|" \
-e "s|@MAJOR_VERSION@|$(MAJOR_VERSION)|" \
-e "s|@MINOR_VERSION@|$(MINOR_VERSION)|" \
diff --git a/configure.in b/configure.in
index e5bd40a6513..9d7af978abd 100644
--- a/configure.in
+++ b/configure.in
@@ -322,6 +322,17 @@ else
AC_MSG_RESULT(found)
fi
+# yojson
+########
+
+AC_MSG_CHECKING(for Yojson)
+
+YOJSON=$($OCAMLFIND query yojson -format %v)
+if test -z "$YOJSON" ; then
+ AC_MSG_ERROR(Cannot find yojson via ocamlfind \
+(requires yojson 1.4.1 or higher).)
+fi
+
#################################################
# Check for other (optional) tools/libraries #
#################################################
@@ -344,21 +355,6 @@ fi
AC_CHECK_PROG(OTAGS,otags,otags,)
-# yojson
-########
-
-AC_MSG_CHECKING(for Yojson)
-
-YOJSON_PATH=$($OCAMLFIND query yojson 2>/dev/null | tr -d '\r\n')
-if test -f "$YOJSON_PATH/yojson.$OBJ_SUFFIX"; then
- HAS_YOJSON="yes";
- AC_MSG_RESULT(found)
-else
- HAS_YOJSON="no";
- AC_MSG_RESULT(yojson not found. Kernel option -json-compilation-database won't be available.)
-fi;
-
-
# apron
########
@@ -1024,7 +1020,6 @@ AC_SUBST(VERBOSEMAKE)
AC_SUBST(DEVELOPMENT)
AC_SUBST(DOT)
AC_SUBST(HAS_DOT)
-AC_SUBST(HAS_YOJSON)
AC_SUBST(HAS_APRON)
AC_SUBST(HAS_MPFR)
AC_SUBST(HAS_LANDMARKS)
diff --git a/doc/userman/user-sources.tex b/doc/userman/user-sources.tex
index d07054ba2be..0c352fbc84c 100644
--- a/doc/userman/user-sources.tex
+++ b/doc/userman/user-sources.tex
@@ -1,4 +1,4 @@
-\chapter{Preparing the Sources}
+ojson\chapter{Preparing the Sources}
\label{user-sources}
This chapter explains how to specify the source files that form the
@@ -49,8 +49,7 @@ directories (\texttt{-I} switches), as in
\texttt{-cpp-extra-args="-DDEBUG -DARCH=ia32 -I./headers"}.
If you have a JSON compilation database file\footnote{%
- \url{http://clang.llvm.org/docs/JSONCompilationDatabase.html}} (and if your
-\FramaC was compiled with \texttt{yojson} support), you can use
+ \url{http://clang.llvm.org/docs/JSONCompilationDatabase.html}}, you can use
it to retrieve preprocessing macros such as \texttt{-D} and \texttt{-I}
for each file in the database, via option
\optiondef{-}{json-compilation-database} \texttt{<path>}, where \texttt{<path>}
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 7a59f56fa0a..c60f329e2a1 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -528,9 +528,8 @@ src/kernel_services/ast_queries/file.ml: CEA_LGPL
src/kernel_services/ast_queries/file.mli: CEA_LGPL
src/kernel_services/ast_queries/filecheck.ml: CEA_LGPL
src/kernel_services/ast_queries/filecheck.mli: CEA_LGPL
-src/kernel_services/ast_queries/json_compilation_database.ko.ml: CEA_LGPL
+src/kernel_services/ast_queries/json_compilation_database.ml: CEA_LGPL
src/kernel_services/ast_queries/json_compilation_database.mli: CEA_LGPL
-src/kernel_services/ast_queries/json_compilation_database.ok.ml: CEA_LGPL
src/kernel_services/ast_queries/logic_const.ml: CEA_INRIA_LGPL
src/kernel_services/ast_queries/logic_const.mli: CEA_INRIA_LGPL
src/kernel_services/ast_queries/logic_env.ml: CEA_INRIA_LGPL
diff --git a/man/frama-c.1 b/man/frama-c.1
index 8195efa760f..a9ad49458ae 100644
--- a/man/frama-c.1
+++ b/man/frama-c.1
@@ -383,8 +383,6 @@ specifications in \f[I]path\f[].
If \f[I]path\f[] is a directory, use
\f[B]<path>/compile_commands.json\f[].
Disabled by default.
-\f[B]Note\f[]: this option is only available if Frama\-C was compiled
-with yojson support.
.RS
.RE
.TP
diff --git a/man/frama-c.1.md b/man/frama-c.1.md
index 36031b4fd79..b4aece519c7 100644
--- a/man/frama-c.1.md
+++ b/man/frama-c.1.md
@@ -230,8 +230,7 @@ Defaults to **frama_c_journal**.
for more information): each file preprocessed by Frama-C will include
corresponding **-I** and **-D** flags according to the specifications in *path*.
If *path* is a directory, use **\<path>/compile_commands.json**.
-Disabled by default. **Note**: this option is only available if Frama-C was
-compiled with yojson support.
+Disabled by default.
[-no]-keep-comments
: tries to preserve comments when pretty-printing the source code.
diff --git a/nix/default.nix b/nix/default.nix
index 4cc5134a468..3717e307479 100644
--- a/nix/default.nix
+++ b/nix/default.nix
@@ -3,7 +3,7 @@
let mk_buildInputs = { opamPackages ? [] } :
[ pkgs.gnugrep pkgs.gnused pkgs.autoconf pkgs.gnumake pkgs.gcc pkgs.ncurses pkgs.time pkgs.python3 pkgs.perl pkgs.file] ++ opam2nix.build {
- specs = opam2nix.toSpecs ([ "ocamlfind" "zarith" "ocamlgraph"
+ specs = opam2nix.toSpecs ([ "ocamlfind" "zarith" "ocamlgraph" "yojson"
{ name = "coq"; constraint = "=8.7.2"; }
] ++ opamPackages ++
(if ocaml_version == "pkgs.ocaml-ng.ocamlPackages_4_02.ocaml"
diff --git a/opam/opam b/opam/opam
index d8f0366beb9..e5bb63baad4 100644
--- a/opam/opam
+++ b/opam/opam
@@ -94,10 +94,10 @@ depends: [
"conf-gtksourceview"
( "alt-ergo-free" | "alt-ergo" )
"conf-graphviz" { post }
+ "yojson"
]
depopts: [
- "yojson" { build & >= "1.6.0" }
"coq" { build }
"why3" { build }
"mlgmpidl" { build }
@@ -116,8 +116,6 @@ conflicts: [
]
messages: [
- "Yojson enables kernel option -json-compilation-database"
- {!yojson:installed}
"Why3 can be used by the WP plug-in for running additional automatic solvers"
{!why3:installed}
"Coq can be used with the WP plug-in for proving interactively proof obligations"
diff --git a/share/Makefile.config.in b/share/Makefile.config.in
index af34cfa5a5c..f6b545148e7 100644
--- a/share/Makefile.config.in
+++ b/share/Makefile.config.in
@@ -120,9 +120,6 @@ endif
# lablgnomecanvas
HAS_GNOMECANVAS ?=@HAS_GNOMECANVAS@
-# yojson
-HAS_YOJSON ?=@HAS_YOJSON@
-
# apron
HAS_APRON ?=@HAS_APRON@
@@ -160,9 +157,7 @@ THREAD_IS_KEYWORD ?=@THREAD_IS_KEYWORD@
TEST_DIRS_AS_PLUGIN:=\
dynamic dynamic_plugin journal saveload spec misc syntax cil \
pretty_printing builtins libc value fc_script
-ifeq ("$(HAS_YOJSON)","yes")
TEST_DIRS_AS_PLUGIN+=jcdb
-endif
PLUGIN_TESTS_LIST+=$(TEST_DIRS_AS_PLUGIN)
##########################
@@ -190,16 +185,12 @@ ENABLE_USERS ?=@ENABLE_USERS@
ENABLE_EVA ?=@ENABLE_EVA@
#bytes is part of the stdlib, but is used as a transitional package.
-LIBRARY_NAMES := findlib ocamlgraph unix str dynlink bytes zarith
+LIBRARY_NAMES := findlib ocamlgraph unix str dynlink bytes zarith yojson
ifeq ($(HAS_LANDMARKS),yes)
LIBRARY_NAMES += landmarks landmarks.ppx
endif
-ifeq ($(HAS_YOJSON),yes)
-LIBRARY_NAMES += yojson
-endif
-
ifneq ($(ENABLE_GUI),no)
LIBRARY_NAMES_GUI = $(LABLGTK) $(GTKSOURCEVIEW)
ifeq ($(HAS_GNOMECANVAS),yes)
diff --git a/src/kernel_internals/runtime/config.ml.in b/src/kernel_internals/runtime/config.ml.in
index c0f5852814a..cb7c24c0576 100644
--- a/src/kernel_internals/runtime/config.ml.in
+++ b/src/kernel_internals/runtime/config.ml.in
@@ -97,6 +97,4 @@ 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 d223daf3b96..80c125ae0c0 100644
--- a/src/kernel_internals/runtime/config.mli
+++ b/src/kernel_internals/runtime/config.mli
@@ -130,11 +130,6 @@ 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 Chlorine-20180501
-*)
-
(*
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
deleted file mode 100644
index 1536859cce6..00000000000
--- a/src/kernel_services/ast_queries/json_compilation_database.ko.ml
+++ /dev/null
@@ -1,34 +0,0 @@
-(**************************************************************************)
-(* *)
-(* This file is part of Frama-C. *)
-(* *)
-(* Copyright (C) 2007-2019 *)
-(* CEA (Commissariat à l'énergie atomique et aux énergies *)
-(* alternatives) *)
-(* *)
-(* you can redistribute it and/or modify it under the terms of the GNU *)
-(* Lesser General Public License as published by the Free Software *)
-(* Foundation, version 2.1. *)
-(* *)
-(* It is distributed in the hope that it will be useful, *)
-(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
-(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
-(* GNU Lesser General Public License for more details. *)
-(* *)
-(* See the GNU Lesser General Public License version 2.1 *)
-(* for more details (enclosed in the file licenses/LGPLv2.1). *)
-(* *)
-(**************************************************************************)
-
-let get_flags _ =
- 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/ast_queries/json_compilation_database.ok.ml b/src/kernel_services/ast_queries/json_compilation_database.ml
similarity index 99%
rename from src/kernel_services/ast_queries/json_compilation_database.ok.ml
rename to src/kernel_services/ast_queries/json_compilation_database.ml
index 8d31f5b6709..e813c4ddcb7 100644
--- a/src/kernel_services/ast_queries/json_compilation_database.ok.ml
+++ b/src/kernel_services/ast_queries/json_compilation_database.ml
@@ -131,7 +131,7 @@ let split_command_args s =
never need quotes. *)
let quote_define_argument arg = Format.sprintf "%S" arg
-let parse_entry ?(cwd=Sys.getcwd()) (r : Yojson.Basic.t) =
+let parse_entry ?(cwd=Sys.getcwd()) r =
let open Yojson.Basic.Util in
let filename = r |> member "file" |> to_string in
let dirname = r |> member "directory" |> to_string_option |> Extlib.opt_conv "" in
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index 31065775b51..e77d3bf7ff4 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -1024,48 +1024,20 @@ module C11 =
let () = Parameter_customize.set_group parsing
let () = Parameter_customize.do_not_reset_on_copy ()
-module JsonCompilationDatabaseOption =
+module JsonCompilationDatabase =
String
(struct
- let module_name = "JsonCompilationDatabaseOption"
+ let module_name = "JsonCompilationDatabase"
let option_name = "-json-compilation-database"
let default = ""
let arg_name = "path"
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)
-
-(* This module holds the real value of the option. It is only updated
- if Yojson support has been compiled. Otherwise, attempt to use
- -json-compilation-database results in a warning.
-*)
-module JsonCompilationDatabase =
- State_builder.Ref(Datatype.String)
- (struct
- let name = "JsonCompilationDatabase"
- let dependencies = [ JsonCompilationDatabaseOption.self ]
- let default () = ""
+ "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."
end)
-let () =
- if Fc_config.has_yojson then
- JsonCompilationDatabaseOption.add_set_hook
- (fun _ new_opt -> JsonCompilationDatabase.set new_opt)
- else begin
- JsonCompilationDatabaseOption.add_set_hook
- (fun _ _ ->
- warning ~once:true
- "trying to set -json-compilation-database even though Yojson \
- is not available. Ignoring argument.")
- end
-
(* ************************************************************************* *)
(** {2 Customizing Normalization} *)
(* ************************************************************************* *)
diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli
index c837fb5a091..cf9edf9d0fb 100644
--- a/src/kernel_services/plugin_entry_points/kernel.mli
+++ b/src/kernel_services/plugin_entry_points/kernel.mli
@@ -444,7 +444,7 @@ module ImplicitFunctionDeclaration: Parameter_sig.String
module C11: Parameter_sig.Bool
(** Behavior of option "-c11" *)
-module JsonCompilationDatabase: State_builder.Ref with type data = string
+module JsonCompilationDatabase: Parameter_sig.String
(** Behavior of option "-json-compilation-database" *)
(* ************************************************************************* *)
--
GitLab