|Anonymous | Login | Signup for a new account||2019-01-19 04:16 CET|
|Main | My View | View Issues | Change Log | Roadmap | Repositories|
|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0002374||Frama-C||Plug-in > wp||public||2018-05-09 13:19||2018-06-05 09:41|
|Status||closed||Resolution||no change required|
|Product Version||Frama-C GIT, precise the release id|
|Target Version||Fixed in Version|
|Summary||0002374: Strange difference in generated Coq code between Chlorine and Sulfur|
|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
< 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.
|Tags||No tags attached.|
|Attached Files|| foo.c [^] (685 bytes) 2018-05-09 13:19 [Show Content]
A_Count.sulfur.v [^] (1,416 bytes) 2018-05-09 13:20
A_Count.chlorine.v [^] (1,407 bytes) 2018-05-09 13:20
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.
|New normalisation of quantifiers that can be replaced by let-bindings.|
Remark: there is a dual normalisation for existential quantifiers :
exits x, x = e /\ P <==> let x = e in P
|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.|
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]`
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.
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...
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.
|I fully agree. Probably, as we plan to switch to, the Why-3 output will be more stable in the future.|
Shall work on how to handle script migration when output is broken.
|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 - 2019 MantisBT Team|