[wp/region] test + oracles

src/plugins/wp/tests/wp_region/affectations.c

+/*@ predicate pointed(int *p, int* q) = p==q || \separated(p,q);
+*/
+
+/*@
+  requires \valid(p);
+  requires \valid(q);
+  requires pointed(p,q);
+  assigns  *p, *q;
+  region   PQ: *p, *q;
+  behavior EQ:
+    assumes  p == q;
+    ensures  P: *p == \old(*p);
+    ensures  Q: *q == \old(*q);
+  behavior SEP:
+    assumes  p != q;
+    ensures  Q: *p == \old(*p)+1;
+    ensures  Q: *q == \old(*q)-1;
+*/
+void f(int* p, int* q) {
+  (*p)++;
+  (*q)--;
+}

src/plugins/wp/tests/wp_region/heterogenous_cast.c

+/*@
+    assigns *p;
+@*/
+void g (int *p) {
+  *p = 42;
+  short *q = (short*) p;
+  q[0] = -1;
+  q[1] = -1;
+  //@ assert *p == -1;
+}

src/plugins/wp/tests/wp_region/oracle/affectations.res.oracle

+# frama-c -wp -wp-model 'Region' [...]
+[kernel] Parsing affectations.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal f_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal f_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+  Function f
+------------------------------------------------------------
+
+Goal Assigns (file affectations.c, line 8) in 'f' (1/2):
+Effect at line 20
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file affectations.c, line 8) in 'f' (2/2):
+Effect at line 21
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function f with behavior EQ
+------------------------------------------------------------
+
+Goal Post-condition for 'EQ' 'P' in 'f':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Post-condition for 'EQ' 'Q' in 'f':
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function f with behavior SEP
+------------------------------------------------------------
+
+Goal Post-condition for 'SEP' 'Q' in 'f':
+Let x = Msint32_0[p].
+Let x_1 = 1 + x.
+Let m = Msint32_0[p <- x_1].
+Let x_2 = m[q].
+Let x_3 = x_2 - 1.
+Let x_4 = m[q <- x_3][p].
+Assume {
+  Type: is_sint32(x) /\ is_sint32(Msint32_0[q]) /\ is_sint32(x_2) /\
+      is_sint32(x_3) /\ is_sint32(x_4).
+  (* Heap *)
+  Type: (region(p.base) <= 0) /\ (region(q.base) <= 0) /\ linked(alloc_0).
+  (* Pre-condition *)
+  Have: valid_rw(alloc_0, p, 4).
+  (* Pre-condition *)
+  Have: valid_rw(alloc_0, q, 4).
+  (* Pre-condition *)
+  Have: P_pointed(p, q).
+  (* Pre-condition for 'SEP' *)
+  Have: q != p.
+}
+Prove: x_4 = x_1.
+
+------------------------------------------------------------
+
+Goal Post-condition for 'SEP' 'Q' in 'f':
+Let x = Msint32_0[p].
+Let x_1 = Msint32_0[q].
+Let m = Msint32_0[p <- 1 + x].
+Let x_2 = m[q].
+Let x_3 = x_2 - 1.
+Assume {
+  Type: is_sint32(x) /\ is_sint32(x_1) /\ is_sint32(x_2) /\ is_sint32(x_3) /\
+      is_sint32(m[q <- x_3][p]).
+  (* Heap *)
+  Type: (region(p.base) <= 0) /\ (region(q.base) <= 0) /\ linked(alloc_0).
+  (* Pre-condition *)
+  Have: valid_rw(alloc_0, p, 4).
+  (* Pre-condition *)
+  Have: valid_rw(alloc_0, q, 4).
+  (* Pre-condition *)
+  Have: P_pointed(p, q).
+  (* Pre-condition for 'SEP' *)
+  Have: q != p.
+}
+Prove: x_2 = x_1.
+
+------------------------------------------------------------

src/plugins/wp/tests/wp_region/oracle/heterogenous_cast.res.oracle

+# frama-c -wp -wp-model 'Region' [...]
+[kernel] Parsing heterogenous_cast.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal g_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal g_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+------------------------------------------------------------
+  Function g
+------------------------------------------------------------
+
+Goal Assertion (file heterogenous_cast.c, line 9):
+Let x = read_sint32(write_sint16(write_sint16(write_sint32(mem_0, p, 42),
+                                   shift_sint16(p, 0), -1),
+                      shift_sint16(p, 1), -1), p).
+Assume {
+  Type: is_sint32(x).
+  (* Heap *)
+  Type: (region(p.base) <= 0) /\ framed(mem_0) /\ sconst(mem_0).
+}
+Prove: x = (-1).
+
+------------------------------------------------------------
+
+Goal Assigns (file heterogenous_cast.c, line 2) in 'g' (1/3):
+Effect at line 5
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file heterogenous_cast.c, line 2) in 'g' (2/3):
+Effect at line 7
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file heterogenous_cast.c, line 2) in 'g' (3/3):
+Effect at line 8
+Prove: true.
+
+------------------------------------------------------------

src/plugins/wp/tests/wp_region/oracle_qualif/affectations.res.oracle

+# frama-c -wp -wp-model 'Region' [...]
+[kernel] Parsing affectations.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal f_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal f_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+[wp] 6 goals scheduled
+[wp] [Valid] region_f_assigns_part1 (Qed)
+[wp] [Valid] region_f_assigns_part2 (Qed)
+[wp] [Valid] region_f_EQ_ensures_P (Qed)
+[wp] [Valid] region_f_EQ_ensures_Q (Qed)
+[wp] [Valid] region_f_SEP_ensures_Q (Alt-Ergo) (Cached)
+[wp] [Valid] region_f_SEP_ensures_Q_2 (Alt-Ergo) (Cached)
+[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%
+------------------------------------------------------------

src/plugins/wp/tests/wp_region/oracle_qualif/heterogenous_cast.res.oracle

+# frama-c -wp -wp-model 'Region' [...]
+[kernel] Parsing heterogenous_cast.c (with preprocessing)
+[wp] Running WP plugin...
+[wp] [Valid] Goal g_exits (Cfg) (Unreachable)
+[wp] [Valid] Goal g_terminates (Cfg) (Trivial)
+[wp] Warning: Missing RTE guards
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[region] heterogenous_cast.c:9: Warning: Annotations not analyzed
+[wp] 4 goals scheduled
+[wp] [Valid] region_g_assert (Alt-Ergo) (Cached)
+[wp] [Valid] region_g_assigns_part1 (Qed)
+[wp] [Valid] region_g_assigns_part2 (Qed)
+[wp] [Valid] region_g_assigns_part3 (Qed)
+[wp] Proved goals:    6 / 6
+  Terminating:     1
+  Unreachable:     1
+  Qed:             3
+  Alt-Ergo:        1
+------------------------------------------------------------
+ Functions                 WP     Alt-Ergo  Total   Success
+  g                         3        1        4       100%
+------------------------------------------------------------