diff --git a/share/analysis-scripts/make_wrapper.py b/share/analysis-scripts/make_wrapper.py index 3dba6e1c2752541daab67256f0ec4568c602298d..7f9f5b9b517b3be2e1eacdc325dad720ee5eed69 100755 --- a/share/analysis-scripts/make_wrapper.py +++ b/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("") diff --git a/src/plugins/value/engine/recursion.ml b/src/plugins/value/engine/recursion.ml index eadcb4cbf943e945f81cd2c325484dbfa62fc092..71c6807a8fec3367044cdfc1717b4e4722b2629f 100644 --- a/src/plugins/value/engine/recursion.ml +++ b/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