[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
CountBoundsthat works for Frama-C 20
- an attempt of a coq proof in file
CountBoundsthat fails for Frama-C 21
- The files
CountBounds.v.21contain the coq code as extracted from CoqIde
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.
I suspect that this is related to changes in the generated Coq code of the VC of lemma
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)) ->
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.