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 b797957eeb5db40710aaf6eb46af17c2ca03c0f0..e3dafca01d88506b4c9402155b7c5b0f84f1b29e 100755
--- a/bin/frama-c-script
+++ b/bin/frama-c-script
@@ -59,6 +59,21 @@ if [ $# -lt 1 ]; then
echo " Monitors and summarizes multiple analyses dispatched by a Makefile"
echo " in the current PWD."
echo " Use $0 summary --help for more informations."
+ echo ""
+ echo " - configure <machdep>"
+ echo " Runs an existing configure script to only consider files"
+ echo " in Frama-C's libc; this will hopefully disable non-essential"
+ 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
@@ -105,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
@@ -115,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"
}
@@ -185,6 +233,48 @@ EOF
fi
}
+configure_for_frama_c() {
+ if [ "$#" -eq 0 ]; then
+ echo "error: 'configure' command requires a machdep";
+ exit 1
+ fi
+ MACHDEP="$(echo $1 | tr a-z A-Z)"
+ 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
"make-template")
shift;
@@ -210,6 +300,18 @@ case "$command" in
shift;
${FRAMAC_SHARE}/analysis-scripts/summary.py "$@";
;;
+ "configure")
+ 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/find_fun.py b/share/analysis-scripts/find_fun.py
index b8a3565da0bad21178f815a28b18749f3405d46d..5ef92a69b6287eeb95687c4cc6c443bec8bf503b 100755
--- a/share/analysis-scripts/find_fun.py
+++ b/share/analysis-scripts/find_fun.py
@@ -101,8 +101,8 @@ else:
if possible_declarators != []:
print("Possible declarations for function '%s' in the following file(s):"
% fname)
- print(" " + "\n ".join(possible_declarators))
+ print(" " + "\n ".join(map(os.path.relpath, possible_declarators)))
if possible_definers != []:
print("Possible definitions for function '%s' in the following file(s):"
% fname)
- print(" " + "\n ".join(possible_definers))
+ print(" " + "\n ".join(map(os.path.relpath, possible_definers)))
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"]()
diff --git a/src/kernel_services/ast_queries/json_compilation_database.ok.ml b/src/kernel_services/ast_queries/json_compilation_database.ok.ml
index 2442e726b6a3dd8583bed2415b238e1fd64af819..8d31f5b6709a8bedd67c52e864f04b4076b00881 100644
--- a/src/kernel_services/ast_queries/json_compilation_database.ok.ml
+++ b/src/kernel_services/ast_queries/json_compilation_database.ok.ml
@@ -81,6 +81,10 @@ let split_command_args s =
let c = String.get s i in
let new_state, new_acc =
match state, prev_c, c with
+ | Outside_quote, '\\', c when c = '\"' || c = '\'' ->
+ (* escaped quote, continue with previous arg *)
+ Buffer.add_char buf c;
+ state, acc
| Outside_quote, _, q when q = '\'' || q = '\"' ->
(* continue previous arg with q *)
Buffer.add_char buf q;
diff --git a/tests/jcdb/jcdb.c b/tests/jcdb/jcdb.c
index ddf00afcd0acb406597062b30cab1a821f769faf..f2389fe2e8ada1276a640ceb2689b7ff4f5a6f76 100644
--- a/tests/jcdb/jcdb.c
+++ b/tests/jcdb/jcdb.c
@@ -1,7 +1,7 @@
/* run.config
EXECNOW: make -s @PTEST_DIR@/@PTEST_NAME@.cmxs
OPT: -json-compilation-database @PTEST_DIR@ -print
-OPT: -json-compilation-database @PTEST_DIR@/with_arguments.json -print
+OPT: @PTEST_DIR@/jcdb2.c -json-compilation-database @PTEST_DIR@/with_arguments.json -print
OPT: -json-compilation-database @PTEST_DIR@/with_arguments.json -no-autoload-plugins -load-module @PTEST_DIR@/@PTEST_NAME@.cmxs
EXECNOW: LOG list_files.res LOG list_files.err share/analysis-scripts/list_files.py @PTEST_DIR@/compile_commands_working.json > @PTEST_DIR@/result/list_files.res 2> @PTEST_DIR@/result/list_files.err
*/
diff --git a/tests/jcdb/oracle/jcdb.1.res.oracle b/tests/jcdb/oracle/jcdb.1.res.oracle
index 87d1d04f76ffe2da596bb596c8ebbb67ea0e9d88..3fbf07641f32aa75dd444c39500a1a58a7fe4029 100644
--- a/tests/jcdb/oracle/jcdb.1.res.oracle
+++ b/tests/jcdb/oracle/jcdb.1.res.oracle
@@ -1,4 +1,5 @@
[kernel] Parsing tests/jcdb/jcdb.c (with preprocessing)
+[kernel] Parsing tests/jcdb/jcdb2.c (with preprocessing)
/* Generated by Frama-C */
#include "errno.h"
#include "stdarg.h"
diff --git a/tests/jcdb/with_arguments.json b/tests/jcdb/with_arguments.json
index 49b11f5d572af2f851c3795ef79d706217af6881..4217869b5eafd76539298bf3156a9d8d7a1df764 100644
--- a/tests/jcdb/with_arguments.json
+++ b/tests/jcdb/with_arguments.json
@@ -16,5 +16,9 @@
"-UTOUNDEF"
],
"file": "jcdb.c"
+ },
+ { "directory": "tests/jcdb",
+ "command": "/usr/bin/cc -DONION_VERSION=\\\"0.1.tr\\\" -Ibla -o jcdb2.o -c jcdb2.c jcdb.c",
+ "file": "jcdb2.c"
}
]