[analysis-scripts] minor fix to make_wrapper.py; add test

share/analysis-scripts/make_wrapper.py

@@ -54,7 +54,8 @@ if not framac_bin:
 framac_script = f"{framac_bin}/frama-c-script"
 
 _logfd, logname = tempfile.mkstemp(prefix="make_wrapper_tmp_")
-with subprocess.Popen(['make', "-C", make_dir] + args,
+cmd_list = ['make', "-C", make_dir] + args
+with subprocess.Popen(cmd_list,
                       stdout=subprocess.PIPE,
                       stderr=subprocess.STDOUT) as proc, \
      open (logname, "bw") as logfile:

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
+   EXECNOW: LOG make-wrapper.res LOG make-wrapper.err cd @PTEST_DIR@ && 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:.*Error" > 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

+make: Entering directory 'PWD'
+
+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:16: 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: Leaving directory 'PWD'
+
+***** 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