## 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 `

Coq`proof obligations. When one adds a simple`

intros` 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.

To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information