From e8b0b40faa1dfaaa06fa95487c39657ba52b1b13 Mon Sep 17 00:00:00 2001
From: Allan Blanchard <allan.blanchard@cea.fr>
Date: Wed, 15 Sep 2021 15:59:08 +0200
Subject: [PATCH] [tests] Fixes make wrapper test
---
share/analysis-scripts/make_wrapper.py | 9 ++++++---
tests/fc_script/oracle/make-wrapper.res | 2 +-
2 files changed, 7 insertions(+), 4 deletions(-)
diff --git a/share/analysis-scripts/make_wrapper.py b/share/analysis-scripts/make_wrapper.py
index 7025db38a3d..eee32358838 100755
--- a/share/analysis-scripts/make_wrapper.py
+++ b/share/analysis-scripts/make_wrapper.py
@@ -87,7 +87,7 @@ with subprocess.Popen(cmd_list, stdout=subprocess.PIPE, stderr=subprocess.PIPE)
else:
break
-re_missing_spec = re.compile("Neither code nor specification for function ([^,]+),")
+re_missing_spec = re.compile("Neither code nor (specification|[^ ]+ assigns clause) for function ([^,]+),")
re_recursive_call_start = re.compile("detected recursive call")
re_recursive_call_stack_start = re.compile(r"^\s+stack:")
re_recursive_call_stack_end = re.compile(r"^\[")
@@ -134,7 +134,8 @@ for line in lines:
assert False
match = re_missing_spec.search(line)
if match:
- fname = match.group(1)
+ spec_kind = match.group(1)
+ fname = match.group(2)
def _action(fname):
out = subprocess.Popen(
@@ -174,7 +175,9 @@ for line in lines:
print("Find the sources defining it and add them, " + "or provide a stub.")
tip = {
- "message": "Found function with missing spec: "
+ "message": "Found function with missing "
+ + spec_kind
+ + ": "
+ fname
+ "\n"
+ " Looking for files defining it...",
diff --git a/tests/fc_script/oracle/make-wrapper.res b/tests/fc_script/oracle/make-wrapper.res
index a291cdc31ab..4d7db660ccc 100644
--- a/tests/fc_script/oracle/make-wrapper.res
+++ b/tests/fc_script/oracle/make-wrapper.res
@@ -11,7 +11,7 @@
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
+2. Found function with missing specification: 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-wrapper.c
--
GitLab