[analysis-scripts] fix issues in make-template and remove obsolete make-path

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 "$@";

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

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

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,

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...