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.
Contextual information
- 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 a.c
/*@
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)).
The -1
does not seem to be right.
In 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?