suspicious Coq code for ACSL lemma in Frama-C 21
Thank you for submitting an issue to the Frama-C team. We propose the following template to ease the process. Please directly edit it inline to provide the required information.
Before submitting the issue, please confirm (by adding a X in the [ ]):
- 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.
- Frama-C installation mode: opam
- 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.
Steps to reproduce the issue
The following ACSL lemma in file
/*@ lemma C_Division_Two: \forall integer a; 0 <= a ==> 0 <= a/2 <= a; */
is verified by Alt-Ergo when calling it with
frama-c-gui -wp -wp-prover alt-ergo -wp-prover native:coq a.c
However, in Frama-C 21, the coq representation of the lemma looks wrong to me since it reads
Goal forall (i : Z), ((0 <= i)%Z) -> (((((Cdiv i 2)) <= i)%Z) /\ (((-1) <= i)%Z)).
-1 does not seem to be right.
Frama-C 20, on the other hand, the coq representation looks like this
Goal forall (i : Z), let x := ((Cdiv i 2))%Z in ((0 <= i)%Z) -> (((x <= i)%Z) /\ ((0 <= x)%Z)).
Am I missing something here?