Skip to content
Snippets Groups Projects
Commit b8516599 authored by Valentin Perrelle's avatar Valentin Perrelle
Browse files

Merge branch 'fix/andre/fc-script-simplify-make-template' into 'master'

[analysis-scripts] simplify make-template using FRAMAC_BIN

See merge request frama-c/frama-c!2870
parents 699cfed4 39fa0fcd
No related branches found
No related tags found
No related merge requests found
...@@ -217,7 +217,6 @@ case "$command" in ...@@ -217,7 +217,6 @@ case "$command" in
;; ;;
"make-template") "make-template")
shift; shift;
export FRAMAC="${DIR}/frama-c"
${FRAMAC_SHARE}/analysis-scripts/make_template.py "$@"; ${FRAMAC_SHARE}/analysis-scripts/make_template.py "$@";
;; ;;
"make-path") "make-path")
......
...@@ -44,15 +44,15 @@ if len(sys.argv) > 2: ...@@ -44,15 +44,15 @@ if len(sys.argv) > 2:
print(" creates a Frama-C makefile in [dir] (default: .frama-c)") print(" creates a Frama-C makefile in [dir] (default: .frama-c)")
sys.exit(1) sys.exit(1)
framac_in_path = False # Note: if Frama-C is in the path, ignore the one in FRAMAC_BIN
if os.environ.get("FRAMAC"): framac = shutil.which("frama-c")
framac = os.environ["FRAMAC"] if framac:
if not framac or not os.path.isfile(framac): framac_bin = Path(os.path.dirname(os.path.abspath(framac)))
framac_in_path = True else:
framac = shutil.which("frama-c") framac_bin = os.getenv('FRAMAC_BIN')
if not framac: if not framac_bin:
sys.exit("error: frama-c must be in the PATH, "\ sys.exit("error: FRAMAC_BIN not in environment")
"or in environment variable FRAMAC") framac_bin = Path(framac_bin)
jcdb = Path("compile_commands.json") jcdb = Path("compile_commands.json")
...@@ -72,18 +72,16 @@ if "PTESTS_TESTING" in os.environ: ...@@ -72,18 +72,16 @@ if "PTESTS_TESTING" in os.environ:
fc_stubs_c.touch() fc_stubs_c.touch()
gnumakefile.touch() gnumakefile.touch()
bindir = Path(os.path.dirname(os.path.abspath(framac))) process = Popen([framac_bin / "frama-c", "-no-autoload-plugins", "-print-share-path"], stdout=PIPE)
frama_c_config = bindir / "frama-c-config"
process = Popen([frama_c_config, "-share"], stdout=PIPE)
(output, err) = process.communicate() (output, err) = process.communicate()
output = output.decode('utf-8') output = output.decode('utf-8')
exit_code = process.wait() exit_code = process.wait()
if exit_code != 0: if exit_code != 0:
sys.exit("error running frama-c-config") sys.exit(f"error running frama-c -print-share-path")
sharedir = Path(output) sharedir = Path(output)
def get_known_machdeps(): 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, err) = process.communicate()
output = output.decode('utf-8') output = output.decode('utf-8')
exit_code = process.wait() exit_code = process.wait()
...@@ -97,22 +95,22 @@ def get_known_machdeps(): ...@@ -97,22 +95,22 @@ def get_known_machdeps():
return (default_machdep, machdeps) return (default_machdep, machdeps)
def check_path_exists(path): def check_path_exists(path):
if os.path.exists(path): if path.exists():
yn = input(f"warning: {path} already exists. Overwrite? [y/N] ") yn = input(f"warning: {path} already exists. Overwrite? [y/N] ")
if yn == "" or not (yn[0] == "Y" or yn[0] == "y"): if yn == "" or not (yn[0] == "Y" or yn[0] == "y"):
print("Exiting without overwriting.") print("Exiting without overwriting.")
sys.exit(0) sys.exit(0)
pathdir = os.path.dirname(path) pathdir = path.parent
if not os.path.exists(pathdir): if not pathdir.exists():
yn = input(f"warning: directory '{pathdir}' does not exit. Create it? [y/N] ") yn = input(f"warning: directory '{pathdir}' does not exit. Create it? [y/N] ")
if yn == "" or not (yn[0] == "Y" or yn[0] == "y"): if yn == "" or not (yn[0] == "Y" or yn[0] == "y"):
print("Exiting without creating.") print("Exiting without creating.")
sys.exit(0) sys.exit(0)
Path(pathdir).mkdir(parents=True, exist_ok=False) pathdir.mkdir(parents=True, exist_ok=False)
check_path_exists(gnumakefile) check_path_exists(gnumakefile)
main = input("Main target name: ") 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)") sys.exit("error: invalid main target name (can only contain letters, digits, dash or underscore)")
main_fun_finder_re = function_finder.prepare("main") main_fun_finder_re = function_finder.prepare("main")
...@@ -250,9 +248,9 @@ gnumakefile.write_text("".join(lines)) ...@@ -250,9 +248,9 @@ gnumakefile.write_text("".join(lines))
print(f"Template created: {gnumakefile}") 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}") 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}") os.system(f"{frama_c_script} make-path {dir}")
if "PTESTS_TESTING" in os.environ: if "PTESTS_TESTING" in os.environ:
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment