[wp] added test for large arrays

src/plugins/wp/tests/wp_plugin/bigarray.c

+/* 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;
+}

src/plugins/wp/tests/wp_plugin/oracle/bigarray.0.res.oracle

+# 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.
+
+------------------------------------------------------------

src/plugins/wp/tests/wp_plugin/oracle/bigarray.1.res.oracle

+# 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.