Anonymous | Login | Signup for a new account | 2018-05-25 20:24 CEST |

Main | My View | View Issues | Change Log | Roadmap | Repositories |

View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||||||

ID | Project | Category | View Status | Date Submitted | Last Update | ||||||||

0002374 | Frama-C | Plug-in > wp | public | 2018-05-09 13:19 | 2018-05-25 17:47 | ||||||||

Reporter | jens | ||||||||||||

Assigned To | correnson | ||||||||||||

Priority | high | Severity | block | Reproducibility | always | ||||||||

Status | assigned | Resolution | no change required | ||||||||||

Platform | OS | OS Version | |||||||||||

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

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

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 |