[analysis-scripts/make_wrapper.py] more permissive inputs

share/analysis-scripts/make_wrapper.py

@@ -80,12 +80,44 @@ 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_stack_start = re.compile("^\s+stack:")
-re_recursive_call_stack_end = re.compile("\[kernel:annot:missing-spec\]")
+re_recursive_call_stack_end = re.compile("^\[")
 
 tips = []
 
 lines = iter(output_lines)
 for line in lines:
+    match = re_recursive_call_start.search(line)
+    if match:
+       def action():
+         print("Consider patching, stubbing or adding an ACSL " +
+               "specification to the recursive call, " +
+               "then re-run the analysis.")
+       while True:
+         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)
+             # note: this ending line can also match re_missing_spec
+             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
     match = re_missing_spec.search(line)
     if match:
        fname = match.group(1)
@@ -120,38 +152,6 @@ for line in lines:
               "action":partial(action, fname)
        }
        tips.append(tip)
-    else:
-       match = re_recursive_call_start.search(line)
-       if match:
-          def action():
-             print("Consider patching, stubbing or adding an ACSL " +
-                   "specification to the recursive call, " +
-                   "then re-run the analysis.")
-          while True:
-             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("")

src/plugins/value/engine/recursion.ml

@@ -51,7 +51,10 @@ let get_spec kinstr kf =
       "@[Recursive call to %a@ without a specification.@ \
        Generating probably incomplete assigns to interpret the call.@ \
        Try to increase@ the %s parameter@ \
-       or write a correct specification@ for function %a.%t@]"
+       or write a correct specification@ for function %a.@\n%t@]"
+      (* note: the "\n" before the pretty print of the stack is required by:
+         FRAMAC_SHARE/analysis-scripts/make_wrapper.py
+      *)
       Kernel_function.pretty kf
       Value_parameters.RecursiveUnroll.name
       Kernel_function.pretty kf