From 0e233e833ba00560a7925ddbce5d220dfe1fdde0 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?C=C3=A9cile=20RUET-CROS?= <cecile.ruet-cros@cea.fr>
Date: Wed, 9 Oct 2024 17:34:46 +0200
Subject: [PATCH] [wp/region] + oracle tests (arrays + union)
---
src/plugins/wp/tests/wp_region/array.c | 26 +
src/plugins/wp/tests/wp_region/copy_array.c | 21 +
.../tests/wp_region/oracle/array.res.oracle | 502 ++++++++++++++++++
.../wp_region/oracle/copy_array.res.oracle | 501 +++++++++++++++++
.../tests/wp_region/oracle/union.res.oracle | 114 ++++
.../wp_region/oracle_qualif/array.res.oracle | 384 ++++++++++++++
.../oracle_qualif/copy_array.res.oracle | 320 +++++++++++
.../wp_region/oracle_qualif/union.res.oracle | 71 +++
src/plugins/wp/tests/wp_region/union.i | 16 +
9 files changed, 1955 insertions(+)
create mode 100644 src/plugins/wp/tests/wp_region/array.c
create mode 100644 src/plugins/wp/tests/wp_region/copy_array.c
create mode 100644 src/plugins/wp/tests/wp_region/oracle/array.res.oracle
create mode 100644 src/plugins/wp/tests/wp_region/oracle/copy_array.res.oracle
create mode 100644 src/plugins/wp/tests/wp_region/oracle/union.res.oracle
create mode 100644 src/plugins/wp/tests/wp_region/oracle_qualif/array.res.oracle
create mode 100644 src/plugins/wp/tests/wp_region/oracle_qualif/copy_array.res.oracle
create mode 100644 src/plugins/wp/tests/wp_region/oracle_qualif/union.res.oracle
create mode 100644 src/plugins/wp/tests/wp_region/union.i
diff --git a/src/plugins/wp/tests/wp_region/array.c b/src/plugins/wp/tests/wp_region/array.c
new file mode 100644
index 00000000000..dcc7a41a65a
--- /dev/null
+++ b/src/plugins/wp/tests/wp_region/array.c
@@ -0,0 +1,26 @@
+struct S {
+ int len;
+ int content[10];
+};
+/*@ predicate pointed(struct S *p, struct S * q) = p==q || \separated(p,q);
+*/
+
+
+/*@
+ requires pointed(a, b);
+ region AB: *a, *b;
+ ensures a!=b ==> a->content[2] == \old(a->content[2]) + b->content[2];
+ ensures a==b ==> a->content[2] == 2*\old(a->content[2]);
+ ensures a->content[2] == \old(a->content[2] + b->content[2]);
+ ensures a->content[4] == \old(a->content[4]);
+*/
+void add_first4(struct S * a , struct S * b )
+{
+ a->content[0] += b->content[0];
+ a->content[1] += b->content[1];
+ note1:
+ a->content[2] += b->content[2];
+ //@ assert a!=b ==> a->content[2] == \at(a->content[2],note1) + b->content[2];
+ //@ assert a==b ==> a->content[2] == 2*\at(a->content[2],note1);
+ a->content[3] += b->content[3];
+}
diff --git a/src/plugins/wp/tests/wp_region/copy_array.c b/src/plugins/wp/tests/wp_region/copy_array.c
new file mode 100644
index 00000000000..4084930a672
--- /dev/null
+++ b/src/plugins/wp/tests/wp_region/copy_array.c
@@ -0,0 +1,21 @@
+
+/*@ requires n>=0 ;
+ requires \separated( a+ (0..n-1) , b + (0..n-1) );
+ ensures \forall integer k ; 0 <= k < n ==> a[k] == b[k] ;
+ assigns a[0..n-1] ;
+ region AB: a[..], b[..];
+ */
+void copy( int * a , int * b , int n )
+{
+ /*@ loop invariant Range: 0 <= i <= n ;
+ loop invariant Copy: \forall integer k ; 0 <= k < i ==> a[k] == b[k] ;
+ loop assigns i , a[0..n-1] ;
+ loop variant n - i;
+ */
+ for (int i = 0 ; i < n ; i++) {
+ L:
+ a[i] = b[i] ;
+ /*@ assert A: \forall integer k ; 0 <= k < i ==> a[k] == \at(a[k],L); */
+ /*@ assert B: \forall integer k ; 0 <= k < i ==> b[k] == \at(b[k],L); */
+ }
+}
diff --git a/src/plugins/wp/tests/wp_region/oracle/array.res.oracle b/src/plugins/wp/tests/wp_region/oracle/array.res.oracle
new file mode 100644
index 00000000000..6fd76bcdc0e
--- /dev/null
+++ b/src/plugins/wp/tests/wp_region/oracle/array.res.oracle
@@ -0,0 +1,502 @@
+# frama-c -wp -wp-model 'Region' [...]
+[kernel] Parsing array.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal add_first4_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal add_first4_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+------------------------------------------------------------
+ Function add_first4
+------------------------------------------------------------
+
+Goal Post-condition (file array.c, line 12) in 'add_first4':
+Let a_1 = shiftfield_F1_S_content(a).
+Let a_2 = shift_sint32(a_1, 0).
+Let x = Msint32_0[a_2].
+Let a_3 = shiftfield_F1_S_content(b).
+Let x_1 = Msint32_0[shift_sint32(a_3, 0)].
+Let m = Msint32_0[a_2 <- x + x_1].
+Let a_4 = shift_sint32(a_1, 1).
+Let x_2 = Msint32_0[a_4].
+Let x_3 = m[shift_sint32(a_3, 1)].
+Let m_1 = m[a_4 <- x_2 + x_3].
+Let a_5 = shift_sint32(a_1, 2).
+Let x_4 = Msint32_0[a_5].
+Let a_6 = shift_sint32(a_3, 2).
+Let x_5 = m_1[a_6].
+Let x_6 = x_4 + x_5.
+Let m_2 = m_1[a_5 <- x_6].
+Let a_7 = shift_sint32(a_1, 3).
+Let x_7 = Msint32_0[a_7].
+Let x_8 = m_2[shift_sint32(a_3, 3)].
+Let x_9 = m_2[a_7 <- x_7 + x_8][a_6].
+Assume {
+ Type: is_sint32(x) /\ is_sint32(x_2) /\ is_sint32(x_4) /\ is_sint32(x_7) /\
+ is_sint32(Msint32_0[shift_sint32(a_1, 4)]) /\ is_sint32(x_1) /\
+ is_sint32(Msint32_0[a_6]) /\ is_sint32(x_3) /\ is_sint32(x_5) /\
+ is_sint32(x_6) /\ is_sint32(x_8) /\ is_sint32(x_9).
+ (* Heap *)
+ Type: (region(a.base) <= 0) /\ (region(b.base) <= 0).
+ (* Goal *)
+ When: b != a.
+ (* Pre-condition *)
+ Have: P_pointed(a, b).
+ (* Assertion *)
+ Have: m_2[a_6] = x_5.
+}
+Prove: x_9 = x_5.
+
+------------------------------------------------------------
+
+Goal Post-condition (file array.c, line 13) in 'add_first4':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Post-condition (file array.c, line 14) in 'add_first4':
+Let a_1 = shiftfield_F1_S_content(a).
+Let a_2 = shift_sint32(a_1, 0).
+Let x = Msint32_0[a_2].
+Let a_3 = shiftfield_F1_S_content(b).
+Let x_1 = Msint32_0[shift_sint32(a_3, 0)].
+Let m = Msint32_0[a_2 <- x + x_1].
+Let a_4 = shift_sint32(a_1, 1).
+Let x_2 = Msint32_0[a_4].
+Let x_3 = m[shift_sint32(a_3, 1)].
+Let m_1 = m[a_4 <- x_2 + x_3].
+Let a_5 = shift_sint32(a_3, 2).
+Let x_4 = m_1[a_5].
+Let a_6 = shift_sint32(a_1, 2).
+Let x_5 = Msint32_0[a_6].
+Let x_6 = x_5 + x_4.
+Let m_2 = m_1[a_6 <- x_6].
+Let x_7 = m_2[a_5].
+Let a_7 = shift_sint32(a_1, 3).
+Let x_8 = Msint32_0[a_7].
+Let x_9 = Msint32_0[a_5].
+Let x_10 = m_2[shift_sint32(a_3, 3)].
+Assume {
+ Type: is_sint32(x) /\ is_sint32(x_2) /\ is_sint32(x_5) /\ is_sint32(x_8) /\
+ is_sint32(Msint32_0[shift_sint32(a_1, 4)]) /\ is_sint32(x_1) /\
+ is_sint32(x_9) /\ is_sint32(x_3) /\ is_sint32(x_4) /\ is_sint32(x_6) /\
+ is_sint32(x_7) /\ is_sint32(x_10) /\
+ is_sint32(m_2[a_7 <- x_8 + x_10][a_5]).
+ (* Heap *)
+ Type: (region(a.base) <= 0) /\ (region(b.base) <= 0).
+ (* Pre-condition *)
+ Have: P_pointed(a, b).
+ (* Assertion *)
+ Have: ((b != a) -> (x_7 = x_4)).
+ (* Assertion *)
+ Have: ((b = a) -> (x_4 = x_5)).
+}
+Prove: x_4 = x_9.
+
+------------------------------------------------------------
+
+Goal Post-condition (file array.c, line 15) in 'add_first4':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assertion (file array.c, line 23):
+Let a_1 = shiftfield_F1_S_content(a).
+Let a_2 = shift_sint32(a_1, 0).
+Let x = Msint32_0[a_2].
+Let a_3 = shift_sint32(a_1, 1).
+Let x_1 = Msint32_0[a_3].
+Let a_4 = shift_sint32(a_1, 2).
+Let x_2 = Msint32_0[a_4].
+Let a_5 = shiftfield_F1_S_content(b).
+Let x_3 = Msint32_0[shift_sint32(a_5, 0)].
+Let a_6 = shift_sint32(a_5, 2).
+Let m = Msint32_0[a_2 <- x + x_3].
+Let x_4 = m[shift_sint32(a_5, 1)].
+Let m_1 = m[a_3 <- x_1 + x_4].
+Let x_5 = m_1[a_6].
+Let x_6 = x_2 + x_5.
+Let m_2 = m_1[a_4 <- x_6].
+Let x_7 = m_2[a_6].
+Assume {
+ Type: is_sint32(x) /\ is_sint32(x_1) /\ is_sint32(x_2) /\
+ is_sint32(Msint32_0[shift_sint32(a_1, 3)]) /\
+ is_sint32(Msint32_0[shift_sint32(a_1, 4)]) /\ is_sint32(x_3) /\
+ is_sint32(Msint32_0[a_6]) /\ is_sint32(x_4) /\ is_sint32(x_5) /\
+ is_sint32(x_6) /\ is_sint32(x_7) /\
+ is_sint32(m_2[shift_sint32(a_5, 3)]).
+ (* Heap *)
+ Type: (region(a.base) <= 0) /\ (region(b.base) <= 0).
+ (* Goal *)
+ When: b != a.
+ (* Pre-condition *)
+ Have: P_pointed(a, b).
+}
+Prove: x_7 = x_5.
+
+------------------------------------------------------------
+
+Goal Assertion (file array.c, line 24):
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle/copy_array.res.oracle b/src/plugins/wp/tests/wp_region/oracle/copy_array.res.oracle
new file mode 100644
index 00000000000..b50ed95f5a1
--- /dev/null
+++ b/src/plugins/wp/tests/wp_region/oracle/copy_array.res.oracle
@@ -0,0 +1,501 @@
+# frama-c -wp -wp-model 'Region' [...]
+[kernel] Parsing copy_array.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal copy_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal copy_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+------------------------------------------------------------
+ Function copy
+------------------------------------------------------------
+
+Goal Post-condition (file copy_array.c, line 4) in 'copy':
+Let a_1 = shift_sint32(a, 0).
+Let a_2 = havoc(Msint32_undef_0, Msint32_0, a_1, n).
+Let x = 4 * n.
+Let a_3 = havoc(Msint32_undef_0, Msint32_0, a_1, i).
+Assume {
+ Type: is_sint32(i) /\ is_sint32(n).
+ (* Heap *)
+ Type: (region(a.base) <= 0) /\ (region(b.base) <= 0).
+ (* Goal *)
+ When: (0 <= i_1) /\ (i_1 < n).
+ (* Pre-condition *)
+ Have: separated(a_1, x, shift_sint32(b, 0), x).
+ (* Invariant 'Range' *)
+ Have: 0 <= n.
+ (* Invariant 'Range' *)
+ Have: (0 <= i) /\ (i <= n).
+ (* Invariant 'Copy' *)
+ Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+ (a_2[shift_sint32(b, i_2)] = a_2[shift_sint32(a, i_2)]))).
+ (* Else *)
+ Have: n <= i.
+}
+Prove: a_3[shift_sint32(b, i_1)] = a_3[shift_sint32(a, i_1)].
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'Copy' (file copy_array.c, line 11):
+Let a_1 = shift_sint32(a, 0).
+Let a_2 = havoc(Msint32_undef_0, Msint32_0, a_1, n).
+Let a_3 = a_2[shift_sint32(a, i) <- a_2[shift_sint32(b, i)]].
+Let x = 4 * n.
+Assume {
+ Type: is_sint32(i) /\ is_sint32(n) /\ is_sint32(1 + i).
+ (* Heap *)
+ Type: (region(a.base) <= 0) /\ (region(b.base) <= 0).
+ (* Goal *)
+ When: (i_1 <= i) /\ (0 <= i_1).
+ (* Pre-condition *)
+ Have: separated(a_1, x, shift_sint32(b, 0), x).
+ (* Invariant 'Range' *)
+ Have: 0 <= n.
+ (* Invariant 'Range' *)
+ Have: (0 <= i) /\ (i <= n).
+ (* Invariant 'Copy' *)
+ Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+ (a_2[shift_sint32(b, i_2)] = a_2[shift_sint32(a, i_2)]))).
+ (* Then *)
+ Have: i < n.
+ (* Assertion 'A' *)
+ Have: forall i_2 : Z. let a_4 = shift_sint32(a, i_2) in ((0 <= i_2) ->
+ ((i_2 < i) -> (a_3[a_4] = a_2[a_4]))).
+ (* Assertion 'B' *)
+ Have: forall i_2 : Z. let a_4 = shift_sint32(b, i_2) in ((0 <= i_2) ->
+ ((i_2 < i) -> (a_3[a_4] = a_2[a_4]))).
+ (* Invariant 'Range' *)
+ Have: (-1) <= i.
+}
+Prove: a_3[shift_sint32(b, i_1)] = a_3[shift_sint32(a, i_1)].
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'Copy' (file copy_array.c, line 11):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant 'Range' (file copy_array.c, line 10):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant 'Range' (file copy_array.c, line 10):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assertion 'A' (file copy_array.c, line 18):
+Let a_1 = shift_sint32(a, 0).
+Let a_2 = havoc(Msint32_undef_0, Msint32_0, a_1, n).
+Let x = 4 * n.
+Let a_3 = shift_sint32(a, i_1).
+Assume {
+ Type: is_sint32(i) /\ is_sint32(n).
+ (* Heap *)
+ Type: (region(a.base) <= 0) /\ (region(b.base) <= 0).
+ (* Goal *)
+ When: (0 <= i_1) /\ (i_1 < i).
+ (* Pre-condition *)
+ Have: separated(a_1, x, shift_sint32(b, 0), x).
+ (* Invariant 'Range' *)
+ Have: 0 <= n.
+ (* Invariant 'Range' *)
+ Have: (0 <= i) /\ (i <= n).
+ (* Invariant 'Copy' *)
+ Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+ (a_2[shift_sint32(b, i_2)] = a_2[shift_sint32(a, i_2)]))).
+ (* Then *)
+ Have: i < n.
+}
+Prove: a_2[shift_sint32(a, i) <- a_2[shift_sint32(b, i)]][a_3] = a_2[a_3].
+
+------------------------------------------------------------
+
+Goal Assertion 'B' (file copy_array.c, line 19):
+Let a_1 = shift_sint32(a, 0).
+Let a_2 = havoc(Msint32_undef_0, Msint32_0, a_1, n).
+Let a_3 = a_2[shift_sint32(a, i) <- a_2[shift_sint32(b, i)]].
+Let x = 4 * n.
+Let a_4 = shift_sint32(b, i_1).
+Assume {
+ Type: is_sint32(i) /\ is_sint32(n).
+ (* Heap *)
+ Type: (region(a.base) <= 0) /\ (region(b.base) <= 0).
+ (* Goal *)
+ When: (0 <= i_1) /\ (i_1 < i).
+ (* Pre-condition *)
+ Have: separated(a_1, x, shift_sint32(b, 0), x).
+ (* Invariant 'Range' *)
+ Have: 0 <= n.
+ (* Invariant 'Range' *)
+ Have: (0 <= i) /\ (i <= n).
+ (* Invariant 'Copy' *)
+ Have: forall i_2 : Z. ((0 <= i_2) -> ((i_2 < i) ->
+ (a_2[shift_sint32(b, i_2)] = a_2[shift_sint32(a, i_2)]))).
+ (* Then *)
+ Have: i < n.
+ (* Assertion 'A' *)
+ Have: forall i_2 : Z. let a_5 = shift_sint32(a, i_2) in ((0 <= i_2) ->
+ ((i_2 < i) -> (a_3[a_5] = a_2[a_5]))).
+}
+Prove: a_3[a_4] = a_2[a_4].
+
+------------------------------------------------------------
+
+Goal Loop assigns (file copy_array.c, line 12) (1/3):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file copy_array.c, line 12) (2/3):
+Effect at line 15
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file copy_array.c, line 12) (3/3):
+Effect at line 17
+Let a_1 = shift_sint32(a, 0).
+Let a_2 = havoc(Msint32_undef_0, Msint32_0, a_1, n).
+Let x = i - 1.
+Let a_3 = shift_sint32(a, x).
+Let a_4 = a_2[a_3 <- a_2[shift_sint32(b, x)]].
+Let x_1 = 4 * n.
+Assume {
+ Type: is_sint32(i) /\ is_sint32(n) /\ is_sint32(x).
+ (* Heap *)
+ Type: (region(a.base) <= 0) /\ (region(b.base) <= 0) /\ linked(alloc_0).
+ (* Goal *)
+ When: !invalid(alloc_0[P_a_24 <- 8][P_b_25 <- 8], a_3, 4).
+ (* Pre-condition *)
+ Have: separated(a_1, x_1, shift_sint32(b, 0), x_1).
+ (* Invariant 'Range' *)
+ Have: 0 <= n.
+ (* Invariant 'Range' *)
+ Have: (0 < i) /\ (i <= (1 + n)).
+ (* Invariant 'Copy' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> (((2 + i_1) <= i) ->
+ (a_2[shift_sint32(b, i_1)] = a_2[shift_sint32(a, i_1)]))).
+ (* Then *)
+ Have: i <= n.
+ (* Assertion 'A' *)
+ Have: forall i_1 : Z. let a_5 = shift_sint32(a, i_1) in ((0 <= i_1) ->
+ (((2 + i_1) <= i) -> (a_4[a_5] = a_2[a_5]))).
+ (* Assertion 'B' *)
+ Have: forall i_1 : Z. let a_5 = shift_sint32(b, i_1) in ((0 <= i_1) ->
+ (((2 + i_1) <= i) -> (a_4[a_5] = a_2[a_5]))).
+ (* Invariant 'Copy' *)
+ Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < i) ->
+ (a_4[shift_sint32(b, i_1)] = a_4[shift_sint32(a, i_1)]))).
+}
+Prove: included(a_3, 4, a_1, x_1).
+
+------------------------------------------------------------
+
+Goal Assigns (file copy_array.c, line 5) in 'copy':
+Effect at line 15
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Decreasing of Loop variant at loop (file copy_array.c, line 15):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Positivity of Loop variant at loop (file copy_array.c, line 15):
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle/union.res.oracle b/src/plugins/wp/tests/wp_region/oracle/union.res.oracle
new file mode 100644
index 00000000000..87cfc66c455
--- /dev/null
+++ b/src/plugins/wp/tests/wp_region/oracle/union.res.oracle
@@ -0,0 +1,114 @@
+# frama-c -wp -wp-model 'Region' [...]
+[kernel] Parsing union.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal f_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal f_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+------------------------------------------------------------
+ Function f
+------------------------------------------------------------
+
+Goal Post-condition (file union.i, line 8) in 'f':
+Let a = shiftfield_F1_U_i(p).
+Let a_1 = shiftfield_F1_U_s(p).
+Let m = write_sint16(write_sint16(write_sint32(mem_0, a, 42),
+ shift_sint16(a_1, 0), -1), shift_sint16(a_1, 1), -1).
+Let x = read_sint32(write_sint32(m, a, 0), a).
+Assume {
+ Type: is_sint32(x).
+ (* Heap *)
+ Type: (region(p.base) <= 0) /\ framed(mem_0) /\ sconst(mem_0).
+ (* Assertion *)
+ Have: read_sint32(m, a) = (-1).
+}
+Prove: x = 0.
+
+------------------------------------------------------------
+
+Goal Assertion (file union.i, line 14):
+Let a = shiftfield_F1_U_i(p).
+Let a_1 = shiftfield_F1_U_s(p).
+Let x = read_sint32(write_sint16(write_sint16(write_sint32(mem_0, a, 42),
+ shift_sint16(a_1, 0), -1),
+ shift_sint16(a_1, 1), -1), a).
+Assume {
+ Type: is_sint32(x).
+ (* Heap *)
+ Type: (region(p.base) <= 0) /\ framed(mem_0) /\ sconst(mem_0).
+}
+Prove: x = (-1).
+
+------------------------------------------------------------
+
+Goal Assigns (file union.i, line 7) in 'f' (1/4):
+Effect at line 11
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file union.i, line 7) in 'f' (2/4):
+Effect at line 12
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file union.i, line 7) in 'f' (3/4):
+Effect at line 13
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file union.i, line 7) in 'f' (4/4):
+Effect at line 15
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/array.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/array.res.oracle
new file mode 100644
index 00000000000..132cfb8a7b3
--- /dev/null
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/array.res.oracle
@@ -0,0 +1,384 @@
+# frama-c -wp -wp-model 'Region' [...]
+[kernel] Parsing array.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal add_first4_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal add_first4_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[region] array.c:23: Warning: Annotations not analyzed
+[region] array.c:24: Warning: Annotations not analyzed
+[wp] 6 goals scheduled
+[wp] [Valid] region_add_first4_ensures (Alt-Ergo) (Cached)
+[wp] [Valid] region_add_first4_ensures_2 (Qed)
+[wp] [Valid] region_add_first4_ensures_3 (Alt-Ergo) (Cached)
+[wp] [Valid] region_add_first4_ensures_4 (Qed)
+[wp] [Valid] region_add_first4_assert (Alt-Ergo) (Cached)
+[wp] [Valid] region_add_first4_assert_2 (Qed)
+[wp] Proved goals: 8 / 8
+ Terminating: 1
+ Unreachable: 1
+ Qed: 3
+ Alt-Ergo: 3
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ add_first4 3 3 6 100%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/copy_array.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/copy_array.res.oracle
new file mode 100644
index 00000000000..7071946431d
--- /dev/null
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/copy_array.res.oracle
@@ -0,0 +1,320 @@
+# frama-c -wp -wp-model 'Region' [...]
+[kernel] Parsing copy_array.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal copy_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal copy_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[region] copy_array.c:15: Warning: Annotations not analyzed
+[region] copy_array.c:18: Warning: Annotations not analyzed
+[region] copy_array.c:19: Warning: Annotations not analyzed
+[wp] 13 goals scheduled
+[wp] [Valid] region_copy_ensures (Alt-Ergo) (Cached)
+[wp] [Valid] region_copy_loop_invariant_Copy_preserved (Alt-Ergo) (Cached)
+[wp] [Valid] region_copy_loop_invariant_Copy_established (Qed)
+[wp] [Valid] region_copy_loop_invariant_Range_preserved (Qed)
+[wp] [Valid] region_copy_loop_invariant_Range_established (Qed)
+[wp] [Valid] region_copy_assert_A (Alt-Ergo) (Cached)
+[wp] [Valid] region_copy_assert_B (Alt-Ergo) (Cached)
+[wp] [Valid] region_copy_loop_assigns_part1 (Qed)
+[wp] [Valid] region_copy_loop_assigns_part2 (Qed)
+[wp] [Valid] region_copy_loop_assigns_part3 (Alt-Ergo) (Cached)
+[wp] [Valid] region_copy_assigns (Qed)
+[wp] [Valid] region_copy_loop_variant_decrease (Qed)
+[wp] [Valid] region_copy_loop_variant_positive (Qed)
+[wp] Proved goals: 15 / 15
+ Terminating: 1
+ Unreachable: 1
+ Qed: 8
+ Alt-Ergo: 5
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ copy 8 5 13 100%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/oracle_qualif/union.res.oracle b/src/plugins/wp/tests/wp_region/oracle_qualif/union.res.oracle
new file mode 100644
index 00000000000..40300a0021d
--- /dev/null
+++ b/src/plugins/wp/tests/wp_region/oracle_qualif/union.res.oracle
@@ -0,0 +1,71 @@
+# frama-c -wp -wp-model 'Region' [...]
+[kernel] Parsing union.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal f_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal f_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[region] union.i:14: Warning: Annotations not analyzed
+[wp] 6 goals scheduled
+[wp] [Valid] region_f_ensures (Alt-Ergo) (Cached)
+[wp] [Valid] region_f_assert (Alt-Ergo) (Cached)
+[wp] [Valid] region_f_assigns_part1 (Qed)
+[wp] [Valid] region_f_assigns_part2 (Qed)
+[wp] [Valid] region_f_assigns_part3 (Qed)
+[wp] [Valid] region_f_assigns_part4 (Qed)
+[wp] Proved goals: 8 / 8
+ Terminating: 1
+ Unreachable: 1
+ Qed: 4
+ Alt-Ergo: 2
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ f 4 2 6 100%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_region/union.i b/src/plugins/wp/tests/wp_region/union.i
new file mode 100644
index 00000000000..edc24141817
--- /dev/null
+++ b/src/plugins/wp/tests/wp_region/union.i
@@ -0,0 +1,16 @@
+union U {
+ short s[2];
+ int i;
+};
+
+/*@
+ assigns *p;
+ ensures p->i == 0;
+@*/
+void f (union U *p) {
+ p->i = 42;
+ p->s[0] = -1;
+ p->s[1] = -1;
+ //@ assert p->i == -1;
+ (p->i)++;
+}
--
GitLab