[WP] added tests with incomplete consolidation

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

@@ -6,10 +6,10 @@
    OPT: -wp-dynamic -wp
 */
 //-----------------------------------------------------------------------------
-/*@ 
+/*@
   requires -10<=x<=10;
-  ensures \result == x+1; 
-  assigns \nothing; 
+  ensures \result == x+1;
+  assigns \nothing;
 */
 int f1(int x);
 
@@ -22,7 +22,7 @@ typedef struct S {
 } ;
 
 /*@
-  requires (closure->f == &f1 && \abs(closure->param)<=5) || closure->f == &f2 ; 
+  requires (closure->f == &f1 && \abs(closure->param)<=5) || closure->f == &f2 ;
   ensures \abs(\result - closure->param) <= 1 ;
  */
 int call(struct S * closure) {
@@ -78,6 +78,15 @@ int some_behaviors (int (*p)(void)) {
   return (*p)();
 }
 
+/*@
+  ensures X1==1;
+  assigns X1 ;
+*/
+int missing_context (int (*p)(void)) {
+  //@ calls h1 ;
+  return (*p)();
+}
+
 //-----------------------------------------------------------------------------
 //@ requires \false; ensures \false; exits \false; assigns \nothing;
 int unreachable_g(int x);

src/plugins/wp/tests/wp_plugin/dynamic.i.0.report.json

-{ "wp:global": { "alt-ergo": { "total": 3, "valid": 3, "rank": 16 },
-                 "qed": { "total": 43, "valid": 43 },
-                 "wp:main": { "total": 46, "valid": 46, "rank": 16 } },
+{ "wp:global": { "alt-ergo": { "total": 4, "valid": 3, "unknown": 1,
+                               "rank": 16 },
+                 "qed": { "total": 47, "valid": 47 },
+                 "wp:main": { "total": 51, "valid": 50, "unknown": 1,
+                              "rank": 16 } },
   "wp:functions": { "call": { "specialization_f1_pre_at_call_stmt_3": 
                                 { "alt-ergo": { "total": 1, "valid": 1,
                                                 "rank": 16 },
@@ -104,7 +106,32 @@
                                                                  "valid": 24 },
                                                         "wp:main": { "total": 24,
                                                                     "valid": 24 } } },
-                    "no_call": { "specialization_unreachable_g_pre_at_no_call_stmt_27": 
+                    "missing_context": { "missing_context_stmt_calls_h1": 
+                                           { "alt-ergo": { "total": 1,
+                                                           "unknown": 1 },
+                                             "wp:main": { "total": 1,
+                                                          "unknown": 1 } },
+                                         "missing_context_assign": { "qed": 
+                                                                    { "total": 3,
+                                                                    "valid": 3 },
+                                                                    "wp:main": 
+                                                                    { "total": 3,
+                                                                    "valid": 3 } },
+                                         "missing_context_post": { "qed": 
+                                                                    { "total": 1,
+                                                                    "valid": 1 },
+                                                                   "wp:main": 
+                                                                    { "total": 1,
+                                                                    "valid": 1 } },
+                                         "wp:section": { "alt-ergo": 
+                                                           { "total": 1,
+                                                             "unknown": 1 },
+                                                         "qed": { "total": 4,
+                                                                  "valid": 4 },
+                                                         "wp:main": { "total": 5,
+                                                                    "valid": 4,
+                                                                    "unknown": 1 } } },
+                    "no_call": { "specialization_unreachable_g_pre_at_no_call_stmt_32": 
                                    { "qed": { "total": 1, "valid": 1 },
                                      "wp:main": { "total": 1, "valid": 1 } },
                                  "no_call_stmt_calls_unreachable_g": 

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

@@ -7,8 +7,9 @@
 [wp] tests/wp_plugin/dynamic.i:65: Calls h1 h2
 [wp] tests/wp_plugin/dynamic.i:78: Calls (for bhv1) h1 h2 h0
 [wp] tests/wp_plugin/dynamic.i:78: Calls (for bhv0) h1 h2 h0
-[wp] tests/wp_plugin/dynamic.i:91: Calls unreachable_g
-[wp:calls] Dynamic call(s): 5.
+[wp] tests/wp_plugin/dynamic.i:87: Calls h1
+[wp] tests/wp_plugin/dynamic.i:100: Calls unreachable_g
+[wp:calls] Dynamic call(s): 6.
 [wp] Loading driver 'share/wp.driver'
 [wp] tests/wp_plugin/dynamic.i:78: Warning: 
   Missigns 'calls' clause dedicated to dynamic calls (see WP manual)
@@ -158,28 +159,60 @@ Goal Post-condition (file tests/wp_plugin/dynamic.i, line 39) in 'guarded_call'
 Tags: Call g.
 Prove: true.
 
+------------------------------------------------------------
+------------------------------------------------------------
+  Function missing_context
+------------------------------------------------------------
+
+Goal Calls h1 in 'missing_context' at instruction (file tests/wp_plugin/dynamic.i, line 87):
+Assume { (* Heap *) Have: region(p.base) <= 0. }
+Prove: global(G_h1_57) = p.
+
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_plugin/dynamic.i, line 82) in 'missing_context':
+Tags: Call h1.
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/dynamic.i, line 83) in 'missing_context':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/dynamic.i, line 83) in 'missing_context' (1/2):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns (file tests/wp_plugin/dynamic.i, line 83) in 'missing_context' (2/2):
+Call Result at line 87
+Tags: Call h1.
+Prove: true.
+
 ------------------------------------------------------------
 ------------------------------------------------------------
   Function no_call
 ------------------------------------------------------------
 
-Goal Calls unreachable_g in 'no_call' at instruction (file tests/wp_plugin/dynamic.i, line 91):
+Goal Calls unreachable_g in 'no_call' at instruction (file tests/wp_plugin/dynamic.i, line 100):
 Prove: true.
 
 ------------------------------------------------------------
 
-Goal Post-condition (file tests/wp_plugin/dynamic.i, line 85) in 'no_call' (1/2):
+Goal Post-condition (file tests/wp_plugin/dynamic.i, line 94) in 'no_call' (1/2):
 Prove: true.
 
 ------------------------------------------------------------
 
-Goal Post-condition (file tests/wp_plugin/dynamic.i, line 85) in 'no_call' (2/2):
+Goal Post-condition (file tests/wp_plugin/dynamic.i, line 94) in 'no_call' (2/2):
 Tags: Call unreachable_g.
 Prove: true.
 
 ------------------------------------------------------------
 
-Goal Instance of 'Pre-condition (file tests/wp_plugin/dynamic.i, line 82) in 'unreachable_g'' in 'no_call' at instruction (file tests/wp_plugin/dynamic.i, line 91)
+Goal Instance of 'Pre-condition (file tests/wp_plugin/dynamic.i, line 91) in 'unreachable_g'' in 'no_call' at instruction (file tests/wp_plugin/dynamic.i, line 100)
 :
 Tags: Call unreachable_g.
 Prove: true.
@@ -350,3 +383,6 @@ Prove: true.
 [wp] Warning: Memory model hypotheses for function 'some_behaviors':
   /*@ behavior typed: requires \separated(&X1,p); */
   int some_behaviors(int (*p)(void));
+[wp] Warning: Memory model hypotheses for function 'missing_context':
+  /*@ behavior typed: requires \separated(&X1,p); */
+  int missing_context(int (*p)(void));

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

@@ -5,7 +5,7 @@
 [wp] tests/wp_plugin/dynamic.i:78: Warning: 
   Missigns 'calls' clause dedicated to dynamic calls (see WP manual)
 [wp] Warning: Missing RTE guards
-[wp] 46 goals scheduled
+[wp] 51 goals scheduled
 [wp] [Qed] Goal typed_behavior_stmt_calls_h1_h2_for_bhv1 : Valid
 [wp] [Qed] Goal typed_behavior_bhv1_post_part1 : Valid
 [wp] [Qed] Goal typed_behavior_bhv1_post_part2 : Valid
@@ -24,6 +24,11 @@
 [wp] [Qed] Goal typed_guarded_call_post_part2 : Valid
 [wp] [Qed] Goal typed_guarded_call_post_2_part1 : Valid
 [wp] [Qed] Goal typed_guarded_call_post_2_part2 : Valid
+[wp] [Alt-Ergo] Goal typed_missing_context_stmt_calls_h1 : Unknown
+[wp] [Qed] Goal typed_missing_context_post : Valid
+[wp] [Qed] Goal typed_missing_context_assign_exit : Valid
+[wp] [Qed] Goal typed_missing_context_assign_normal_part1 : Valid
+[wp] [Qed] Goal typed_missing_context_assign_normal_part2 : Valid
 [wp] [Qed] Goal typed_no_call_stmt_calls_unreachable_g : Valid
 [wp] [Qed] Goal typed_no_call_post_part1 : Valid
 [wp] [Qed] Goal typed_no_call_post_part2 : Valid
@@ -52,9 +57,9 @@
 [wp] [Qed] Goal typed_some_behaviors_bhv1_assign_normal_part3 : Valid
 [wp] [Qed] Goal typed_some_behaviors_bhv1_assign_normal_part4 : Valid
 [wp] [Qed] Goal typed_some_behaviors_bhv1_assign_normal_part5 : Valid
-[wp] Proved goals:   46 / 46
-  Qed:            43 
-  Alt-Ergo:        3
+[wp] Proved goals:   50 / 51
+  Qed:            47 
+  Alt-Ergo:        3  (unknown: 1)
 [wp] Report 'tests/wp_plugin/dynamic.i.0.report.json'
 -------------------------------------------------------------
 Functions           WP     Alt-Ergo        Total   Success
@@ -62,6 +67,7 @@ call                 2      2 (56..80)       4       100%
 guarded_call         4      1 (16..28)       5       100%
 behavior             9     -                 9       100%
 some_behaviors      24     -                24       100%
+missing_context      4     -                 5      80.0%
 no_call              4     -                 4       100%
 -------------------------------------------------------------
 [wp] Warning: Memory model hypotheses for function 'guarded_call':
@@ -73,3 +79,6 @@ no_call              4     -                 4       100%
 [wp] Warning: Memory model hypotheses for function 'some_behaviors':
   /*@ behavior typed: requires \separated(&X1,p); */
   int some_behaviors(int (*p)(void));
+[wp] Warning: Memory model hypotheses for function 'missing_context':
+  /*@ behavior typed: requires \separated(&X1,p); */
+  int missing_context(int (*p)(void));