diff --git a/Makefile b/Makefile
index 4df5cf329a46333da072ec0bcfb9db04d8e5ffe6..c8eee3952170faf9f3cc72f2852c29860fbfc60e 100644
--- a/Makefile
+++ b/Makefile
@@ -264,6 +264,7 @@ DISTRIB_FILES:=\
share/analysis-scripts/frama_c_results.py \
share/analysis-scripts/git_utils.py \
share/analysis-scripts/list_files.py \
+ share/analysis-scripts/make_template.py \
share/analysis-scripts/make_wrapper.py \
share/analysis-scripts/parse-coverage.sh \
share/analysis-scripts/README.md \
diff --git a/bin/frama-c-script b/bin/frama-c-script
index 17c2872620774db6c5d46115422e0ecc2b12542f..3543aaee31f3e85e2215b71ac50e13946c444888 100755
--- a/bin/frama-c-script
+++ b/bin/frama-c-script
@@ -120,62 +120,6 @@ open_file() {
esac
}
-make_template() {
- if [ "$#" -gt 0 ]; then
- dir="${1%/}"
- else
- dir="."
- fi
- path="$dir/GNUmakefile"
- path_tmp="${path}.tmp"
- check_path_exists "$path"
- read -p "Main target name: " main
- if [[ ! ( "$main" =~ ^[a-zA-Z_0-9]+$ ) ]]; then
- echo "error: invalid main target name";
- exit 1
- fi
- read -p "Source files separated by spaces (default if empty: *.c): " sources
- if [ "$sources" = "" ]; then
- sources="*.c"
- fi
-
- add_main_stub=0
- read -p "Add stub for function main (only needed if it uses command-line arguments)? [y/N] " yn
- case $yn in
- [Yy])
- add_main_stub=1
- sources="fc_stubs.c $sources"
- ;;
- *)
- ;;
- esac
-
- sed "s/^MAIN_TARGET :=/MAIN_TARGET := ${main}/" "${FRAMAC_SHARE}/analysis-scripts/template.mk" > "$path"
- sed "s|\$(MAIN_TARGET).parse:|\$(MAIN_TARGET).parse: $sources|" "$path" | sed "/# Remove these lines after defining the main target/{N;N;N;N;d;}" > "$path_tmp"; mv "$path_tmp" "$path"
- if [ -e "compile_commands.json" ]; then
- read -p "compile_commands.json exists, add option -json-compilation-database? [Y/n] " yn
- case $yn in
- [Nn])
- echo "Option not added; you can later add it to FCFLAGS."
- ;;
- *)
- # the command below inserts a line after matching a given
- # pattern; compatible with macOS sed
- sed -e '/^FCFLAGS[[:space:]]\++=/a\
-\ \ -json-compilation-database .\\' "$path" > "$path_tmp"; mv "$path_tmp" "$path"
- ;;
- esac
- fi
- if [ $add_main_stub -eq 1 ]; then
- check_path_exists "fc_stubs.c"
- cp "${FRAMAC_SHARE}/analysis-scripts/fc_stubs.c" "./"
- echo "Created stub for main function: fc_stubs.c"
- sed -e '/^FCFLAGS[[:space:]]\++=/a\
-\ \ -main eva_main \\' "$path" > "$path_tmp"; mv "$path_tmp" "$path"
- fi
- echo "Template created: $path"
-}
-
make_path() {
cat <<EOF > frama-c-path.mk
FRAMAC_DIR=${DIR}
@@ -288,7 +232,7 @@ case "$command" in
;;
"make-template")
shift;
- make_template "$@";
+ ${FRAMAC_SHARE}/analysis-scripts/make_template.py "$0" "$@";
;;
"make-path")
shift;
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 166fbddd62c2cbc23bcf5798fb293433cbd20083..e54f95810601d05af5828bf7ea15f183ce797813 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -130,6 +130,7 @@ share/analysis-scripts/find_fun.py: .ignore
share/analysis-scripts/flamegraph.pl: CDDL
share/analysis-scripts/git_utils.py: .ignore
share/analysis-scripts/list_files.py: .ignore
+share/analysis-scripts/make_template.py: .ignore
share/analysis-scripts/make_wrapper.py: .ignore
share/analysis-scripts/parse-coverage.sh: .ignore
share/analysis-scripts/README.md: .ignore
diff --git a/share/analysis-scripts/make_template.py b/share/analysis-scripts/make_template.py
new file mode 100755
index 0000000000000000000000000000000000000000..ca241cc8f0ebf660365c6369a52385506d19bd24
--- /dev/null
+++ b/share/analysis-scripts/make_template.py
@@ -0,0 +1,191 @@
+#!/usr/bin/env python3
+#-*- coding: utf-8 -*-
+##########################################################################
+# #
+# This file is part of Frama-C. #
+# #
+# Copyright (C) 2007-2018 #
+# CEA (Commissariat à l'énergie atomique et aux énergies #
+# alternatives) #
+# #
+# you can redistribute it and/or modify it under the terms of the GNU #
+# Lesser General Public License as published by the Free Software #
+# Foundation, version 2.1. #
+# #
+# It is distributed in the hope that it will be useful, #
+# but WITHOUT ANY WARRANTY; without even the implied warranty of #
+# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
+# GNU Lesser General Public License for more details. #
+# #
+# See the GNU Lesser General Public License version 2.1 #
+# for more details (enclosed in the file licenses/LGPLv2.1). #
+# #
+##########################################################################
+
+# This script is used to interactively fill template.mk, converting it
+# into a GNUmakefile ready for analysis.
+
+import sys
+import os
+import re
+from subprocess import Popen, PIPE
+from pathlib import Path
+
+MIN_PYTHON = (3, 5) # for glob(recursive)
+if sys.version_info < MIN_PYTHON:
+ sys.exit("Python %s.%s or later is required.\n" % MIN_PYTHON)
+
+if len(sys.argv) > 3:
+ print("usage: %s path-to-frama-c-script [dir]" % sys.argv[0])
+ print(" creates a GNUmakefile for running Frama-C on a set of files,")
+ print(" interactively filling a template.")
+ sys.exit(1)
+
+if not os.path.isfile(sys.argv[1]):
+ print("error: path to frama-c-script is not a file: " + sys.argv[1])
+ sys.exit(1)
+
+jcdb = Path("compile_commands.json")
+
+if "PTESTS_TESTING" in os.environ:
+ print("Running ptests: setting up mock files...")
+ jcdb.touch()
+
+bindir = Path(os.path.dirname(os.path.abspath(sys.argv[1])))
+frama_c_config = bindir / "frama-c-config"
+process = Popen([frama_c_config, "-print-share-path"], stdout=PIPE)
+(output, err) = process.communicate()
+output = output.decode('utf-8')
+exit_code = process.wait()
+if exit_code != 0:
+ print("error running frama-c-config")
+ sys.exit(1)
+sharedir = Path(output)
+
+def get_known_machdeps():
+ process = Popen([bindir / "frama-c", "-machdep", "help"], stdout=PIPE)
+ (output, err) = process.communicate()
+ output = output.decode('utf-8')
+ exit_code = process.wait()
+ if exit_code != 0:
+ print("error getting machdeps: " + output)
+ sys.exit(1)
+ match = re.match("\[kernel\] supported machines are (.*) \(default is (.*)\).", output, re.DOTALL)
+ if not match:
+ print("error getting known machdeps: " + output)
+ sys.exit()
+ machdeps = match.group(1).split()
+ default_machdep = match.group(2)
+ return (default_machdep, machdeps)
+
+dir = Path(sys.argv[2] if len(sys.argv) == 3 else ".")
+gnumakefile = dir / "GNUmakefile"
+
+def check_path_exists(path):
+ if os.path.exists(path):
+ yn = input("warning: {} already exists. Overwrite? [y/N] ".format(path))
+ if yn == "" or not (yn[0] == "Y" or yn[0] == "y"):
+ print("Exiting without overwriting.")
+ sys.exit(0)
+
+check_path_exists(gnumakefile)
+main = input("Main target name: ")
+if not re.match("^[a-zA-Z_0-9]+$", main):
+ print("error: invalid main target name")
+ sys.exit(1)
+
+sources = input("Source files separated by spaces (default if empty: *.c): ")
+if not sources:
+ sources="*.c"
+
+json_compilation_database = None
+if jcdb.is_file():
+ yn = input("compile_commands.json exists, add option -json-compilation-database? [Y/n] ")
+ if yn == "" or not (yn[0] == "N" or yn[0] == "n"):
+ json_compilation_database = "."
+ else:
+ print("Option not added; you can later add it to FCFLAGS.")
+
+add_main_stub = False
+yn = input("Add stub for function main (only needed if it uses command-line arguments)? [y/N] ")
+if yn != "" and (yn[0] == "Y" or yn[0] == "y"):
+ add_main_stub = True
+ sources = "fc_stubs.c " + sources
+
+print("Please define the architectural model (machdep) of the target machine.")
+(default_machdep, machdeps) = get_known_machdeps()
+print("Known machdeps: " + " ".join(machdeps))
+machdep_chosen = False
+while not machdep_chosen:
+ machdep = input("Please enter the machdep [" + default_machdep + "]: ")
+ if not machdep:
+ machdep = default_machdep
+ machdep_chosen = True
+ else:
+ if not (machdep in machdeps):
+ yn = input("'{}' is not a standard machdep. Proceed anyway? [y/N]".format(machdep))
+ if yn != "" and (yn[0] == "Y" or yn[0] == "y"):
+ machdep_chosen = True
+ else:
+ machdep_chosen = True
+
+def insert_line_after(lines, line_pattern, newline):
+ re_line = re.compile(line_pattern)
+ for i in range(0, len(lines)):
+ if re_line.search(lines[i]):
+ lines.insert(i+1, newline)
+ return lines
+ print("error: no lines found matching pattern: " + line_pattern)
+ sys.exit(1)
+
+def replace_line(lines, line_pattern, value):
+ re_line = re.compile(line_pattern)
+ for i in range(0, len(lines)):
+ if re_line.search(lines[i]):
+ lines[i] = value
+ return lines
+ print("error: no lines found matching pattern: " + line_pattern)
+ sys.exit(1)
+
+def remove_lines_between(lines, start_pattern, end_pattern):
+ re_start = re.compile(start_pattern)
+ re_end = re.compile(end_pattern)
+ first_to_remove = -1
+ last_to_remove = -1
+ for i in range(0, len(lines)):
+ if first_to_remove == -1 and re_start.search(lines[i]):
+ first_to_remove = i
+ elif re_end.search(lines[i]):
+ last_to_remove = i
+ break
+ if first_to_remove == -1:
+ print("error: could not find start pattern: " + start_pattern)
+ sys.exit(1)
+ elif last_to_remove == -1:
+ print("error: could not find end pattern: " + end_pattern)
+ sys.exit(1)
+ return (lines[:first_to_remove-1] if first_to_remove > 0 else []) + (lines[last_to_remove+1:] if last_to_remove < len(lines)-1 else [])
+
+with open(sharedir / "analysis-scripts" / "template.mk") as f:
+ lines = list(f)
+ lines = replace_line(lines, "^MAIN_TARGET :=", "MAIN_TARGET := {}\n".format(main))
+ lines = remove_lines_between(lines, "Remove these lines.*main target", "^endif")
+ lines = replace_line(lines, "^\$\(MAIN_TARGET\).parse:", "$(MAIN_TARGET).parse: {}\n".format(sources))
+ if json_compilation_database:
+ lines = insert_line_after(lines, "^FCFLAGS", " -json-compilation-database {} \\\n".format(json_compilation_database))
+ lines = insert_line_after(lines, "^FCFLAGS", " -machdep {} \\\n".format(machdep))
+ if add_main_stub:
+ check_path_exists("fc_stubs.c")
+ from shutil import copyfile
+ copyfile(sharedir / "analysis-scripts" / "fc_stubs.c", "fc_stubs.c")
+ print("Created stub for main function: fc_stubs.c")
+
+gnumakefile.write_text("".join(lines))
+
+print("Template created: " + gnumakefile.name)
+
+if "PTESTS_TESTING" in os.environ:
+ print("Running ptests: cleaning up after tests...")
+ jcdb.unlink()
+ if add_main_stub:
+ Path("fc_stubs.c").unlink()
diff --git a/tests/fc_script/main.c b/tests/fc_script/main.c
index 176bf1c3e843ae5c5e9967c7c2607ec6006562d3..74d57214aa95bddef791ede03759c1a863e371da 100644
--- a/tests/fc_script/main.c
+++ b/tests/fc_script/main.c
@@ -1,6 +1,6 @@
/* run.config
OPT:
- EXECNOW: LOG GNUmakefile LOG make_template.res LOG make_template.err bin/frama-c-script make-template @PTEST_DIR@/result < @PTEST_DIR@/make_template.input > @PTEST_DIR@/result/make_template.res 2> @PTEST_DIR@/result/make_template.err
+ EXECNOW: LOG GNUmakefile LOG make_template.res LOG make_template.err PTESTS_TESTING= bin/frama-c-script make-template @PTEST_DIR@/result < @PTEST_DIR@/make_template.input > @PTEST_DIR@/result/make_template.res 2> @PTEST_DIR@/result/make_template.err
EXECNOW: LOG list_files.res LOG list_files.err bin/frama-c-script list-files @PTEST_DIR@/list_files.json > @PTEST_DIR@/result/list_files.res 2> @PTEST_DIR@/result/list_files.err
EXECNOW: LOG flamegraph.html LOG flamegraph.res LOG flamegraph.err NOGUI=1 bin/frama-c-script flamegraph @PTEST_DIR@/flamegraph.txt @PTEST_DIR@/result > @PTEST_DIR@/result/flamegraph.res 2> @PTEST_DIR@/result/flamegraph.err && rm -f @PTEST_DIR@/result/flamegraph.svg
EXECNOW: LOG find_fun1.res LOG find_fun1.err bin/frama-c-script find-fun main2 @PTEST_DIR@ > @PTEST_DIR@/result/find_fun1.res 2> @PTEST_DIR@/result/find_fun1.err
diff --git a/tests/fc_script/make_template.input b/tests/fc_script/make_template.input
index 7d303e9f0445bd48f79321001776a02c34d473d3..62488cfcb339f48b9263e611e5e7422074143ddb 100644
--- a/tests/fc_script/make_template.input
+++ b/tests/fc_script/make_template.input
@@ -1,2 +1,7 @@
fc_script_main
file1.c file*.c dir/more_files.c
+y
+y
+invalid_machdep
+n
+x86_64
diff --git a/tests/fc_script/oracle/GNUmakefile b/tests/fc_script/oracle/GNUmakefile
index 12cd496ed85d9e8a6db443df0b585e81836f2339..32e5f33f164497fed2b82f1f27117a01a2286360 100644
--- a/tests/fc_script/oracle/GNUmakefile
+++ b/tests/fc_script/oracle/GNUmakefile
@@ -29,6 +29,8 @@ CPPFLAGS +=
# (Optional) Frama-C general flags (parsing and kernel)
FCFLAGS += \
+ -machdep x86_64 \
+ -json-compilation-database . \
-kernel-warn-key annot:missing-spec=abort \
-kernel-warn-key typing:implicit-function-declaration=abort \
@@ -48,7 +50,7 @@ all: $(TARGETS)
# (MANDATORY) List of source files used by MAIN_TARGET.
# If there is a JSON compilation database,
# 'frama-c-script list-files' can help obtain it
-$(MAIN_TARGET).parse: file1.c file*.c dir/more_files.c
+$(MAIN_TARGET).parse: fc_stubs.c file1.c file*.c dir/more_files.c
# The following targets are optional and provided for convenience only
diff --git a/tests/fc_script/oracle/make_template.res b/tests/fc_script/oracle/make_template.res
index 280e7bb79e5a815f6d82b1eabec5b59fae3bb21f..9f38d9c7e745cbea6fe458c9fc77cdcd03f48e1e 100644
--- a/tests/fc_script/oracle/make_template.res
+++ b/tests/fc_script/oracle/make_template.res
@@ -1 +1,6 @@
-Template created: tests/fc_script/result/GNUmakefile
+Running ptests: setting up mock files...
+Main target name: Source files separated by spaces (default if empty: *.c): compile_commands.json exists, add option -json-compilation-database? [Y/n] Add stub for function main (only needed if it uses command-line arguments)? [y/N] Please define the architectural model (machdep) of the target machine.
+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]: Created stub for main function: fc_stubs.c
+Template created: GNUmakefile
+Running ptests: cleaning up after tests...