From 043dfaeebf35df6a417d3d422319ff4f80a6efd6 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Wed, 15 Dec 2021 15:05:46 +0100
Subject: [PATCH] [analysis-scripts/make_wrapper.py] more permissive inputs
---
share/analysis-scripts/make_wrapper.py | 66 +++++++++++++-------------
src/plugins/value/engine/recursion.ml | 5 +-
2 files changed, 37 insertions(+), 34 deletions(-)
diff --git a/share/analysis-scripts/make_wrapper.py b/share/analysis-scripts/make_wrapper.py
index 3dba6e1c275..7f9f5b9b517 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 eadcb4cbf94..71c6807a8fe 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
--
GitLab