[spec] separate wp objectives from kernel ones in check test

tests/spec/generalized_check.i

 /* run.config
-OPT: -wp -wp-prover qed -wp-msg-key no-cache-info,no-time-info -print
+OPT: -wp -wp-prover qed -wp-msg-key no-cache-info,no-time-info
 OPT: -eva -eva-use-spec f
+OPT: -print
 */
 /*@ check lemma easy_proof: \false; */ // should not be put in any environment
 

tests/spec/oracle/generalized_check.0.res.oracle

 [kernel] Parsing tests/spec/generalized_check.i (no preprocessing)
 [wp] Running WP plugin...
-[wp] tests/spec/generalized_check.i:29: Warning: 
+[wp] tests/spec/generalized_check.i:30: Warning: 
   Unsupported generalized invariant, use loop invariant instead.
   Ignored invariant 
   check invariant \true;
 [wp] Warning: Missing RTE guards
-[wp] tests/spec/generalized_check.i:36: Warning: 
+[wp] tests/spec/generalized_check.i:37: Warning: 
   Missing assigns clause (assigns 'everything' instead)
 [wp] 11 goals scheduled
 [wp] [Qed] Goal typed_f_assigns : Valid
@@ -21,53 +21,3 @@
 [wp] [Failed] Goal typed_main_check_main_valid_ko
 [wp] Proved goals:    3 / 11
   Qed:             3
-/* Generated by Frama-C */
-/*@ check lemma easy_proof: \false;
- */
-/*@ check requires f_valid_x: \valid(x);
-    check ensures f_init_x: *\old(x) ≡ 0;
-    assigns *x;
- */
-void f(int *x)
-{
-  /*@ check f_valid_ko: \valid(x); */ ;
-  *x = 0;
-  return;
-}
-
-void loop(void);
-
-int main(void)
-{
-  int __retres;
-  int volatile c;
-  int a = 4;
-  int *p = (int *)0;
-  if (c) p = & a;
-  f(p);
-  /*@ check main_valid_ko: \valid(p); */ ;
-  /*@ check main_p_content_ko: *p ≡ 0; */ ;
-  loop();
-  __retres = 0;
-  return __retres;
-}
-
-void loop(void)
-{
-  int j = 0;
-  {
-    int i = 0;
-    /*@ check loop invariant false_but_preserved: j ≡ 10;
-        loop assigns i; */
-    while (i < 10) i ++;
-  }
-  /*@ check implied_by_false_invariant: j ≡ 10; */ ;
-  l: /*@ check invariant \true; */ ;
-  if (j >= 10) goto l1;
-  j ++;
-  goto l;
-  l1: ;
-  return;
-}
-
-

tests/spec/oracle/generalized_check.1.res.oracle

@@ -4,21 +4,21 @@
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
   
-[eva:alarm] tests/spec/generalized_check.i:22: Warning: 
+[eva:alarm] tests/spec/generalized_check.i:23: Warning: 
   accessing uninitialized left-value. assert \initialized(&c);
 [eva] using specification for function f
-[eva:alarm] tests/spec/generalized_check.i:23: Warning: 
+[eva:alarm] tests/spec/generalized_check.i:24: Warning: 
   function f: precondition 'f_valid_x' got status unknown.
-[eva] tests/spec/generalized_check.i:8: Warning: 
+[eva] tests/spec/generalized_check.i:9: Warning: 
   no \from part for clause 'assigns *x;'
-[eva:alarm] tests/spec/generalized_check.i:24: Warning: 
-  check 'main_valid_ko' got status unknown.
 [eva:alarm] tests/spec/generalized_check.i:25: Warning: 
+  check 'main_valid_ko' got status unknown.
+[eva:alarm] tests/spec/generalized_check.i:26: Warning: 
   check 'main_p_content_ko' got status unknown.
-[eva:alarm] tests/spec/generalized_check.i:31: Warning: 
+[eva:alarm] tests/spec/generalized_check.i:32: Warning: 
   loop invariant 'false_but_preserved' got status invalid.
-[eva] tests/spec/generalized_check.i:34: starting to merge loop iterations
-[eva:alarm] tests/spec/generalized_check.i:35: Warning: 
+[eva] tests/spec/generalized_check.i:35: starting to merge loop iterations
+[eva:alarm] tests/spec/generalized_check.i:36: Warning: 
   check 'implied_by_false_invariant' got status invalid.
 [eva] done for function main
 [eva] ====== VALUES COMPUTED ======

tests/spec/oracle/generalized_check.2.res.oracle

+[kernel] Parsing tests/spec/generalized_check.i (no preprocessing)
+/* Generated by Frama-C */
+/*@ check lemma easy_proof: \false;
+ */
+/*@ check requires f_valid_x: \valid(x);
+    check ensures f_init_x: *\old(x) ≡ 0;
+    assigns *x;
+ */
+void f(int *x)
+{
+  /*@ check f_valid_ko: \valid(x); */ ;
+  *x = 0;
+  return;
+}
+
+void loop(void);
+
+int main(void)
+{
+  int __retres;
+  int volatile c;
+  int a = 4;
+  int *p = (int *)0;
+  if (c) p = & a;
+  f(p);
+  /*@ check main_valid_ko: \valid(p); */ ;
+  /*@ check main_p_content_ko: *p ≡ 0; */ ;
+  loop();
+  __retres = 0;
+  return __retres;
+}
+
+void loop(void)
+{
+  int j = 0;
+  {
+    int i = 0;
+    /*@ check loop invariant false_but_preserved: j ≡ 10;
+        loop assigns i; */
+    while (i < 10) i ++;
+  }
+  /*@ check implied_by_false_invariant: j ≡ 10; */ ;
+  l: /*@ check invariant \true; */ ;
+  if (j >= 10) goto l1;
+  j ++;
+  goto l;
+  l1: ;
+  return;
+}
+
+