[wp] Coq region is a function

src/plugins/wp/share/coqwp/Memory.v

@@ -249,7 +249,7 @@ Lemma separated_1 :
 Admitted.
 
 (* Why3 goal *)
-Definition region : array Z.
+Definition region : Z -> Z.
 Admitted.
 
 (* Why3 goal *)
@@ -262,7 +262,7 @@ Admitted.
 
 (* Why3 assumption *)
 Definition framed (m: farray addr addr) : Prop :=
-  forall (p:addr), ((region .[ (base (m .[ p ]))] ) <= 0%Z)%Z.
+  forall (p:addr), ((region (base (m .[ p ])) ) <= 0%Z)%Z.
 
 (* Why3 goal *)
 Lemma separated_included :

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

+# frama-c -wp [...]
+[kernel] Parsing tests/wp_plugin/region_to_coq.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[wp] Warning: native support for coq is deprecated, use tip instead
+[wp] 4 goals scheduled
+[wp] [Coq] Goal typed_copy_loop_invariant_preserved : Saved script
+[wp] [Coq (native)] Goal typed_copy_loop_invariant_preserved : Valid
+[wp] [Coq] Goal typed_copy_loop_invariant_established : Saved script
+[wp] [Coq (native)] Goal typed_copy_loop_invariant_established : Valid
+[wp] [Qed] Goal typed_copy_loop_assigns_part1 : Valid
+[wp] [Coq] Goal typed_copy_loop_assigns_part2 : Saved script
+[wp] [Coq (native)] Goal typed_copy_loop_assigns_part2 : Valid
+[wp] Proved goals:    4 / 4
+  Qed:             1 
+  Coq (native):    3
+------------------------------------------------------------
+ Functions                 WP     Alt-Ergo  Total   Success
+  copy                      1        -        4       100%
+------------------------------------------------------------

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

+/* run.config
+   DONTRUN:
+*/
+/* run.config_qualif
+   OPT: -wp-prover native:coq -wp-coq-script tests/wp_plugin/region_to_coq.script
+*/
+
+void copy(int* a, unsigned int n, int* b)
+{
+    /*@ loop invariant 0 <= i <= n ;
+        loop assigns i, b[0..n-1]; */
+    for(unsigned int i = 0; i < n; ++i)
+        b[i] = a[i];
+}

src/plugins/wp/tests/wp_plugin/region_to_coq.script

+(* Generated by Frama-C WP *)
+
+Goal typed_copy_loop_assigns_part2.
+Hint *,b,copy,i,loop-assigns,part-1.
+Proof.
+  intros.
+  unfold included, shift_sint32.
+  unfold base, offset, shift ; simpl.
+  omega.
+Qed.
+
+Goal typed_copy_loop_invariant_established.
+Hint copy,established.
+Proof.
+  unfold is_uint32 ; intros ; omega.
+Qed.
+
+Goal typed_copy_loop_invariant_preserved.
+Hint copy,preserved.
+Proof.
+  intros.
+  assert (Hi_1: (1+i_1 <= i)%Z) by omega.
+  unfold is_uint32, to_uint32.
+  unfold to_range.
+  intros.
+  rewrite Z.add_0_l.
+  repeat rewrite Z.sub_0_r.
+  unfold is_uint32 in H2.
+  assert (Bs: (1 + i_1 = 4294967296)%Z \/ (1 + i_1 < 4294967296)%Z) by omega.
+  inversion Bs.
+  - rewrite <- H4.
+    rewrite Z_mod_same ; omega.
+  - rewrite Z.mod_small ; omega.
+Qed.
+
+