diff --git a/bin/frama-c-script b/bin/frama-c-script index 7b137a3d4f849a7c4b41c0a68036bf7645651d04..2c0b0dec11588ad3285c314393a0941c36220165 100755 --- a/bin/frama-c-script +++ b/bin/frama-c-script @@ -217,7 +217,6 @@ case "$command" in ;; "make-template") shift; - export FRAMAC="${DIR}/frama-c" ${FRAMAC_SHARE}/analysis-scripts/make_template.py "$@"; ;; "make-path") diff --git a/share/analysis-scripts/make_template.py b/share/analysis-scripts/make_template.py index 6cbab8c30caf80289ff47531e00502af661bbbab..d00f9d9881be2fc73d8dc54126569c80b5d0b012 100755 --- a/share/analysis-scripts/make_template.py +++ b/share/analysis-scripts/make_template.py @@ -44,15 +44,15 @@ if len(sys.argv) > 2: print(" creates a Frama-C makefile in [dir] (default: .frama-c)") sys.exit(1) -framac_in_path = False -if os.environ.get("FRAMAC"): - framac = os.environ["FRAMAC"] -if not framac or not os.path.isfile(framac): - framac_in_path = True - framac = shutil.which("frama-c") - if not framac: - sys.exit("error: frama-c must be in the PATH, "\ - "or in environment variable FRAMAC") +# 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) jcdb = Path("compile_commands.json") @@ -72,8 +72,7 @@ if "PTESTS_TESTING" in os.environ: fc_stubs_c.touch() gnumakefile.touch() -bindir = Path(os.path.dirname(os.path.abspath(framac))) -frama_c_config = bindir / "frama-c-config" +frama_c_config = framac_bin / "frama-c-config" process = Popen([frama_c_config, "-share"], stdout=PIPE) (output, err) = process.communicate() output = output.decode('utf-8') @@ -83,7 +82,7 @@ if exit_code != 0: sharedir = Path(output) def get_known_machdeps(): - process = Popen([bindir / "frama-c", "-machdep", "help"], stdout=PIPE) + process = Popen([framac_bin / "frama-c", "-machdep", "help"], stdout=PIPE) (output, err) = process.communicate() output = output.decode('utf-8') exit_code = process.wait() @@ -250,9 +249,9 @@ gnumakefile.write_text("".join(lines)) print(f"Template created: {gnumakefile}") -if not "PTESTS_TESTING" in os.environ and not framac_in_path: +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 = bindir / "frama-c-script" + frama_c_script = framac_bin / "frama-c-script" os.system(f"{frama_c_script} make-path {dir}") if "PTESTS_TESTING" in os.environ: