From 63976d10437d7ccabc48e2386280ea15116a39e2 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.maroneze@cea.fr>
Date: Thu, 1 Oct 2020 18:08:44 +0200
Subject: [PATCH] [analysis-scripts] minor fix to make_wrapper.py; add test
---
share/analysis-scripts/make_wrapper.py | 3 ++-
tests/fc_script/make-for-make-wrapper.mk | 22 +++++++++++++++++++
tests/fc_script/make-wrapper.c | 17 ++++++++++++++
tests/fc_script/make-wrapper2.c | 16 ++++++++++++++
tests/fc_script/make-wrapper3.c | 9 ++++++++
tests/fc_script/oracle/find_fun1.res | 2 +-
tests/fc_script/oracle/find_fun2.res | 2 +-
tests/fc_script/oracle/find_fun3.res | 2 +-
tests/fc_script/oracle/make-wrapper.err | 0
tests/fc_script/oracle/make-wrapper.res | 28 ++++++++++++++++++++++++
10 files changed, 97 insertions(+), 4 deletions(-)
create mode 100644 tests/fc_script/make-for-make-wrapper.mk
create mode 100644 tests/fc_script/make-wrapper.c
create mode 100644 tests/fc_script/make-wrapper2.c
create mode 100644 tests/fc_script/make-wrapper3.c
create mode 100644 tests/fc_script/oracle/make-wrapper.err
create mode 100644 tests/fc_script/oracle/make-wrapper.res
diff --git a/share/analysis-scripts/make_wrapper.py b/share/analysis-scripts/make_wrapper.py
index 5574816cf13..25cb2b838ae 100755
--- a/share/analysis-scripts/make_wrapper.py
+++ b/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:
diff --git a/tests/fc_script/make-for-make-wrapper.mk b/tests/fc_script/make-for-make-wrapper.mk
new file mode 100644
index 00000000000..983f2a16d9f
--- /dev/null
+++ b/tests/fc_script/make-for-make-wrapper.mk
@@ -0,0 +1,22 @@
+# 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
+###############################################################################
diff --git a/tests/fc_script/make-wrapper.c b/tests/fc_script/make-wrapper.c
new file mode 100644
index 00000000000..4375eef42f7
--- /dev/null
+++ b/tests/fc_script/make-wrapper.c
@@ -0,0 +1,17 @@
+/* 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);
+}
diff --git a/tests/fc_script/make-wrapper2.c b/tests/fc_script/make-wrapper2.c
new file mode 100644
index 00000000000..0f97864c1b8
--- /dev/null
+++ b/tests/fc_script/make-wrapper2.c
@@ -0,0 +1,16 @@
+/* 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);
diff --git a/tests/fc_script/make-wrapper3.c b/tests/fc_script/make-wrapper3.c
new file mode 100644
index 00000000000..83ed541f1db
--- /dev/null
+++ b/tests/fc_script/make-wrapper3.c
@@ -0,0 +1,9 @@
+/* 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;
+}
diff --git a/tests/fc_script/oracle/find_fun1.res b/tests/fc_script/oracle/find_fun1.res
index a846b6beb54..3e35782af42 100644
--- a/tests/fc_script/oracle/find_fun1.res
+++ b/tests/fc_script/oracle/find_fun1.res
@@ -1,4 +1,4 @@
-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):
diff --git a/tests/fc_script/oracle/find_fun2.res b/tests/fc_script/oracle/find_fun2.res
index 273cc015b4e..e9f42fdf76a 100644
--- a/tests/fc_script/oracle/find_fun2.res
+++ b/tests/fc_script/oracle/find_fun2.res
@@ -1,4 +1,4 @@
-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):
diff --git a/tests/fc_script/oracle/find_fun3.res b/tests/fc_script/oracle/find_fun3.res
index a7059bd1c96..65fc349325d 100644
--- a/tests/fc_script/oracle/find_fun3.res
+++ b/tests/fc_script/oracle/find_fun3.res
@@ -1,2 +1,2 @@
-Looking for 'false_positive' inside 5 file(s)...
+Looking for 'false_positive' inside 8 file(s)...
No declaration/definition found for function 'false_positive'
diff --git a/tests/fc_script/oracle/make-wrapper.err b/tests/fc_script/oracle/make-wrapper.err
new file mode 100644
index 00000000000..e69de29bb2d
diff --git a/tests/fc_script/oracle/make-wrapper.res b/tests/fc_script/oracle/make-wrapper.res
new file mode 100644
index 00000000000..d2d19765aa4
--- /dev/null
+++ b/tests/fc_script/oracle/make-wrapper.res
@@ -0,0 +1,28 @@
+make: Entering directory 'PWD'
+
+[34mCommand: ../../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[m
+
+[kernel] Parsing make-wrapper.c (with preprocessing)
+[kernel] Parsing make-wrapper2.c (with preprocessing)
+
+[34mCommand: ../../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[m
+
+[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
--
GitLab