[wp] broken tests for post-assigns and post-valid

src/plugins/wp/tests/wp_plugin/oracle/post_assigns.res.oracle

+# frama-c -wp [...]
+[kernel] Parsing tests/wp_plugin/post_assigns.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+  Function receive
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_plugin/post_assigns.i, line 9) in 'receive':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/post_assigns.i, line 10) in 'receive' (1/2):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/post_assigns.i, line 10) in 'receive' (2/2):
+Call Effect at line 14
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/post_assigns.i, line 10) in 'receive' (1/2):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/post_assigns.i, line 10) in 'receive' (2/2):
+Call Effect at line 14
+Assume {
+  Have: 0 <= size_0.
+  Type: is_sint32(size_1) /\ is_sint32(size_0).
+  (* Heap *)
+  Type: (region(message_0.base) <= 0) /\ linked(Malloc_0).
+  (* Goal *)
+  When: !invalid(Malloc_0, shift_sint8(message_0, 0), 1 + size_0).
+}
+Prove: size_0 <= size_1.
+
+------------------------------------------------------------
+[wp] Warning: Memory model hypotheses for function 'receive':
+  /*@ behavior typed: requires \separated(&size,message+(..)); */
+  void receive(int n, char *message);

src/plugins/wp/tests/wp_plugin/oracle/post_valid.res.oracle

+# frama-c -wp [...]
+[kernel] Parsing tests/wp_plugin/post_valid.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+  Function job
+------------------------------------------------------------
+
+Goal Post-condition 'LOCAL' in 'job':
+Assume { (* Heap *) Type: linked(Malloc_0). }
+Prove: !valid_rw(Malloc_0[P_formal_26 <- 1][L_local_28 <- 0][P_formal_26
+                   <- 0], global(L_local_28), 1).
+
+------------------------------------------------------------
+
+Goal Post-condition 'FORMAL' in 'job':
+Assume { (* Heap *) Type: linked(Malloc_0). }
+Prove: valid_rw(Malloc_0[P_formal_26 <- 1][L_local_28 <- 0][P_formal_26 <- 0],
+         global(P_formal_26), 1).
+
+------------------------------------------------------------
+
+Goal Post-condition 'GLOBAL' in 'job':
+Assume { (* Heap *) Type: linked(Malloc_0). }
+Prove: valid_rw(Malloc_0[P_formal_26 <- 1][L_local_28 <- 0][P_formal_26 <- 0],
+         global(G_global_20), 1).
+
+------------------------------------------------------------

src/plugins/wp/tests/wp_plugin/oracle_qualif/post_assigns.res.oracle

+# frama-c -wp [...]
+[kernel] Parsing tests/wp_plugin/post_assigns.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[wp] 5 goals scheduled
+[wp] [Qed] Goal typed_receive_ensures : Valid
+[wp] [Qed] Goal typed_receive_assigns_exit_part1 : Valid
+[wp] [Qed] Goal typed_receive_assigns_exit_part2 : Valid
+[wp] [Qed] Goal typed_receive_assigns_normal_part1 : Valid
+[wp] [Alt-Ergo] Goal typed_receive_assigns_normal_part2 : Unsuccess
+[wp] Proved goals:    4 / 5
+  Qed:             4 
+  Alt-Ergo:        0  (unsuccess: 1)
+------------------------------------------------------------
+ Functions                 WP     Alt-Ergo  Total   Success
+  receive                   4        -        5      80.0%
+------------------------------------------------------------
+[wp] Warning: Memory model hypotheses for function 'receive':
+  /*@ behavior typed: requires \separated(&size,message+(..)); */
+  void receive(int n, char *message);

src/plugins/wp/tests/wp_plugin/oracle_qualif/post_valid.res.oracle

+# frama-c -wp [...]
+[kernel] Parsing tests/wp_plugin/post_valid.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[wp] 3 goals scheduled
+[wp] [Alt-Ergo] Goal typed_job_ensures_LOCAL : Valid
+[wp] [Alt-Ergo] Goal typed_job_ensures_FORMAL : Unsuccess
+[wp] [Alt-Ergo] Goal typed_job_ensures_GLOBAL : Valid
+[wp] Proved goals:    2 / 3
+  Qed:             0 
+  Alt-Ergo:        2  (unsuccess: 1)
+------------------------------------------------------------
+ Functions                 WP     Alt-Ergo  Total   Success
+  job                       -        2        3      66.7%
+------------------------------------------------------------

src/plugins/wp/tests/wp_plugin/post_assigns.i

+/*@
+  assigns *(message + (0 .. n));
+*/
+extern void write(char *message, int n);
+
+int size;
+
+/*@
+  ensures size == n;
+  assigns size, message[ 0 .. \at(size,Post) ]; // FAILS
+*/
+void receive(int n,char *message) {
+  size = n ;
+  write(message, size);
+}

src/plugins/wp/tests/wp_plugin/post_valid.i

+int global;
+
+int *p_global, *p_local, *p_formal ;
+
+/*@
+  ensures LOCAL: !\valid(p_local);
+  ensures FORMAL: \valid(p_formal); // FAILS
+  ensures GLOBAL: \valid(p_global);
+*/
+void job(int formal) {
+  int local = formal;
+  p_local = &local;
+  p_global = &global;
+  p_formal = &formal;
+}