Merge branch 'feature/andre/make-wrapper-output' into 'master'

[frama-c-script] improve output of make-wrapper

See merge request frama-c/frama-c!2274

share/analysis-scripts/analysis.mk

@@ -84,7 +84,7 @@ else
   SED_UNBUFFERED:=sed --unbuffered
 ifneq (,$(wildcard /usr/bin/time))
 define time_with_output
-  /usr/bin/time --format='user_time=%U\nmemory=%M' --output="$(1)"
+  /usr/bin/time -f 'user_time=%U\nmemory=%M' -o "$(1)"
 endef
 else
 define time_with_output
@@ -143,7 +143,7 @@ clean-backups:
 
 HR_TIMESTAMP := $(shell date +"%H:%M:%S %d/%m/%Y")# Human readable
 DIR          := $(dir $(lastword $(MAKEFILE_LIST)))
-SHELL        := /bin/bash
+SHELL        := $(shell which bash)
 .SHELLFLAGS  := -eu -o pipefail -c
 
 .ONESHELL:

share/analysis-scripts/make_wrapper.py

@@ -32,6 +32,7 @@ import re
 import subprocess
 import sys
 from functools import partial
+import tempfile
 
 MIN_PYTHON = (3, 6) # for automatic Path conversions
 if sys.version_info < MIN_PYTHON:
@@ -40,7 +41,7 @@ if sys.version_info < MIN_PYTHON:
 parser = argparse.ArgumentParser(description="""
 Builds the specified target, parsing the output to identify and recommend
 actions in case of failure.""")
-parser.add_argument('--make-dir', metavar='DIR', default=".frama-c", nargs=1,
+parser.add_argument('--make-dir', metavar='DIR', default=".frama-c",
                     help='directory containing the makefile (default: .frama-c)')
 
 (make_dir_arg, args) = parser.parse_known_args()
@@ -52,10 +53,19 @@ if not framac_bin:
    sys.exit("error: FRAMAC_BIN not in environment (set by frama-c-script)")
 framac_script = f"{framac_bin}/frama-c-script"
 
-out = subprocess.Popen(['make', "-C", make_dir] + args,
-                       stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
-
-output = out.communicate()[0].decode('utf-8')
+output_lines = []
+cmd_list = ['make', "-C", make_dir] + args
+with subprocess.Popen(cmd_list,
+                      stdout=subprocess.PIPE,
+                      stderr=subprocess.PIPE) as proc:
+  while True:
+    line = proc.stdout.readline()
+    if line:
+       sys.stdout.buffer.write(line)
+       sys.stdout.flush()
+       output_lines.append(line.decode('utf-8'))
+    else:
+       break
 
 re_missing_spec = re.compile("Neither code nor specification for function ([^,]+),")
 re_recursive_call_start = re.compile("detected recursive call")
@@ -63,9 +73,8 @@ re_recursive_call_end = re.compile("Use -eva-ignore-recursive-calls to ignore")
 
 tips = []
 
-lines = iter(output.splitlines())
+lines = iter(output_lines)
 for line in lines:
-    print(line)
     match = re_missing_spec.search(line)
     if match:
        fname = match.group(1)

tests/fc_script/make-for-make-wrapper.mk

+# Customized makefile template for testing 'frama-c-script make-wrapper'.
+
+include $(shell $(FRAMAC) -no-autoload-plugins -print-share-path)/analysis-scripts/prologue.mk
+
+FCFLAGS     += \
+  -kernel-warn-key annot:missing-spec=abort \
+  -kernel-warn-key typing:implicit-function-declaration=abort \
+
+EVAFLAGS    += \
+  -eva-warn-key builtins:missing-spec=abort \
+
+## Analysis targets (suffixed with .eva)
+TARGETS = make-for-make-wrapper.eva
+
+make-for-make-wrapper.parse: \
+  make-wrapper.c \
+  make-wrapper2.c \
+  # make-wrapper3.c is deliberately absent of this list
+
+### Epilogue. Do not modify this block. #######################################
+include $(shell $(FRAMAC) -no-autoload-plugins -print-share-path)/analysis-scripts/epilogue.mk
+###############################################################################

tests/fc_script/make-wrapper.c

+/* run.config
+   NOFRAMAC: testing frama-c-script
+   COMMENT: we must filter 'make:' output lines, since they differ when run by the CI (e.g. mention to jobserver)
+   EXECNOW: LOG make-wrapper.res LOG make-wrapper.err cd @PTEST_DIR@ && touch make-wrapper2.c && touch make-wrapper3.c && FRAMAC=../../bin/frama-c ../../bin/frama-c-script make-wrapper --make-dir . -f make-for-make-wrapper.mk | sed -e "s:$PWD:PWD:g" | grep -v "^make.*" > result/make-wrapper.res 2> result/make-wrapper.err && rm -rf make-for-make-wrapper.parse make-for-make-wrapper.eva
+*/
+
+int defined(int a);
+
+int specified(int a);
+
+int external(int a);
+
+int main() {
+  int a = 42;
+  a = defined(a);
+  a = specified(a);
+  a = external(a);
+}

tests/fc_script/make-wrapper2.c

+/* run.config
+   DONTRUN: part of the test in make-wrapper.c
+*/
+
+int defined(int a) {
+  return a + 1;
+}
+
+/*@
+  assigns \result \from a;
+  ensures \result == a + 2;
+ */
+int specified(int a);
+
+// defined in another, non-included, file
+int external(int a);

tests/fc_script/make-wrapper3.c

+/* run.config
+   DONTRUN: part of the test in make-wrapper.c
+*/
+
+// This file contains a definition for function 'external', but it is _not_
+// included when parsing 'make-wrapper.c'. This triggers a make-wrapper message.
+int external(int a) {
+  return a + 3;
+}

tests/fc_script/oracle/find_fun1.res

-Looking for 'main2' inside 5 file(s)...
+Looking for 'main2' inside 8 file(s)...
 Possible declarations for function 'main2' in the following file(s):
   tests/fc_script/for-find-fun.c
 Possible definitions for function 'main2' in the following file(s):

tests/fc_script/oracle/find_fun2.res

-Looking for 'main3' inside 5 file(s)...
+Looking for 'main3' inside 8 file(s)...
 Possible declarations for function 'main3' in the following file(s):
   tests/fc_script/for-find-fun2.c
 Possible definitions for function 'main3' in the following file(s):

tests/fc_script/oracle/find_fun3.res

-Looking for 'false_positive' inside 5 file(s)...
+Looking for 'false_positive' inside 8 file(s)...
 No declaration/definition found for function 'false_positive'

tests/fc_script/oracle/make-wrapper.res

+
+Command: ../../bin/frama-c  -kernel-warn-key annot:missing-spec=abort -kernel-warn-key typing:implicit-function-declaration=abort   -cpp-extra-args="" make-wrapper.c make-wrapper2.c(B
+
+[kernel] Parsing make-wrapper.c (with preprocessing)
+[kernel] Parsing make-wrapper2.c (with preprocessing)
+
+Command: ../../bin/frama-c  -kernel-warn-key annot:missing-spec=abort -kernel-warn-key typing:implicit-function-declaration=abort  -eva -eva-no-print -eva-no-show-progress -eva-msg-key=-initial-state -eva-print-callstacks -eva-warn-key alarm=inactive -no-deps-print -no-calldeps-print -eva-warn-key garbled-mix -calldeps -from-verbose 0   -eva-warn-key builtins:missing-spec=abort (B
+
+[eva] Analyzing a complete application starting at main
+[eva] Computing initial state
+[eva] Initial state computed
+[eva] using specification for function specified
+[kernel:annot:missing-spec] make-wrapper.c:17: Warning: 
+  Neither code nor specification for function external, generating default assigns from the prototype
+[kernel] User Error: warning annot:missing-spec treated as fatal error.
+[kernel] Frama-C aborted: invalid user input.
+[kernel] Warning: attempting to save on non-zero exit code: modifying filename into `PWD/make-for-make-wrapper.eva/framac.sav.error'.
+
+***** make-wrapper recommendations *****
+
+*** recommendation #1 ***
+
+1. Found function with missing spec: external
+   Looking for files defining it...
+Add the following file to the list of sources to be parsed:
+  make-wrapper3.c