diff --git a/INSTALL.md b/INSTALL.md
index 4fdc7fd8b309cc4cb7bbe1d53f719240657d6fa8..a23be4576a55c29525dcd1991c3af03e28613b2a 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 5d51fd0d81a053bf22fff6c62c7071d0c83a2a08..1d64170d82c445ccf52f7d2992c527b07341280b 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 568a02af72e64b3b4a4a3dc5eb59f60f86d3aa3f..04faf2bbc7a06a9c5326c0fb07a415fda453dd1c 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 e5bd40a6513a1d657def0d283f009bb05147adaa..9d7af978abdac032d2344d65ab3204939ee1a2ad 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 d07054ba2be5b7438a587bf27ba1fe296eb6151f..0c352fbc84c508b0610191cc18168a9fa79571a5 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 7a59f56fa0af6966a004d87d2a7ee43768bc23cb..c60f329e2a1fa61190aa06a7722a339ac9887b2a 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 8195efa760fefebbb1878eb745e3d32d4edca2a7..a9ad49458ae172586ce531afabf03cb8214380be 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 36031b4fd79c4b4396b9c98d58d33cacb533d16e..b4aece519c794ac664fcb063ce6b7d4e7484c328 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 4cc5134a468b55159dd553d21afe8452050d10bd..04a61cb18b32751faebba26ed925ef081c4805bd 100644
--- a/nix/default.nix
+++ b/nix/default.nix
@@ -1,9 +1,9 @@
# paramaterised derivation with dependencies injected (callPackage style)
{ pkgs, stdenv, src ? ../., opam2nix, ocaml_version ? "ocaml-ng.ocamlPackages_4_05.ocaml", plugins ? { } }:
-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"
+let mk_buildInputs = { opamPackages ? [], nixPackages ? [] } :
+ [ pkgs.gnugrep pkgs.gnused pkgs.autoconf pkgs.gnumake pkgs.gcc pkgs.ncurses pkgs.time pkgs.python3 pkgs.perl] ++ nixPackages ++ opam2nix.build {
+ specs = opam2nix.toSpecs ([ "ocamlfind" "zarith" "ocamlgraph" "yojson"
{ name = "coq"; constraint = "=8.7.2"; }
] ++ opamPackages ++
(if ocaml_version == "pkgs.ocaml-ng.ocamlPackages_4_02.ocaml"
@@ -15,7 +15,7 @@ let mk_buildInputs = { opamPackages ? [] } :
in
rec {
- inherit src;
+ inherit src mk_buildInputs;
buildInputs = mk_buildInputs {};
installed = main.out;
main = stdenv.mkDerivation {
diff --git a/nix/frama-ci.nix b/nix/frama-ci.nix
index e26a55d0f058b25b43d59ddd40a3656c951ef440..3976ce7088a3c25cb19a0f142a0452a3526cb14a 100644
--- a/nix/frama-ci.nix
+++ b/nix/frama-ci.nix
@@ -5,8 +5,8 @@ let
src = builtins.fetchGit {
"url" = "https://bobot:${password}@git.frama-c.com/frama-c/Frama-CI.git";
"name" = "Frama-CI";
- "rev" = "70045f4252e668e0facad12d7db2c6ab83fc813b";
- "ref" = "master";
+ "rev" = "ed541f6e3818da2bf31125740b8555acb086ca29";
+ "ref" = "feature/andre/yojson-mandatory-dependence";
};
in
{
diff --git a/opam/opam b/opam/opam
index d8f0366beb9887943e65435726e1292afc1441f0..e5bb63baad4b18b0d5d933d912fe9ef13a7e7e64 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 af34cfa5a5cf9307aeb9d4a237a432b084a05d05..f6b545148e78dc450b717a4f7d9b5c539f4a0cfc 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 c0f5852814ae1f34681f122f7a672be1ee95ed92..cb7c24c057653ceb6af78e8d50670d5487651e83 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 d223daf3b963e3919f947abc024a05619d04c9f4..80c125ae0c08c5d0a3955961112c8ab7235c4bd3 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 1536859cce6c7eb3cf1436e30ce370d607679892..0000000000000000000000000000000000000000
--- 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 8d31f5b6709a8bedd67c52e864f04b4076b00881..e813c4ddcb7649fac11bfa04d99d97f267a9ae70 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 31065775b513da7b9bb861c01a9eeef1b47b9101..e77d3bf7ff4029797ed397fff4a6d27ca01e2d02 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 c837fb5a0919eddb59eabfe811336a46ccf66629..cf9edf9d0fb2f117fcdb109e04ba00d9577bd207 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" *)
(* ************************************************************************* *)