Strange difference in generated Coq code between Chlorine and Sulfur

ID0002374: This issue was created automatically from Mantis Issue 2374. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0002374	Frama-C	Plug-in > wp	public	2018-05-09	2018-06-05

Reporter	jens	Assigned To	correnson	Resolution	no change required
Priority	high	Severity	block	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C GIT, precise the release id	Target Version	-	Fixed in Version	-

Description :

This report refers to the BETA-release of Chlorine and affects a couple of Coq-proofs in ACSL by Example:

The problem is like this: If the attached file 'foo.c' is processed with the command line

  frama-c -wp -wp-prover coq -wp-out foo.wp foo.c

then it produces in foo.wp among other files the Coq file A_Count.v. The only difference when using with Frama-C-Sulfur or Frama-C-Chlorine is the following:

diff A_Count.sulfur.v A_Count.chlorine.v

28,32c28,32 < Hypothesis Q_CountSectionHit: forall (i_2 i_1 i : Z), < forall (t : farray addr Z), forall (a : addr), let x := (i_1%Z - 1%Z)%Z in < (((t.[ (shift_sint32 a x) ]) = i_2)%Z) -> ((i < i_1)%Z) -> < ((is_sint32 i_2%Z)) -> < (((1 + ((L_Count t a i%Z x i_2%Z))) = ((L_Count t a i%Z i_1%Z i_2%Z)))%Z).

Hypothesis Q_CountSectionHit: forall (i_1 i : Z), forall (t : farray addr Z), forall (a : addr), let x := (i_1%Z - 1%Z)%Z in let x_1 := (t.[ (shift_sint32 a x) ])%Z in ((i < i_1)%Z) -> ((is_sint32 x_1)) -> (((1 + ((L_Count t a i%Z x x_1))) = ((L_Count t a i%Z i_1%Z x_1)))%Z).

It looks like as if the argument 'v' of axiom 'CountSectionHit' has not been translated into Coq.

Attachments

• foo.c
• A_Count.sulfur.v
• A_Count.chlorine.v