diff --git a/INSTALL.md b/INSTALL.md index b9d1bf2c5b67a80763f03d29cb69445bf4d9acfb..662edf1da292d336cacb342e1bce01ee8591532c 100644 --- a/INSTALL.md +++ b/INSTALL.md @@ -415,7 +415,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 diff --git a/Makefile b/Makefile index 64c9342a84132a7b20497f917d6822f09645d03b..2dcdb559eeb574801801b8ccf130cfd548ba66dd 100644 --- a/Makefile +++ b/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) @@ -1979,9 +1979,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 @@ -2236,7 +2234,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 diff --git a/Makefile.generating b/Makefile.generating index 1c89d12715aba8629f180701b1d767f9df1620f0..256316a60ebf16ac0ff22ab2aed6ca96fc187d74 100644 --- a/Makefile.generating +++ b/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 diff --git a/bin/frama-c-config b/bin/frama-c-config index be9eed99a62f14309d63061b1a2b55d1bc884f28..fb19e40f4764c2c8ab2c86b474a9e0b72396f38c 100755 --- a/bin/frama-c-config +++ b/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 "$@" diff --git a/headers/header_spec.txt b/headers/header_spec.txt index 3292d5c140719b154d3caefeac71af3922106fdf..1f2bf78c937580d526ed56fc17766e61cc3e3e11 100644 --- a/headers/header_spec.txt +++ b/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 diff --git a/src/kernel_internals/runtime/frama_c_config.ml.in b/src/kernel_internals/runtime/frama_c_config.ml.in deleted file mode 100644 index 6b0e200a724380edfba96d88e2aaa62243da89fb..0000000000000000000000000000000000000000 --- a/src/kernel_internals/runtime/frama_c_config.ml.in +++ /dev/null @@ -1,89 +0,0 @@ -(**************************************************************************) -(* *) -(* 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 *)