Merge branch 'feature/andre/remove-frama-c-config' into 'master'

Feature/andre/remove frama c config

See merge request frama-c/frama-c!2882

INSTALL.md

@@ -414,7 +414,7 @@ available:
 
 - `frama-c`
 - `frama-c-gui`       if available
-- `frama-c-config`    displays Frama-C configuration paths
+- `frama-c-config`    lightweight wrapper used to display configuration paths
 - `frama-c.byte`      bytecode version of frama-c
 - `frama-c-gui.byte`  bytecode version of frama-c-gui, if available
 - `ptests.opt`        testing tool for Frama-c

Makefile

@@ -338,7 +338,7 @@ DOC_GEN_FILES:=$(addprefix doc/code/,\
 
 # additional compilation targets for 'make all'.
 # cannot be delayed after 'make all'
-EXTRAS	= ptests bin/fc-config$(EXE)
+EXTRAS	= ptests
 
 ifneq ($(ENABLE_GUI),no)
 ifeq ($(HAS_LABLGTK),yes)
@@ -1980,9 +1980,7 @@ install:: install-lib-$(OCAMLBEST)
 	fi
 	$(CP) bin/ptests.$(OCAMLBEST)$(EXE) \
 	      $(BINDIR)/ptests.$(OCAMLBEST)$(EXE)
-	if [ -x bin/fc-config$(EXE) ] ; then \
-		$(CP) bin/fc-config$(EXE) $(BINDIR)/frama-c-config$(EXE); \
-	fi
+	$(CP) bin/frama-c-config $(BINDIR)/frama-c-config; \
 	if [ -x bin/frama-c-script ] ; then \
 		$(CP) bin/frama-c-script $(BINDIR)/frama-c-script; \
 	fi
@@ -2237,7 +2235,6 @@ clean:: $(PLUGIN_LIST:=_CLEAN) \
 	$(PRINT_RM) binaries
 	$(RM) bin/toplevel.byte$(EXE) bin/viewer.byte$(EXE) \
 		bin/ptests.byte$(EXE) bin/*.opt$(EXE) bin/toplevel.top$(EXE)
-	$(RM) bin/fc-config$(EXE)
 
 smartclean:
 	$(MAKE) -f share/Makefile.clean smartclean

Makefile.generating

@@ -158,30 +158,6 @@ else
 	$(CHMOD_RO) $@
 endif
 
-##################
-# Frama-C-config #
-##################
-
-src/kernel_internals/runtime/frama_c_config.ml: src/kernel_internals/runtime/fc_config.ml \
-	src/kernel_internals/runtime/frama_c_config.ml.in Makefile.generating
-	$(PRINT_MAKING) $@
-	$(RM) $@
-	$(ECHO) "module Filepath = struct let add_symbolic_dir _ _ = () end" >> $@
-	$(ECHO) "module Fc_config = struct" >> $@
-	$(CAT) src/kernel_internals/runtime/fc_config.ml >> $@
-	$(ECHO) "end" >> $@
-	$(CAT) src/kernel_internals/runtime/frama_c_config.ml.in >> $@
-	$(CHMOD_RO) $@
-
-GENERATED+= src/kernel_internals/runtime/frama_c_config.ml
-
-bin/fc-config$(EXE): src/kernel_internals/runtime/frama_c_config.ml
-ifeq ($(OCAMLBEST),opt)
-	$(OCAMLOPT) str.cmxa $< -o $@
-else
-	$(OCAMLC) str.cma $< -o $@
-endif
-
 # Merlin #
 
 .PHONY:merlin

bin/frama-c-config

@@ -21,7 +21,4 @@
 #                                                                        #
 ##########################################################################
 
-
-. $(dirname $0)/local_export.sh
-
-exec $BINDIR/fc-config "$@"
+exec $(dirname $0)/frama-c -no-autoload-plugins "$@"

headers/header_spec.txt

@@ -371,7 +371,6 @@ src/kernel_internals/runtime/dump_config.ml: CEA_LGPL
 src/kernel_internals/runtime/dump_config.mli: CEA_LGPL
 src/kernel_internals/runtime/fc_config.ml.in: CEA_LGPL
 src/kernel_internals/runtime/fc_config.mli: CEA_LGPL
-src/kernel_internals/runtime/frama_c_config.ml.in: CEA_LGPL
 src/kernel_internals/runtime/frama_c_init.ml: CEA_LGPL
 src/kernel_internals/runtime/frama_c_init.mli: CEA_LGPL
 src/kernel_internals/runtime/gui_init.ml: CEA_LGPL

src/kernel_internals/runtime/frama_c_config.ml.in

-(**************************************************************************)
-(*                                                                        *)
-(*  This file is part of Frama-C.                                         *)
-(*                                                                        *)
-(*  Copyright (C) 2007-2020                                               *)
-(*    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).            *)
-(*                                                                        *)
-(**************************************************************************)
-
-# 24 "src/kernel_internals/runtime/frama_c_config.ml.in"
-
-(** This file is *not* linked in Frama-C. Instead, is it is concatenated
-    to Config, to create a standalone executable *)
-
-let version _ =
-  Format.printf
-    "Frama-C %s (%s)@\n\
-     Environment:@\n  \
-       FRAMAC_SHARE  = %S@\n  \
-       FRAMAC_LIB    = %S@\n  \
-       FRAMAC_PLUGIN = %S@."
-    Fc_config.version Fc_config.codename
-    Fc_config.datadir Fc_config.libdir Fc_config.plugin_path
-  ;
-  exit 0
-
-let options = Arg.([
-  "-print-share-path",
-  Unit (fun _ -> Format.printf "%s%!" Fc_config.datadir; exit 0),
-  " Print the path of Frama-C share directory";
-
-  "-share",
-  Unit (fun _ -> Format.printf "%s%!" Fc_config.datadir; exit 0),
-  " Alias for -print-share-path";
-
-  "-libc",
-  Unit (fun _ -> Format.printf "%s%!"
-           (Filename.concat Fc_config.datadir "libc"); exit 0),
-  " Print the path of Frama-C standard library directory";
-
-  "-scripts",
-  Unit (fun _ -> Format.printf "%s%!"
-           (Filename.concat Fc_config.datadir "analysis-scripts"); exit 0),
-  " Print the path of Frama-C analysis-scripts directory";
-
-  "-print-libpath",
-  Unit (fun _ -> Format.printf "%s%!" Fc_config.libdir; exit 0),
-  " Print the path of Frama-C kernel library";
-
-  "-libpath",
-  Unit (fun _ -> Format.printf "%s%!" Fc_config.libdir; exit 0),
-  " Alias for -print-libpath";
-
-  "-print-plugin-path",
-  Unit (fun _ -> Format.printf "%s%!" Fc_config.plugin_path; exit 0),
-  " Print the path where Frama-C dynamic plug-ins are searched for";
-
-  "-plugin-path",
-  Unit (fun _ -> Format.printf "%s%!" Fc_config.plugin_path; exit 0),
-  " Alias for -print-plugin-path";
-
-  "-print-version",
-  Unit (fun _ -> Format.printf "%s%!" Fc_config.version; exit 0),
-  " Print the version number of Frama-C";
-
-  "-version",
-  Unit version,
-  " Display full version and configuration information"
-])
-
-let usage = "\
-Usage:  frama-c-config <option>"
-
-let () =
-  Arg.parse options (fun _ -> ()) usage;
-  version () (* We only get here if no option has been specified *)