[wp] Adds a test for nullable context pointers

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

+/* run.config
+   OPT: -wp-model Caveat
+*/
+/* run.config_qualif
+   OPT: -wp-model Caveat
+*/
+
+int x ;
+int *g ;
+
+/*@ assigns *g, *p, x ; */
+void nullable_coherence(int* p /*@ nullable */){
+  if(p == (void*)0){
+    //@ check must_fail: \false ;
+    return;
+  }
+  //@ check \valid(p);
+  *p = 42;
+  *g = 24;
+  x = 1;
+}
+
+//@ assigns *p, *q, *r, *s, *t ;
+void nullable_in_context
+(int* p /*@ nullable */,
+ int* q /*@ nullable */,
+ int* r /*@ nullable */,
+ int* s, int* t)
+{
+  *p = 42;
+  *q = 42;
+  *r = 42;
+  *s = *t = 0;
+}

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

+# frama-c -wp -wp-model 'Typed (Caveat)' [...]
+[kernel] Parsing tests/wp_plugin/nullable.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: In Caveat mode, with nullable variables,-wp-rte should be explicitly positioned
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+  Function nullable_coherence
+------------------------------------------------------------
+
+Goal Check 'must_fail' (file tests/wp_plugin/nullable.i, line 14):
+Assume { (* Then *) Have: G_p_24 = 0. }
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Check (file tests/wp_plugin/nullable.i, line 17):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/nullable.i, line 11) in 'nullable_coherence':
+Prove: true.
+
+------------------------------------------------------------
+------------------------------------------------------------
+  Function nullable_in_context
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/nullable.i, line 23) in 'nullable_in_context' (1/2):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/nullable.i, line 23) in 'nullable_in_context' (2/2):
+Effect at line 33
+Prove: true.
+
+------------------------------------------------------------
+[wp] tests/wp_plugin/nullable.i:12: Warning: 
+  Memory model hypotheses for function 'nullable_coherence':
+  /*@
+     behavior wp_typed_caveat:
+       requires \separated(g, &x);
+       requires \separated(p, &x);
+       requires \valid(g);
+       requires p ≢ \null ⇒ \separated(g, p, &x);
+       requires \valid(p) ∨ p ≡ \null;
+     */
+  void nullable_coherence(int *p /*@ nullable */);
+[wp] tests/wp_plugin/nullable.i:24: Warning: 
+  Memory model hypotheses for function 'nullable_in_context':
+  /*@
+     behavior wp_typed_caveat:
+       requires \valid(s);
+       requires \valid(t);
+       requires p ≢ \null ⇒ \separated(p, s, t);
+       requires p ≢ \null ⇒ \separated(p, q) ∧ \separated(p, r);
+       requires q ≢ \null ⇒ \separated(q, s, t);
+       requires q ≢ \null ⇒ \separated(q, r) ∧ \separated(q, p);
+       requires r ≢ \null ⇒ \separated(r, s, t);
+       requires r ≢ \null ⇒ \separated(r, q) ∧ \separated(r, p);
+       requires \valid(p) ∨ p ≡ \null;
+       requires \valid(q) ∨ q ≡ \null;
+       requires \valid(r) ∨ r ≡ \null;
+     */
+  void nullable_in_context(int *p /*@ nullable */, int *q /*@ nullable */,
+                           int *r /*@ nullable */, int *s, int *t);

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

+# frama-c -wp -wp-model 'Typed (Caveat)' [...]
+[kernel] Parsing tests/wp_plugin/nullable.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Warning: In Caveat mode, with nullable variables,-wp-rte should be explicitly positioned
+[wp] Warning: Missing RTE guards
+[wp] 5 goals scheduled
+[wp] [Alt-Ergo] Goal typed_caveat_nullable_coherence_check_must_fail : Unsuccess
+[wp] [Qed] Goal typed_caveat_nullable_coherence_check : Valid
+[wp] [Qed] Goal typed_caveat_nullable_coherence_assigns : Valid
+[wp] [Qed] Goal typed_caveat_nullable_in_context_assigns_part1 : Valid
+[wp] [Qed] Goal typed_caveat_nullable_in_context_assigns_part2 : Valid
+[wp] Proved goals:    4 / 5
+  Qed:             4 
+  Alt-Ergo:        0  (unsuccess: 1)
+------------------------------------------------------------
+ Functions                 WP     Alt-Ergo  Total   Success
+  nullable_coherence        2        -        3      66.7%
+  nullable_in_context       2        -        2       100%
+------------------------------------------------------------
+[wp] tests/wp_plugin/nullable.i:12: Warning: 
+  Memory model hypotheses for function 'nullable_coherence':
+  /*@
+     behavior wp_typed_caveat:
+       requires \separated(g, &x);
+       requires \separated(p, &x);
+       requires \valid(g);
+       requires p ≢ \null ⇒ \separated(g, p, &x);
+       requires \valid(p) ∨ p ≡ \null;
+     */
+  void nullable_coherence(int *p /*@ nullable */);
+[wp] tests/wp_plugin/nullable.i:24: Warning: 
+  Memory model hypotheses for function 'nullable_in_context':
+  /*@
+     behavior wp_typed_caveat:
+       requires \valid(s);
+       requires \valid(t);
+       requires p ≢ \null ⇒ \separated(p, s, t);
+       requires p ≢ \null ⇒ \separated(p, q) ∧ \separated(p, r);
+       requires q ≢ \null ⇒ \separated(q, s, t);
+       requires q ≢ \null ⇒ \separated(q, r) ∧ \separated(q, p);
+       requires r ≢ \null ⇒ \separated(r, s, t);
+       requires r ≢ \null ⇒ \separated(r, q) ∧ \separated(r, p);
+       requires \valid(p) ∨ p ≡ \null;
+       requires \valid(q) ∨ q ≡ \null;
+       requires \valid(r) ∨ r ≡ \null;
+     */
+  void nullable_in_context(int *p /*@ nullable */, int *q /*@ nullable */,
+                           int *r /*@ nullable */, int *s, int *t);