diff --git a/share/analysis-scripts/make_wrapper.py b/share/analysis-scripts/make_wrapper.py
index ac42c8d36bff9465dd8b00cbf768d7123a56b57e..2fa09b4071263c4e8a86aad0726fffee8da0a601 100755
--- a/share/analysis-scripts/make_wrapper.py
+++ b/share/analysis-scripts/make_wrapper.py
@@ -69,7 +69,8 @@ with subprocess.Popen(cmd_list,
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")
+re_recursive_call_stack_start = re.compile("^\s+stack:")
+re_recursive_call_stack_end = re.compile("\[kernel:annot:missing-spec\]")
tips = []
@@ -113,26 +114,34 @@ for line in lines:
match = re_recursive_call_start.search(line)
if match:
def action():
- print("Consider patching or stubbing the recursive call, " +
+ print("Consider patching, stubbing or adding an ACSL " +
+ "specification to 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
+ msg_lines = []
+ match = re_recursive_call_start.search(line)
+ try:
+ while not match:
+ line = next(lines)
+ match = re_recursive_call_start.search(line)
+ match = None
+ while not match:
+ line = next(lines)
+ match = re_recursive_call_stack_start.search(line)
+ match = None
+ while not match:
+ msg_lines.append(line)
+ line = next(lines)
+ match = re_recursive_call_stack_end.search(line)
+ tip = {"message": "Found recursive call at:\n" +
+ "".join(msg_lines),
+ "action":action
+ }
+ tips.append(tip)
+ break
+ except StopIteration:
+ print("** Error: did not match expected regex before EOF")
+ assert False
if tips != []:
print("")
diff --git a/tests/fc_script/make-wrapper.c b/tests/fc_script/make-wrapper.c
index 9fdf20fa96c49dccd7692f09ad85e2f37242c7eb..b52d6c74e87425c96857b0e0bedbcc77f6085f7e 100644
--- a/tests/fc_script/make-wrapper.c
+++ b/tests/fc_script/make-wrapper.c
@@ -10,8 +10,17 @@ int specified(int a);
int external(int a);
+int large_name_to_force_line_break_in_stack_msg(void) {
+ return large_name_to_force_line_break_in_stack_msg();
+}
+
+int rec(void) {
+ return large_name_to_force_line_break_in_stack_msg();
+}
+
int main() {
int a = 42;
+ a = rec();
a = defined(a);
a = specified(a);
a = external(a);
diff --git a/tests/fc_script/oracle/heuristic_list_functions.res b/tests/fc_script/oracle/heuristic_list_functions.res
index fe8495493cd286842024661ea2ed28407625a805..32dba2e292db55b4813517058336a9e52cc76090 100644
--- a/tests/fc_script/oracle/heuristic_list_functions.res
+++ b/tests/fc_script/oracle/heuristic_list_functions.res
@@ -15,7 +15,9 @@ tests/fc_script/main3.c:6:9: main (definition)
tests/fc_script/make-wrapper.c:7:7: defined (declaration)
tests/fc_script/make-wrapper.c:9:9: specified (declaration)
tests/fc_script/make-wrapper.c:11:11: external (declaration)
-tests/fc_script/make-wrapper.c:13:18: main (definition)
+tests/fc_script/make-wrapper.c:13:15: large_name_to_force_line_break_in_stack_msg (definition)
+tests/fc_script/make-wrapper.c:17:19: rec (definition)
+tests/fc_script/make-wrapper.c:21:27: main (definition)
tests/fc_script/make-wrapper2.c:5:7: defined (definition)
tests/fc_script/make-wrapper2.c:13:13: specified (declaration)
tests/fc_script/make-wrapper2.c:16:16: external (declaration)
diff --git a/tests/fc_script/oracle/make-wrapper.res b/tests/fc_script/oracle/make-wrapper.res
index 18747999ef64bba9e9fd47673c4c03caacef85f2..09358673bd043241721520d914345a9a782b35d5 100644
--- a/tests/fc_script/oracle/make-wrapper.res
+++ b/tests/fc_script/oracle/make-wrapper.res
@@ -9,9 +9,21 @@ Command: ../../bin/frama-c -kernel-warn-key annot:missing-spec=abort -kernel-war
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
[eva] Initial state computed
-[eva] using specification for function specified
-[kernel:annot:missing-spec] make-wrapper.c:17: Warning:
- Neither code nor specification for function external, generating default assigns from the prototype
+[eva:recursion] make-wrapper.c:14:
+ detected recursive call
+ of function large_name_to_force_line_break_in_stack_msg.
+[eva] make-wrapper.c:14: User Error:
+ Recursive call to large_name_to_force_line_break_in_stack_msg
+ without a specification.
+ Generating probably incomplete assigns to interpret the call. Try to increase
+ the -eva-unroll-recursive-calls parameter or write a correct specification
+ for function large_name_to_force_line_break_in_stack_msg.
+ stack: large_name_to_force_line_break_in_stack_msg :: make-wrapper.c:14 <-
+ large_name_to_force_line_break_in_stack_msg :: make-wrapper.c:18 <-
+ rec :: make-wrapper.c:23 <-
+ main
+[kernel:annot:missing-spec] make-wrapper.c:13: Warning:
+ Neither code nor specification for function large_name_to_force_line_break_in_stack_msg, generating default assigns from the prototype
[kernel] User Error: warning annot:missing-spec treated as fatal error.
[kernel] Frama-C aborted: invalid user input.
[kernel] Warning: attempting to save on non-zero exit code: modifying filename into `PWD/make-for-make-wrapper.eva/framac.sav.error'.
@@ -20,7 +32,16 @@ Command: ../../bin/frama-c -kernel-warn-key annot:missing-spec=abort -kernel-war
*** recommendation #1 ***
-1. Found function with missing spec: external
+1. Found recursive call at:
+ stack: large_name_to_force_line_break_in_stack_msg :: make-wrapper.c:14 <-
+ large_name_to_force_line_break_in_stack_msg :: make-wrapper.c:18 <-
+ rec :: make-wrapper.c:23 <-
+ main
+
+Consider patching, stubbing or adding an ACSL specification to the recursive call, then re-run the analysis.
+
+*** recommendation #2 ***
+2. Found function with missing spec: large_name_to_force_line_break_in_stack_msg
Looking for files defining it...
Add the following file to the list of sources to be parsed:
- make-wrapper3.c
+ make-wrapper.c