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-06-05 09:41
Reporterjens 
Assigned Tocorrenson 
PriorityhighSeverityblockReproducibilityalways
StatusclosedResolutionno 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...
(0006554)
jens (reporter)
2018-06-03 11:58

I suggest to close this issue because there is no error.
On the other hand, the question is how to communicate this type of changes to the (few?) user of Coq.
(0006557)
correnson (manager)
2018-06-05 09:40

I fully agree. Probably, as we plan to switch to, the Why-3 output will be more stable in the future.
(0006558)
correnson (manager)
2018-06-05 09:41

Problem resolved.
Shall work on how to handle script migration when output is broken.

- 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
2018-06-03 11:58 jens Note Added: 0006554
2018-06-05 09:40 correnson Note Added: 0006557
2018-06-05 09:41 correnson Note Added: 0006558
2018-06-05 09:41 correnson Status assigned => closed


Copyright © 2000 - 2018 MantisBT Team
Powered by Mantis Bugtracker