coq reports an error for a hypothesis involving 'region'

• the issue has not yet been reported on Gitlab;
• the issue has not yet been reported on our BTS;
• you installed Frama-C as prescribed in the instructions.

Contextual information

• Frama-C installation mode: Homebrew
• Frama-C version: 21.0 (Scandium)
• Plug-in used: WP
• OS name: macOS
• OS version: 10.15.5

Please add specific information deemed relevant with regard to this issue.

When trying to proof an obligation with coq, an error is reported w.r.t. to a region hypothesis.

Steps to reproduce the issue

Here is a small example (b.c) of a not particularly expressive function contract

/*@
  requires \valid_read(a + (0..n-1));
  requires \valid(b + (0..n-1));
  assigns  b[0..n-1];
*/
void copy(int* a, unsigned int n, int* b)
{
    /*@
      loop assigns i, b[0..n-1];
    */
    for(unsigned int i = 0; i < n; ++i)
        b[i] = a[i];
}

When calling it with the command line

frama-c-gui -wp -wp-rte -wp-prover alt-ergo -wp-prover native:coq b.c

everything is verified by qed or alt-ergo. The problem I want to report is related to the generated Coqproof obligations. When one adds a simpleintros` to Loop assigns (file b.c, line 10) in the Coq IDE, as in

Goal
  forall (i_1 i : Z),
  forall (t : array Z),
  forall (a_1 a : addr),
  let a_2 := (shift_sint32 a 0%Z) in
  let a_3 := (shift_sint32 a i_1%Z) in
  ((i_1 < i)%Z) ->
  ((((region ((base a_1))%Z)) <= 0)%Z) ->
  ((((region ((base a))%Z)) <= 0)%Z) ->
  ((linked t)) ->
  ((is_uint32 i_1%Z)) ->
  ((is_uint32 i%Z)) ->
  ((valid_rd t ((shift_sint32 a_1 0%Z)) i%Z)) ->
  ((valid_rd t ((shift_sint32 a_1 i_1%Z)) 1%Z)) ->
  ((valid_rw t a_2 i%Z)) ->
  ((valid_rw t a_3 1%Z)) ->
  (~((invalid t a_3 1%Z))) ->
  ((included a_3 1%Z a_2 i%Z)).

Proof.
  intros.
Qed.

then the following error message is shown

Illegal application (Non-functional construction): 
The expression "region" of type "array int" cannot be applied to the term
 "base a_1" : "int"

I conclude from this that the generated coq obligation is syntactically not correct.