[analysis-scripts] fix tips for recursion in make-wrapper; add test

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("")

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);

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)

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