[wp] non-provable local typing constraints in lemmas

Steps to reproduce the issue

The attached archive contains the ACSL function Count together with several lemma. Also contained are

• a Makefile
• a coq proof in file wp0.script.20 for lemma CountBounds that works for Frama-C 20
• an attempt of a coq proof in file wp0.script.21 for lemma CountBounds that fails for Frama-C 21
• The files CountBounds.v.20 and CountBounds.v.21 contain the coq code as extracted from CoqIde

Expected behaviour

My problem is that I am unable to adapt the coq proof that worked fro Frama-C 20 to the newer version of Frama-C.

Actual behaviour

I suspect that this is related to changes in the generated Coq code of the VC of lemma CountBounds This can be best seen when calling diff CountBounds.v.20 CountBounds.v.21.

$ diff CountBounds.v.20  CountBounds.v.21 
39,40c39,40
<   (((t.[ (shift_sint32 a x) ]) <> i_2)%Z) -> ((i < i_1)%Z) ->
<   ((is_sint32 i_2%Z)) ->
---
>   let x_1 := (t.[ (shift_sint32 a x) ])%Z in ((x_1 <> i_2)%Z) ->
>   ((i < i_1)%Z) -> ((is_sint32 i_2%Z)) -> ((is_sint32 x_1)) ->

Fix ideas

I think the issue is caused by the condition ((is_sint32 x_1)) for the newly introduced term x_1 := (t.[ (shift_sint32 a x) ])%Z. I haven't found a way to satisfy the condition ((is_sint32 x_1)) and I suspect that it is not possible. If it is possible, then I apologise and ask for a hint.

Regards

Jens Gerlach

CoqFramac21.tar