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..33819b87e89f0f0b109c67d441dc2ce4c94faf75 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,18 +72,16 @@ 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" -process = Popen([frama_c_config, "-share"], stdout=PIPE) +process = Popen([framac_bin / "frama-c", "-no-autoload-plugins", "-print-share-path"], stdout=PIPE) (output, err) = process.communicate() output = output.decode('utf-8') exit_code = process.wait() if exit_code != 0: - sys.exit("error running frama-c-config") + sys.exit(f"error running frama-c -print-share-path") 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() @@ -97,22 +95,22 @@ def get_known_machdeps(): return (default_machdep, machdeps) def check_path_exists(path): - if os.path.exists(path): + if path.exists(): yn = input(f"warning: {path} already exists. Overwrite? [y/N] ") if yn == "" or not (yn[0] == "Y" or yn[0] == "y"): print("Exiting without overwriting.") sys.exit(0) - pathdir = os.path.dirname(path) - if not os.path.exists(pathdir): + pathdir = path.parent + if not pathdir.exists(): yn = input(f"warning: directory '{pathdir}' does not exit. Create it? [y/N] ") if yn == "" or not (yn[0] == "Y" or yn[0] == "y"): print("Exiting without creating.") sys.exit(0) - Path(pathdir).mkdir(parents=True, exist_ok=False) + pathdir.mkdir(parents=True, exist_ok=False) check_path_exists(gnumakefile) main = input("Main target name: ") -if not re.match("^[a-zA-Z_0-9]+$", main): +if not re.match("^[a-zA-Z_0-9-]+$", main): sys.exit("error: invalid main target name (can only contain letters, digits, dash or underscore)") main_fun_finder_re = function_finder.prepare("main") @@ -250,9 +248,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: