Frama-C Bug Tracking System

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0002374Frama-CPlug-in > wppublic2018-05-09 13:192018-05-25 17:47
Reporterjens 
Assigned Tocorrenson 
PriorityhighSeverityblockReproducibilityalways
StatusassignedResolutionno change required 
PlatformOSOS Version
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in Version 
Summary0002374: Strange difference in generated Coq code between Chlorine and Sulfur
DescriptionThis 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.
TagsNo tags attached.
Attached Filesc file icon foo.c [^] (685 bytes) 2018-05-09 13:19 [Show Content]
? file icon A_Count.sulfur.v [^] (1,416 bytes) 2018-05-09 13:20
? file icon A_Count.chlorine.v [^] (1,407 bytes) 2018-05-09 13:20

- Relationships

-  Notes
(0006546)
correnson (manager)
2018-05-24 11:44

No, it seems OK. Count has the right number of argument in both cases (5).
What happened here is the elimination of quantification because of it is actually a let-binding.
Namely, we now apply the following normalisation :

 forall x,y, x=e(y) -> P(x,y) <==> forall y, let x = e(y) in P(x,y)

This is why i_2 disappear from the Sulfur and was replaced by let x_1 := ... in the Chlorine version.
(0006547)
correnson (manager)
2018-05-24 11:45

New normalisation of quantifiers that can be replaced by let-bindings.
(0006548)
correnson (manager)
2018-05-24 11:46

Remark: there is a dual normalisation for existential quantifiers :

  exits x, x = e /\ P <==> let x = e in P
(0006549)
jens (reporter)
2018-05-24 12:27

Thanks for the reply but it is still not clear to me how I have to adapt my existing Coq proofs so that they work with the new form.
(0006550)
correnson (manager)
2018-05-24 13:40

The only problem will be when instantiating axiom CountSectinHit.

You probably had to supply the correct value for `v`, and then, discharge the equality constraint `v == a[i-1]`
by hand.

With the normalized axiom, you don't have to supply the value `v`, as it is already replaced by value `a[i-1]` in the instantiated axiom.

So I guess adapting the script would be very easy.
(0006551)
jens (reporter)
2018-05-25 17:47

It took some time until I understood how to deal with this new representation.
I have already modified a few of my coq proofs but I am not through yet.
You are saying that I don't need to supply the value 'v'. This is true but I introduced 'v' in my proofs to make them more readable and thus more maintainable.

I probably have still a lot to learn about writing good coq proofs...

- Issue History
Date Modified Username Field Change
2018-05-09 13:19 jens New Issue
2018-05-09 13:19 jens Status new => assigned
2018-05-09 13:19 jens Assigned To => correnson
2018-05-09 13:19 jens File Added: foo.c
2018-05-09 13:20 jens File Added: A_Count.sulfur.v
2018-05-09 13:20 jens File Added: A_Count.chlorine.v
2018-05-24 11:44 correnson Note Added: 0006546
2018-05-24 11:45 correnson Note Added: 0006547
2018-05-24 11:45 correnson Status assigned => resolved
2018-05-24 11:45 correnson Resolution open => no change required
2018-05-24 11:46 correnson Note Added: 0006548
2018-05-24 11:46 correnson Status resolved => assigned
2018-05-24 12:27 jens Note Added: 0006549
2018-05-24 13:40 correnson Note Added: 0006550
2018-05-25 17:47 jens Note Added: 0006551


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker