diff --git a/Makefile b/Makefile
index 4571affc6f865f7c8b251b54fd4f124fbd236454..94bfa0d32a6bfae0a19ef60c26a31fd1aa5e866b 100644
--- a/Makefile
+++ b/Makefile
@@ -262,6 +262,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_wrapper.py \
share/analysis-scripts/parse-coverage.sh \
share/analysis-scripts/README.md \
share/analysis-scripts/results_display.py \
@@ -1915,6 +1916,7 @@ install:: install-lib
share/analysis-scripts/frama_c_results.py \
share/analysis-scripts/git_utils.py \
share/analysis-scripts/list_files.py \
+ share/analysis-scripts/make_wrapper.py \
share/analysis-scripts/parse-coverage.sh \
share/analysis-scripts/README.md \
share/analysis-scripts/results_display.py \
diff --git a/bin/frama-c-script b/bin/frama-c-script
index e5662b42c117dddbb7b26fb64e871bd95236cf63..e3dafca01d88506b4c9402155b7c5b0f84f1b29e 100755
--- a/bin/frama-c-script
+++ b/bin/frama-c-script
@@ -66,6 +66,14 @@ if [ $# -lt 1 ]; then
echo " and non-POSIX external libraries."
echo " <machdep> is necessary to define a required preprocessor symbol"
echo " (run 'frama-c -machdep' help to get the list of machdeps)."
+ echo ""
+ echo " - make-wrapper <target> <args>"
+ echo " Runs 'make <target> <args>', parsing the output to suggest"
+ echo " useful commands in case of failure."
+ echo ""
+ echo " - normalize-jcdb [path/to/compile_commands.json]"
+ echo " Applies some transformations to an existing compile_commands.json"
+ echo " (such as relativizing paths) to improve portability"
exit
fi
@@ -112,6 +120,7 @@ make_template() {
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
@@ -122,9 +131,41 @@ make_template() {
if [ "$sources" = "" ]; then
sources="*.c"
fi
- sed "s/^MAIN_TARGET :=/MAIN_TARGET := ${main}/" "${FRAMAC_SHARE}/analysis-scripts/template.mk" > "${path}.tmp"
- sed "s|\$(MAIN_TARGET).parse:|\$(MAIN_TARGET).parse: $sources|" "${path}.tmp" | sed "/# Remove these lines after defining the main target/{N;N;N;N;d;}" > "$path"
- rm "${path}.tmp"
+
+ 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"
}
@@ -198,8 +239,40 @@ configure_for_frama_c() {
exit 1
fi
MACHDEP="$(echo $1 | tr a-z A-Z)"
- echo $MACHDEP
- CPP="gcc -E -nostdinc -fno-builtin -I${FRAMAC_SHARE}/libc -D__FC_MACHDEP_${MACHDEP}" ./configure
+ shift
+ CPP="gcc -E -nostdinc -fno-builtin -I${FRAMAC_SHARE}/libc -D__FC_MACHDEP_${MACHDEP}" ./configure "$@"
+}
+
+normalize_jcdb() {
+ path=""
+ if [ "$#" -eq 0 ]; then
+ path="./compile_commands.json"
+ else
+ path="$1"
+ fi
+ if [ ! -e "$path" ]; then
+ echo "error: cannot find file: $path";
+ exit 1
+ fi
+ sed "s|$PWD/||g" "$path" > "${path}.tmp"
+ cmp -s "$path" "${path}.tmp"
+ if [ $? -eq 0 ]; then
+ echo "No changes to be applied to $path"
+ rm "${path}.tmp"
+ else
+ echo "Differences to be applied to $path:"
+ diff -u0 "$path" "${path}.tmp"
+ read -p "Normalize $path? [y/N] " yn
+ case $yn in
+ [Yy])
+ mv "${path}.tmp" "$path"
+ echo "Normalization applied to $path"
+ ;;
+ *)
+ echo "Exiting without overwriting."
+ exit 0;;
+ esac
+ fi
}
case "$command" in
@@ -231,6 +304,14 @@ case "$command" in
shift;
configure_for_frama_c "$@";
;;
+ "make-wrapper")
+ shift;
+ ${FRAMAC_SHARE}/analysis-scripts/make_wrapper.py "$0" "$@";
+ ;;
+ "normalize-jcdb")
+ shift;
+ normalize_jcdb "$@";
+ ;;
*)
echo "error: unrecognized command: $command"
esac
diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 8400bc0b75b7c5909a1637aec9185fdd562ded33..52cb9fa3d6b427f8d8d608cb230b39e6c589eb9e 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -128,6 +128,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_wrapper.py: .ignore
share/analysis-scripts/parse-coverage.sh: .ignore
share/analysis-scripts/README.md: .ignore
share/analysis-scripts/results_display.py: .ignore
diff --git a/share/analysis-scripts/fc_stubs.c b/share/analysis-scripts/fc_stubs.c
new file mode 100644
index 0000000000000000000000000000000000000000..ca1ed39a3ba9e6bf25975698f1f058fd08548dc6
--- /dev/null
+++ b/share/analysis-scripts/fc_stubs.c
@@ -0,0 +1,23 @@
+// Stub for a main function which reads arguments from the command line, to be
+// used by the Eva plug-in.
+// This stub emulates non-deterministic input of up to 5 arguments, each up
+// to 256 characters long. This is sufficient to ensure arbitrary input in
+// virtually every case.
+// Do not forget to add option '-main eva_main' in order to use this stub.
+
+#ifdef __FRAMAC__
+# include "__fc_builtin.h"
+int main(int, char **);
+static volatile int nondet;
+int eva_main() {
+ int argc = Frama_C_interval(0, 5);
+ char argv0[256], argv1[256], argv2[256], argv3[256], argv4[256];
+ char *argv[5] = {argv0, argv1, argv2, argv3, argv4};
+ //@ loop unroll 5;
+ for (int i = 0; i < 5; i++) {
+ Frama_C_make_unknown(argv[i], 255);
+ argv[i][255] = 0;
+ }
+ return main(argc, argv);
+}
+#endif // __FRAMAC__
diff --git a/share/analysis-scripts/make_wrapper.py b/share/analysis-scripts/make_wrapper.py
new file mode 100755
index 0000000000000000000000000000000000000000..050643df89c5c074cb25515f9f3da3cbe96ab254
--- /dev/null
+++ b/share/analysis-scripts/make_wrapper.py
@@ -0,0 +1,133 @@
+#!/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 serves as wrapper to 'make' (when using the analysis-scripts
+# GNUmakefile template): it parses the output and suggests useful commands
+# whenever it can, by calling frama-c-script itself.
+
+import subprocess
+import sys
+import os
+import re
+from functools import partial
+
+if len(sys.argv) < 3:
+ print("usage: %s path-to-frama-c-script target" % sys.argv[0])
+ print(" Builds the specified target, parsing the output to")
+ print(" identify and recommend actions in case of failure.")
+ print(" The first argument must be the path to the frama-c-script")
+ print(" binary.")
+ sys.exit(1)
+
+framac_script = sys.argv[1]
+target = sys.argv[2]
+args = sys.argv[3:]
+
+out = subprocess.Popen(['make', target] + args,
+ stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
+
+output = out.communicate()[0].decode('utf-8')
+
+re_missing_spec = re.compile("Neither code nor specification for function ([^,]+),")
+re_recursive_call_start = re.compile("detected recursive call")
+re_recursive_call_end = re.compile("Use -eva-ignore-recursive-calls to ignore")
+
+tips = []
+
+lines = iter(output.splitlines())
+for line in lines:
+ print(line)
+ match = re_missing_spec.search(line)
+ if match:
+ fname = match.group(1)
+ def action(fname):
+ out = subprocess.Popen([framac_script, "find-fun", fname],
+ stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
+ output = out.communicate()[0].decode('utf-8')
+ re_possible_definers = re.compile("Possible definitions for function")
+ find_fun_lines = iter(output.splitlines())
+ for find_fun_line in find_fun_lines:
+ if re_possible_definers.match(find_fun_line):
+ found_files = [next(find_fun_lines)]
+ while True:
+ try:
+ found_files.append(next(find_fun_lines))
+ except StopIteration:
+ if len(found_files) > 1:
+ print("Found several files defining function '"
+ + fname + "', cannot recommend automatically.")
+ print("Check which one is appropriate and add it " +
+ "to the list of sources to be parsed:")
+ print("\n".join(found_files))
+ else:
+ print("Add the following file to the list of "
+ + "sources to be parsed:\n" + found_files[0])
+ return
+ print("Could not find any files defining " + fname + ".")
+ print("Find the sources defining it and add them, " +
+ "or provide a stub.")
+ tip = {"message": "Found function with missing spec: " + fname + "\n" +
+ " Looking for files defining it...",
+ "action":partial(action, fname)
+ }
+ tips.append(tip)
+ else:
+ match = re_recursive_call_start.search(line)
+ if match:
+ def action():
+ print("Consider patching or stubbing the recursive call, " +
+ "then re-run the analysis.")
+ msg_lines = []
+ line = next(lines)
+ while True:
+ match = re_recursive_call_end.search(line)
+ if match:
+ tip = {"message": "Found recursive call at:\n" +
+ "\n".join(msg_lines),
+ "action":action
+ }
+ tips.append(tip)
+ break
+ else:
+ msg_lines.append(line)
+ try:
+ line = next(lines)
+ except StopIteration:
+ print("** Error: EOF without ending recursive call stack?")
+ assert False
+
+if tips != []:
+ print("")
+ print("***** make-wrapper recommendations *****")
+ print("")
+ counter = 1
+ print("*** recommendation #" + str(counter) + " ***")
+ print("")
+ for tip in tips:
+ if counter > 1:
+ print("")
+ print("*** recommendation #" + str(counter) + " ***")
+ print(str(counter) + ". " + tip["message"])
+ counter += 1
+ tip["action"]()