[wp] added test for integer quantifiers

src/plugins/wp/tests/wp_bts/issue_825.i

+/*@
+  ensures \false ;
+  assigns \nothing;
+*/
+void job(void)
+{
+  int i=0, K=0;
+  /*@
+    loop invariant \forall integer j; 0 < j < 0 ==> \false ;
+    loop assigns i ;
+  */
+  while (i < 10) {
+    K ++;
+    i ++;
+  }
+}

src/plugins/wp/tests/wp_bts/oracle/issue_825.res.oracle

+# frama-c -wp [...]
+[kernel] Parsing tests/wp_bts/issue_825.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+------------------------------------------------------------
+  Function job
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_bts/issue_825.i, line 2) in 'job':
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant (file tests/wp_bts/issue_825.i, line 9):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant (file tests/wp_bts/issue_825.i, line 9):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_bts/issue_825.i, line 10) (1/2):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_bts/issue_825.i, line 10) (2/2):
+Effect at line 13
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'job':
+Effect at line 12
+Prove: true.
+
+------------------------------------------------------------

src/plugins/wp/tests/wp_bts/oracle_qualif/issue_825.res.oracle

+# frama-c -wp [...]
+[kernel] Parsing tests/wp_bts/issue_825.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[wp] 6 goals scheduled
+[wp] [Qed] Goal typed_job_ensures : Valid
+[wp] [Qed] Goal typed_job_loop_invariant_preserved : Valid
+[wp] [Qed] Goal typed_job_loop_invariant_established : Valid
+[wp] [Qed] Goal typed_job_loop_assigns_part1 : Valid
+[wp] [Qed] Goal typed_job_loop_assigns_part2 : Valid
+[wp] [Qed] Goal typed_job_assigns : Valid
+[wp] Proved goals:    6 / 6
+  Qed:             6
+------------------------------------------------------------
+ Functions                 WP     Alt-Ergo  Total   Success
+  job                       6        -        6       100%
+------------------------------------------------------------