diff --git a/bin/frama-c-script b/bin/frama-c-script
index f4ba2342d0e2907002113f7497041df36fb4d69b..8ff07f4647a65df4d4b3da0193357f9bdc06a09c 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 2f17e71e214d6280bd58470e878618d7db6c4d89..459e17d0d4ef48f152bd9f82ff72ca7bc046e258 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 1ec1be6c901fd44c3129614bbebfb3c12adfd42e..10d19b2ff648074e0762ab8e8635fb370e4d9c37 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 fb4f76ada7731db4664f3846ab670f0173ca86ac..ed72df096223334ce385db07fc050376f49d21b6 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 fb1240c15cd993966a33449fdccbfa7ab72d65ba..1c380ce5ac17a9c2ffd878e305eb82a5d28d0fb0 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...