From f285b47b78693de88d2026b6bef882586387bf71 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Thu, 8 Sep 2022 10:55:59 +0200
Subject: [PATCH] [Analysis-scripts] move scripts to libexec/lib section
---
bin/frama-c-script | 25 +++----
doc/userman/user-analysis-scripts.tex | 4 +-
dune-project | 2 +-
share/analysis-scripts/build.py | 6 +-
share/analysis-scripts/creduce.sh | 8 +--
share/analysis-scripts/template.mk | 8 +--
share/dune | 90 ++++++++++++++----------
src/plugins/eva/engine/recursion.ml | 2 +-
tests/fc_script/make-for-make-wrapper.mk | 4 +-
tests/fc_script/oracle/GNUmakefile | 8 +--
10 files changed, 86 insertions(+), 71 deletions(-)
diff --git a/bin/frama-c-script b/bin/frama-c-script
index 06e66c57155..2ea801b4290 100755
--- a/bin/frama-c-script
+++ b/bin/frama-c-script
@@ -123,6 +123,7 @@ cd "$WORKING_DIR"
# All scripts called by frama-c-script may rely on FRAMAC_BIN pointing to the
# directory containing frama-c, frama-c-config and frama-c-script.
export FRAMAC_BIN="$DIR"
+FRAMAC_LIB=$("${DIR}/frama-c-config" -print-lib-path)
FRAMAC_SHARE=$("${DIR}/frama-c-config" -print-share-path)
if [ -z ${FRAMAC_SESSION+x} ]; then
FRAMAC_SESSION="./.frama-c";
@@ -179,7 +180,7 @@ flamegraph() {
mkdir "$dir" || { echo "error: could not create '$dir'"; exit 1; }
fi
out_svg="$dir/flamegraph.svg"
- "${FRAMAC_SHARE}/analysis-scripts/flamegraph.pl" \
+ "${FRAMAC_LIB}/analysis-scripts/flamegraph.pl" \
--title "Eva Flamegraph" --inverted --hash "$path" \
--width 1400 --fontsize 11 > "$out_svg.tmp"
if [ ! $? -eq 0 ]; then
@@ -221,11 +222,11 @@ case "$command" in
;;
"build")
shift;
- ${FRAMAC_SHARE}/analysis-scripts/build.py "$@";
+ ${FRAMAC_LIB}/analysis-scripts/build.py "$@";
;;
"list-files")
shift;
- "${FRAMAC_SHARE}"/analysis-scripts/list_files.py "$@";
+ "${FRAMAC_LIB}"/analysis-scripts/list_files.py "$@";
;;
"list-functions")
shift;
@@ -236,7 +237,7 @@ case "$command" in
;;
"find-fun")
shift;
- "${FRAMAC_SHARE}"/analysis-scripts/find_fun.py "$@";
+ "${FRAMAC_LIB}"/analysis-scripts/find_fun.py "$@";
;;
"flamegraph")
shift;
@@ -244,7 +245,7 @@ case "$command" in
;;
"summary")
shift;
- "${FRAMAC_SHARE}"/analysis-scripts/summary.py "$@";
+ "${FRAMAC_LIB}"/analysis-scripts/summary.py "$@";
;;
"configure")
shift;
@@ -252,31 +253,31 @@ case "$command" in
;;
"heuristic-print-callgraph")
shift;
- ${FRAMAC_SHARE}/analysis-scripts/print_callgraph.py "$@";
+ ${FRAMAC_LIB}/analysis-scripts/print_callgraph.py "$@";
;;
"heuristic-detect-recursion")
shift;
- ${FRAMAC_SHARE}/analysis-scripts/detect_recursion.py "$@";
+ ${FRAMAC_LIB}/analysis-scripts/detect_recursion.py "$@";
;;
"heuristic-list-functions")
shift;
- ${FRAMAC_SHARE}/analysis-scripts/heuristic_list_functions.py "$@";
+ ${FRAMAC_LIB}/analysis-scripts/heuristic_list_functions.py "$@";
;;
"estimate-difficulty")
shift;
- ${FRAMAC_SHARE}/analysis-scripts/estimate_difficulty.py "$@";
+ ${FRAMAC_LIB}/analysis-scripts/estimate_difficulty.py "$@";
;;
"make-wrapper")
shift;
- "${FRAMAC_SHARE}"/analysis-scripts/make_wrapper.py "$0" "$@";
+ "${FRAMAC_LIB}"/analysis-scripts/make_wrapper.py "$0" "$@";
;;
"normalize-jcdb")
shift;
- "${FRAMAC_SHARE}"/analysis-scripts/normalize_jcdb.py "$@";
+ "${FRAMAC_LIB}"/analysis-scripts/normalize_jcdb.py "$@";
;;
"creduce")
shift;
- ${FRAMAC_SHARE}/analysis-scripts/creduce.sh "$@";
+ ${FRAMAC_LIB}/analysis-scripts/creduce.sh "$@";
;;
*)
echo "error: unrecognized command: $command";
diff --git a/doc/userman/user-analysis-scripts.tex b/doc/userman/user-analysis-scripts.tex
index 05a4b6b60d3..34b188eef76 100644
--- a/doc/userman/user-analysis-scripts.tex
+++ b/doc/userman/user-analysis-scripts.tex
@@ -32,7 +32,7 @@ Most scripts are accessible via the \texttt{frama-c-script} command, installed
along with \FramaC. Running this command without any arguments prints the list
of commands, with a brief description of each of them. Some extra scripts are
available by directly running them; in both cases, the actual scripts
-themselves are installed in Frama-C's \texttt{share} directory, underneath
+themselves are installed in Frama-C's \texttt{lib} directory, underneath
\texttt{analysis-scripts}.
\subsection{General Framework}
@@ -434,7 +434,7 @@ The following commands require a JSON Compilation Database.
Finally, there is the following script, which is {\em not} available as a
command in \texttt{frama-c-script}, since its usage scenario is very
different. It is available at\\
-\texttt{\$FRAMAC\_SHARE/analysis-scripts/creduce.sh}.
+\texttt{\$FRAMAC\_LIB/analysis-scripts/creduce.sh}.
\begin{description}
\item[creduce.sh]: A script to help running the C-Reduce\footnote{%
diff --git a/dune-project b/dune-project
index acebea6b498..84cf0d2f2e8 100644
--- a/dune-project
+++ b/dune-project
@@ -22,4 +22,4 @@
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(using dune_site 0.1)
-(package (name frama-c) (sites (share share) (lib plugins) (lib plugins_gui)))
+(package (name frama-c) (sites (share share) (libexec lib) (lib plugins) (lib plugins_gui)))
diff --git a/share/analysis-scripts/build.py b/share/analysis-scripts/build.py
index d93bd3ec9fc..f392d8a1913 100755
--- a/share/analysis-scripts/build.py
+++ b/share/analysis-scripts/build.py
@@ -212,7 +212,7 @@ def copy_fc_stubs():
global fc_stubs_copied
dest = dot_framac_dir / "fc_stubs.c"
if not fc_stubs_copied:
- fc_stubs = lines_of_file(share_dir / "analysis-scripts" / "fc_stubs.c")
+ fc_stubs = lines_of_file(lib_dir / "analysis-scripts" / "fc_stubs.c")
re_main = re.compile(r"\bmain\b")
for i, line in enumerate(fc_stubs):
if line.startswith("//"):
@@ -370,7 +370,7 @@ if not dot_framac_dir.is_dir():
dot_framac_dir.mkdir(parents=True, exist_ok=False)
fc_config = json.loads(call_and_get_output([framac_bin / "frama-c", "-print-config-json"]))
-share_dir = Path(fc_config["datadir"])
+lib_dir = Path(fc_config["lib_dir"])
# copy fc_stubs if at least one main function has arguments
any_has_arguments = False
@@ -391,7 +391,7 @@ if any_has_arguments:
gnumakefile = dot_framac_dir / "GNUmakefile"
-template = lines_of_file(share_dir / "analysis-scripts" / "template.mk")
+template = lines_of_file(lib_dir / "analysis-scripts" / "template.mk")
if machdep:
machdeps = fc_config["machdeps"]
diff --git a/share/analysis-scripts/creduce.sh b/share/analysis-scripts/creduce.sh
index 3dab5bcfe51..d093ceea76f 100755
--- a/share/analysis-scripts/creduce.sh
+++ b/share/analysis-scripts/creduce.sh
@@ -155,8 +155,8 @@ else
fi
echo "[info] using FRAMAC: $FRAMAC"
-if [ -z "$FRAMAC_SHARE" ]; then
- FRAMAC_SHARE="$("$FRAMAC" -print-share-path)"
+if [ -z "$FRAMAC_LIB" ]; then
+ FRAMAC_LIB="$("$FRAMAC" -print-lib-path)"
fi
if ! sed --version >/dev/null 2>&1; then
@@ -230,10 +230,10 @@ if [ ! -e "$script_for_creduce" ]; then
read -p "Please enter 1 or 2: " errorkind
case $errorkind in
1)
- cp "$FRAMAC_SHARE/analysis-scripts/script_for_creduce_fatal.sh" "$script_for_creduce"
+ cp "$FRAMAC_LIB/analysis-scripts/script_for_creduce_fatal.sh" "$script_for_creduce"
;;
2)
- cp "$FRAMAC_SHARE/analysis-scripts/script_for_creduce_non_fatal.sh" "$script_for_creduce"
+ cp "$FRAMAC_LIB/analysis-scripts/script_for_creduce_non_fatal.sh" "$script_for_creduce"
echo "Script copied. Please edit $script_for_creduce and re-run this script."
exit 0
;;
diff --git a/share/analysis-scripts/template.mk b/share/analysis-scripts/template.mk
index 54cdd1332ac..650a01dd63c 100644
--- a/share/analysis-scripts/template.mk
+++ b/share/analysis-scripts/template.mk
@@ -29,10 +29,10 @@
# an optional include, unnecessary if frama-c is in the PATH.
FRAMAC ?= frama-c # FRAMAC is defined in path.mk when it is included, but the
# user can override it in the command-line.
-ifeq ($(FRAMAC_SHARE),)
- FRAMAC_SHARE := $(shell $(FRAMAC)-config -print-share-path)
+ifeq ($(FRAMAC_LIB),)
+ FRAMAC_LIB := $(shell $(FRAMAC)-config -print-lib-path)
endif
-include $(FRAMAC_SHARE)/analysis-scripts/prologue.mk
+include $(FRAMAC_LIB)/analysis-scripts/prologue.mk
###############################################################################
# Edit below as needed. Suggested flags are optional.
@@ -66,5 +66,5 @@ main.parse: \
main.c \
### Epilogue. Do not modify this block. #######################################
-include $(FRAMAC_SHARE)/analysis-scripts/epilogue.mk
+include $(FRAMAC_LIB)/analysis-scripts/epilogue.mk
###############################################################################
diff --git a/share/dune b/share/dune
index 0cd0930e72c..8e1aa8af9f9 100644
--- a/share/dune
+++ b/share/dune
@@ -268,44 +268,6 @@
(libc/wchar.h as libc/wchar.h)
(libc/wctype.h as libc/wctype.h)
(libc/wordexp.h as libc/wordexp.h)
-; Analysis scripts
-(analysis-scripts/analysis.mk as analysis-scripts/analysis.mk)
-(analysis-scripts/benchmark_database.py as analysis-scripts/benchmark_database.py)
-(analysis-scripts/bench-sqlite.sh as analysis-scripts/bench-sqlite.sh)
-(analysis-scripts/build_callgraph.py as analysis-scripts/build_callgraph.py)
-(analysis-scripts/build.py as analysis-scripts/build.py)
-(analysis-scripts/clone.sh as analysis-scripts/clone.sh)
-(analysis-scripts/cmd-dep.sh as analysis-scripts/cmd-dep.sh)
-(analysis-scripts/concat-csv.sh as analysis-scripts/concat-csv.sh)
-(analysis-scripts/creduce.sh as analysis-scripts/creduce.sh)
-(analysis-scripts/detect_recursion.py as analysis-scripts/detect_recursion.py)
-(analysis-scripts/epilogue.mk as analysis-scripts/epilogue.mk)
-(analysis-scripts/estimate_difficulty.py as analysis-scripts/estimate_difficulty.py)
-(analysis-scripts/fc_stubs.c as analysis-scripts/fc_stubs.c)
-(analysis-scripts/find_fun.py as analysis-scripts/find_fun.py)
-(analysis-scripts/flamegraph.pl as analysis-scripts/flamegraph.pl)
-(analysis-scripts/frama_c_results.py as analysis-scripts/frama_c_results.py)
-(analysis-scripts/function_finder.py as analysis-scripts/function_finder.py)
-(analysis-scripts/git_utils.py as analysis-scripts/git_utils.py)
-(analysis-scripts/heuristic_list_functions.py as analysis-scripts/heuristic_list_functions.py)
-(analysis-scripts/list_files.py as analysis-scripts/list_files.py)
-(analysis-scripts/list_functions.ml as analysis-scripts/list_functions.ml)
-(analysis-scripts/make_wrapper.py as analysis-scripts/make_wrapper.py)
-(analysis-scripts/normalize_jcdb.py as analysis-scripts/normalize_jcdb.py)
-(analysis-scripts/parse-coverage.sh as analysis-scripts/parse-coverage.sh)
-(analysis-scripts/plot.sh as analysis-scripts/plot.sh)
-(analysis-scripts/print_callgraph.py as analysis-scripts/print_callgraph.py)
-(analysis-scripts/prologue.mk as analysis-scripts/prologue.mk)
-(analysis-scripts/pyproject.toml as analysis-scripts/pyproject.toml)
-(analysis-scripts/readme-graph.graphml as analysis-scripts/readme-graph.graphml)
-(analysis-scripts/readme-graph.svg as analysis-scripts/readme-graph.svg)
-(analysis-scripts/README.md as analysis-scripts/README.md)
-(analysis-scripts/results_display.py as analysis-scripts/results_display.py)
-(analysis-scripts/script_for_creduce_fatal.sh as analysis-scripts/script_for_creduce_fatal.sh)
-(analysis-scripts/script_for_creduce_non_fatal.sh as analysis-scripts/script_for_creduce_non_fatal.sh)
-(analysis-scripts/source_filter.py as analysis-scripts/source_filter.py)
-(analysis-scripts/summary.py as analysis-scripts/summary.py)
-(analysis-scripts/template.mk as analysis-scripts/template.mk)
; Compliance
(compliance/c11_functions.json as compliance/c11_functions.json)
(compliance/c11_headers.json as compliance/c11_headers.json)
@@ -315,3 +277,55 @@
(compliance/nonstandard_identifiers.json as compliance/nonstandard_identifiers.json)
(compliance/posix_identifiers.json as compliance/posix_identifiers.json)
))
+
+; Analysis scripts (executable files)
+(install
+ (package frama-c)
+ (section libexec)
+ (files
+(analysis-scripts/benchmark_database.py as lib/analysis-scripts/benchmark_database.py)
+(analysis-scripts/bench-sqlite.sh as lib/analysis-scripts/bench-sqlite.sh)
+(analysis-scripts/build_callgraph.py as lib/analysis-scripts/build_callgraph.py)
+(analysis-scripts/build.py as lib/analysis-scripts/build.py)
+(analysis-scripts/clone.sh as lib/analysis-scripts/clone.sh)
+(analysis-scripts/cmd-dep.sh as lib/analysis-scripts/cmd-dep.sh)
+(analysis-scripts/concat-csv.sh as lib/analysis-scripts/concat-csv.sh)
+(analysis-scripts/creduce.sh as lib/analysis-scripts/creduce.sh)
+(analysis-scripts/detect_recursion.py as lib/analysis-scripts/detect_recursion.py)
+(analysis-scripts/estimate_difficulty.py as lib/analysis-scripts/estimate_difficulty.py)
+(analysis-scripts/find_fun.py as lib/analysis-scripts/find_fun.py)
+(analysis-scripts/flamegraph.pl as lib/analysis-scripts/flamegraph.pl)
+(analysis-scripts/frama_c_results.py as lib/analysis-scripts/frama_c_results.py)
+(analysis-scripts/function_finder.py as lib/analysis-scripts/function_finder.py)
+(analysis-scripts/git_utils.py as lib/analysis-scripts/git_utils.py)
+(analysis-scripts/heuristic_list_functions.py as lib/analysis-scripts/heuristic_list_functions.py)
+(analysis-scripts/list_files.py as lib/analysis-scripts/list_files.py)
+(analysis-scripts/make_wrapper.py as lib/analysis-scripts/make_wrapper.py)
+(analysis-scripts/normalize_jcdb.py as lib/analysis-scripts/normalize_jcdb.py)
+(analysis-scripts/parse-coverage.sh as lib/analysis-scripts/parse-coverage.sh)
+(analysis-scripts/plot.sh as lib/analysis-scripts/plot.sh)
+(analysis-scripts/print_callgraph.py as lib/analysis-scripts/print_callgraph.py)
+(analysis-scripts/results_display.py as lib/analysis-scripts/results_display.py)
+(analysis-scripts/script_for_creduce_fatal.sh as lib/analysis-scripts/script_for_creduce_fatal.sh)
+(analysis-scripts/script_for_creduce_non_fatal.sh as lib/analysis-scripts/script_for_creduce_non_fatal.sh)
+(analysis-scripts/source_filter.py as lib/analysis-scripts/source_filter.py)
+(analysis-scripts/summary.py as lib/analysis-scripts/summary.py)
+))
+
+; Analysis scripts (non-executable files)
+(install
+ (package frama-c)
+ (section lib)
+ (files
+(analysis-scripts/analysis.mk as lib/analysis-scripts/analysis.mk)
+(analysis-scripts/epilogue.mk as lib/analysis-scripts/epilogue.mk)
+(analysis-scripts/fc_stubs.c as lib/analysis-scripts/fc_stubs.c)
+(analysis-scripts/list_functions.ml as lib/analysis-scripts/list_functions.ml)
+(analysis-scripts/prologue.mk as lib/analysis-scripts/prologue.mk)
+(analysis-scripts/pyproject.toml as lib/analysis-scripts/pyproject.toml)
+(analysis-scripts/readme-graph.graphml as lib/analysis-scripts/readme-graph.graphml)
+(analysis-scripts/readme-graph.svg as lib/analysis-scripts/readme-graph.svg)
+(analysis-scripts/README.md as lib/analysis-scripts/README.md)
+(analysis-scripts/template.mk as lib/analysis-scripts/template.mk)
+
+))
diff --git a/src/plugins/eva/engine/recursion.ml b/src/plugins/eva/engine/recursion.ml
index fb0da4b9b93..5c3d8c60694 100644
--- a/src/plugins/eva/engine/recursion.ml
+++ b/src/plugins/eva/engine/recursion.ml
@@ -53,7 +53,7 @@ let get_spec kinstr kf =
Try to increase@ the %s parameter@ \
or write a correct specification@ for function %a.@\n%t@]"
(* note: the "\n" before the pretty print of the stack is required by:
- FRAMAC_SHARE/analysis-scripts/make_wrapper.py
+ FRAMAC_LIB/analysis-scripts/make_wrapper.py
*)
Kernel_function.pretty kf
Parameters.RecursiveUnroll.name
diff --git a/tests/fc_script/make-for-make-wrapper.mk b/tests/fc_script/make-for-make-wrapper.mk
index 983f2a16d9f..5cac4969ff8 100644
--- a/tests/fc_script/make-for-make-wrapper.mk
+++ b/tests/fc_script/make-for-make-wrapper.mk
@@ -1,6 +1,6 @@
# Customized makefile template for testing 'frama-c-script make-wrapper'.
-include $(shell $(FRAMAC) -no-autoload-plugins -print-share-path)/analysis-scripts/prologue.mk
+include $(shell $(FRAMAC) -no-autoload-plugins -print-lib-path)/analysis-scripts/prologue.mk
FCFLAGS += \
-kernel-warn-key annot:missing-spec=abort \
@@ -18,5 +18,5 @@ make-for-make-wrapper.parse: \
# make-wrapper3.c is deliberately absent of this list
### Epilogue. Do not modify this block. #######################################
-include $(shell $(FRAMAC) -no-autoload-plugins -print-share-path)/analysis-scripts/epilogue.mk
+include $(shell $(FRAMAC) -no-autoload-plugins -print-lib-path)/analysis-scripts/epilogue.mk
###############################################################################
diff --git a/tests/fc_script/oracle/GNUmakefile b/tests/fc_script/oracle/GNUmakefile
index 26fc8e8f569..5cda2a5d946 100644
--- a/tests/fc_script/oracle/GNUmakefile
+++ b/tests/fc_script/oracle/GNUmakefile
@@ -7,10 +7,10 @@
# an optional include, unnecessary if frama-c is in the PATH.
FRAMAC ?= frama-c # FRAMAC is defined in path.mk when it is included, but the
# user can override it in the command-line.
-ifeq ($(FRAMAC_SHARE),)
- FRAMAC_SHARE := $(shell $(FRAMAC)-config -print-share-path)
+ifeq ($(FRAMAC_LIB),)
+ FRAMAC_LIB := $(shell $(FRAMAC)-config -print-lib-path)
endif
-include $(FRAMAC_SHARE)/analysis-scripts/prologue.mk
+include $(FRAMAC_LIB)/analysis-scripts/prologue.mk
###############################################################################
# Edit below as needed. Suggested flags are optional.
@@ -51,5 +51,5 @@ fc_script_main.parse: \
./main3.c \
### Epilogue. Do not modify this block. #######################################
-include $(FRAMAC_SHARE)/analysis-scripts/epilogue.mk
+include $(FRAMAC_LIB)/analysis-scripts/epilogue.mk
###############################################################################
--
GitLab