From 913fb8086c37fc217c8cd43ccce8abce23be7965 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Mon, 26 Oct 2020 21:35:12 +0100
Subject: [PATCH] [analysis-scripts] fix issues in make-template and remove
obsolete make-path
---
bin/frama-c-script | 36 ------------------------
doc/userman/user-analysis-scripts.tex | 3 --
share/analysis-scripts/make_template.py | 34 +++++++++++++---------
share/analysis-scripts/make_wrapper.py | 2 +-
tests/fc_script/oracle/make_template.res | 1 +
5 files changed, 22 insertions(+), 54 deletions(-)
diff --git a/bin/frama-c-script b/bin/frama-c-script
index f4ba2342d0e..8ff07f4647a 100755
--- a/bin/frama-c-script
+++ b/bin/frama-c-script
@@ -38,10 +38,6 @@ usage() {
echo " Interactively prepares a template for analyses,"
echo " writing it to dir/GNUmakefile [default: .frama-c]."
echo ""
- echo " - make-path [dir]"
- echo " [for Frama-C developers and advanced users without Frama-C in the path]"
- echo " Creates a path.mk file in dir [default: .frama-c]."
- echo ""
echo " - list-files [path/to/compile_commands.json]"
echo " Lists all sources in the given compile_commands.json"
echo " [default: ./compile_commands.json]."
@@ -123,34 +119,6 @@ open_file() {
esac
}
-make_path() {
- dir=".frama-c"
- if [ "$#" -gt 0 ]; then
- dir="$1"
- fi
- if [ ! -d "$dir" ]; then
- read -p "Directory '$dir' does not exist. Create it? [y/N] " yn
- case $yn in
- [Yy])
- mkdir -p "$dir"
- ;;
- *)
- echo "Exiting without creating."
- exit 0;;
- esac
- fi
- cat <<EOF > "${dir}/path.mk"
-FRAMAC_BIN=${DIR}
-ifeq (\$(wildcard \$(FRAMAC_BIN)),)
-# Frama-C not installed locally; using the version in the PATH
-else
-FRAMAC=\$(FRAMAC_BIN)/frama-c
-FRAMAC_GUI=\$(FRAMAC_BIN)/frama-c-gui
-endif
-EOF
- echo "Wrote to: ${dir}/path.mk"
-}
-
flamegraph() {
if [ "$#" -eq 0 ]; then
echo "error: 'flamegraph' command requires a path";
@@ -219,10 +187,6 @@ case "$command" in
shift;
${FRAMAC_SHARE}/analysis-scripts/make_template.py "$@";
;;
- "make-path")
- shift;
- make_path "$@";
- ;;
"list-files")
shift;
${FRAMAC_SHARE}/analysis-scripts/list_files.py "$@";
diff --git a/doc/userman/user-analysis-scripts.tex b/doc/userman/user-analysis-scripts.tex
index 2f17e71e214..459e17d0d4e 100644
--- a/doc/userman/user-analysis-scripts.tex
+++ b/doc/userman/user-analysis-scripts.tex
@@ -409,9 +409,6 @@ Other commands, only useful in a few cases, are described below.
system, removing optional code features that could prevent \FramaC from
parsing the sources. Currently, it still depends partially on the host system,
so many features are not disabled.
-\item[make-path] (for \FramaC developers): to be used when Frama-C is not
- installed in the PATH; adds a \texttt{path.mk} file that is used
- by the Makefile generated via \texttt{make-template}.
\item[flamegraph]: opens a {\em flamegraph}\footnote{%
See \url{https://github.com/brendangregg/FlameGraph} for details about
flamegraphs.} to visualize which functions take most of the time
diff --git a/share/analysis-scripts/make_template.py b/share/analysis-scripts/make_template.py
index 1ec1be6c901..10d19b2ff64 100755
--- a/share/analysis-scripts/make_template.py
+++ b/share/analysis-scripts/make_template.py
@@ -45,15 +45,10 @@ if len(sys.argv) > 2:
print(" creates a Frama-C makefile in [dir] (default: .frama-c)")
sys.exit(1)
-# Note: if Frama-C is in the path, ignore the one in FRAMAC_BIN
-framac = shutil.which("frama-c")
-if framac:
- framac_bin = Path(os.path.dirname(os.path.abspath(framac)))
-else:
- framac_bin = os.getenv('FRAMAC_BIN')
- if not framac_bin:
- sys.exit("error: FRAMAC_BIN not in environment")
- framac_bin = Path(framac_bin)
+framac_bin = os.getenv('FRAMAC_BIN')
+if not framac_bin:
+ sys.exit("error: FRAMAC_BIN not in environment (set by frama-c-script)")
+framac_bin = Path(framac_bin)
jcdb = Path("compile_commands.json")
@@ -77,7 +72,7 @@ process = Popen([framac_bin / "frama-c", "-print-config-json"], stdout=PIPE)
(output, err) = process.communicate()
exit_code = process.wait()
if exit_code != 0:
- sys.exit(f"error running frama-c -print-share-path")
+ sys.exit(f"error running frama-c -print-config-json")
fc_config = json.loads(output.decode('utf-8'))
sharedir = Path(fc_config['datadir'])
@@ -237,13 +232,24 @@ gnumakefile.write_text("".join(lines))
print(f"Template created: {gnumakefile}")
-if not "PTESTS_TESTING" in os.environ and not framac:
- print(f"Frama-C not in path, adding path.mk to {dir}")
- frama_c_script = framac_bin / "frama-c-script"
- os.system(f"{frama_c_script} make-path {dir}")
+# write path.mk
+path_mk = dir / "path.mk"
+
+with open(path_mk, "w") as f:
+ f.write(f"""FRAMAC_BIN={framac_bin}
+ifeq ($(wildcard $(FRAMAC_BIN)),)
+# Frama-C not installed locally; using the version in the PATH
+else
+FRAMAC=$(FRAMAC_BIN)/frama-c
+FRAMAC_GUI=$(FRAMAC_BIN)/frama-c-gui
+endif
+""")
+
+print(f"Path to Frama-C binaries written to: {path_mk}")
if "PTESTS_TESTING" in os.environ:
print("Running ptests: cleaning up after tests...")
jcdb.unlink()
fc_stubs_c.unlink()
+ path_mk.unlink()
# gnumakefile is not erased because we want it as an oracle
diff --git a/share/analysis-scripts/make_wrapper.py b/share/analysis-scripts/make_wrapper.py
index fb4f76ada77..ed72df09622 100755
--- a/share/analysis-scripts/make_wrapper.py
+++ b/share/analysis-scripts/make_wrapper.py
@@ -49,7 +49,7 @@ args = args[1:]
framac_bin = os.getenv('FRAMAC_BIN')
if not framac_bin:
- sys.exit("error: FRAMAC_BIN not in environment")
+ sys.exit("error: FRAMAC_BIN not in environment (set by frama-c-script)")
framac_script = f"{framac_bin}/frama-c-script"
out = subprocess.Popen(['make', "-C", make_dir] + args,
diff --git a/tests/fc_script/oracle/make_template.res b/tests/fc_script/oracle/make_template.res
index fb1240c15cd..1c380ce5ac1 100644
--- a/tests/fc_script/oracle/make_template.res
+++ b/tests/fc_script/oracle/make_template.res
@@ -12,4 +12,5 @@ Is this ok? [Y/n] compile_commands.json exists, add option -json-compilation-dat
Known machdeps: x86_16 x86_32 x86_64 gcc_x86_16 gcc_x86_32 gcc_x86_64 ppc_32 msvc_x86_64
Please enter the machdep [x86_32]: 'invalid_machdep' is not a standard machdep. Proceed anyway? [y/N]Please enter the machdep [x86_32]: warning: fc_stubs.c already exists. Overwrite? [y/N] Created stub for main function: fc_stubs.c
Template created: GNUmakefile
+Path to Frama-C binaries written to: path.mk
Running ptests: cleaning up after tests...
--
GitLab