## 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.