diff --git a/share/analysis-scripts/make_wrapper.py b/share/analysis-scripts/make_wrapper.py index 7025db38a3d861520ef5a8fca21fb4f43a6a3d25..eee32358838c1a1a25af908def2d3d1a904b2c72 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 a291cdc31ab4cd51a4176787f3cbe67776a4972d..4d7db660ccc23d7fdb72db0fd967b104b62da771 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