diff --git a/bin/frama-c-script b/bin/frama-c-script index 06e66c5715598ada693958393c75302936577c67..2ea801b4290a6451a3b929a07b60ae5a6b77df79 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 05a4b6b60d39eb91a24d6043e0bd7db42fde673a..34b188eef76a7a1908974f234973c56ec080d1fc 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 acebea6b4983d92807c188bcd83d32ef624b4e98..84cf0d2f2e8af2bad38c92a0b21c20c3fdc1681e 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 d93bd3ec9fc08a9192b21dde2b48faace922ecae..f392d8a1913cfc57e2bc4e02b2df66945598f5e4 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 3dab5bcfe519a42f1b9b0745ba4bb409bded6d3f..d093ceea76f60988c6688684432ef24b33012e99 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 54cdd1332ac9cc37c6ceaae223ad16f217af1d79..650a01dd63cea699fbcd402e3980b9ad18b52b32 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 0cd0930e72caad60bd7c45afb750deac58141e1b..8e1aa8af9f9beb6718852fb8504fa6633b1ba99c 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 fb0da4b9b937d09ce4fa8aac3de912354e5851ab..5c3d8c60694a70c9af58d802235e9121759334e8 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 983f2a16d9f1be8dcaaaa332626afa7c6c54ffee..5cac4969ff81cf3cbc03f8a4bdab0c78178237ee 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 26fc8e8f569ab3fdbb3114a76c0f69466b8b8e2f..5cda2a5d946cf8a1b69fb364326b047eac15a460 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 ###############################################################################