From 4e27ffc166bc4a3c0d3e895781d609cf8b6feca0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 26 Mar 2021 12:33:36 +0100
Subject: [PATCH] [wp] added test for large arrays
---
src/plugins/wp/tests/wp_plugin/bigarray.c | 30 +++++++++++++++++++
.../wp_plugin/oracle/bigarray.0.res.oracle | 20 +++++++++++++
.../wp_plugin/oracle/bigarray.1.res.oracle | 13 ++++++++
3 files changed, 63 insertions(+)
create mode 100644 src/plugins/wp/tests/wp_plugin/bigarray.c
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle/bigarray.0.res.oracle
create mode 100644 src/plugins/wp/tests/wp_plugin/oracle/bigarray.1.res.oracle
diff --git a/src/plugins/wp/tests/wp_plugin/bigarray.c b/src/plugins/wp/tests/wp_plugin/bigarray.c
new file mode 100644
index 00000000000..266998147bf
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/bigarray.c
@@ -0,0 +1,30 @@
+/* run.config
+ OPT: -cpp-extra-args="-DFIT"
+ OPT: -cpp-extra-args="-DLARGE"
+ */
+
+/* run.config_qualif
+ DONTRUN:
+*/
+
+#include <stdint.h>
+#ifdef FIT
+#define SIZE (SIZE_MAX / sizeof(int))
+#endif
+#ifdef LARGE
+#define SIZE SIZE_MAX
+#endif
+
+/*@
+ assigns \result \from p[0..n-1];
+*/
+int f(int *p, int n)
+{
+ int s = 0;
+ int tmp[SIZE];
+ /*@ loop assigns i,s, tmp[..]; */
+ for (int i = 0; i < n; i++) {
+ s+= p[i]; tmp[i] = s;
+ }
+ return s;
+}
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/bigarray.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/bigarray.0.res.oracle
new file mode 100644
index 00000000000..c62b8402ac0
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle/bigarray.0.res.oracle
@@ -0,0 +1,20 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_plugin/bigarray.c (with preprocessing)
+[kernel] tests/wp_plugin/bigarray.c:26: Warning:
+ Cannot represent length of array as an attribute
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+ Function f
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_plugin/bigarray.c, line 25):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'f':
+Effect at line 26
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/bigarray.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/bigarray.1.res.oracle
new file mode 100644
index 00000000000..08244d758f0
--- /dev/null
+++ b/src/plugins/wp/tests/wp_plugin/oracle/bigarray.1.res.oracle
@@ -0,0 +1,13 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_plugin/bigarray.c (with preprocessing)
+[kernel] tests/wp_plugin/bigarray.c:26: Warning:
+ Cannot represent length of array as an attribute
+[wp] Running WP plugin...
+[wp] Warning: Missing RTE guards
+[wp] tests/wp_plugin/bigarray.c:26: Warning:
+ Array size too large (0xFFFFFFFFFFFFFFFF)
+[wp] tests/wp_plugin/bigarray.c:27: Warning:
+ Array size too large (0xFFFFFFFFFFFFFFFF)
+[wp] tests/wp_plugin/bigarray.c:19: User Error:
+ Array size too large (0xFFFFFFFFFFFFFFFF)
+[kernel] Plug-in wp aborted: invalid user input.
--
GitLab