... | ... | @@ -9,9 +9,9 @@ Our main focus is to ensure that if the operation succeeds, the resulting progra |
|
|
Supported operations :
|
|
|
|
|
|
* Renaming global variables.
|
|
|
** And swapping two global variable names.
|
|
|
* And swapping two global variable names.
|
|
|
* Removing unused local variables.
|
|
|
** And adding a local variable.
|
|
|
* And adding a local variable.
|
|
|
|
|
|
|
|
|
# Status
|
... | ... | @@ -22,26 +22,31 @@ This is a proof of concept. It has the limitations given below. |
|
|
|
|
|
|
|
|
* The research report is available at https://hal.archives-ouvertes.fr/hal-01248121 : *A Correct Refactoring Operation to Rename Global Variables in C Programs* (2015)
|
|
|
* An [article](http://arxiv.org/abs/1607.02226) was presented at the _4th International Workshop on Verification and Program Transformation_ (available in [Electronic Proceedings in Theoretical Computer Science](http://eptcs.web.cse.unsw.edu.au/content.cgi?VPT2016) / apr. 2016).
|
|
|
* An [article](http://arxiv.org/abs/1607.02226) was presented at the _4th International Workshop on Verification and Program Transformation_ (available in [Electronic Proceedings in Theoretical Computer Science](http://eptcs.web.cse.unsw.edu.au/content.cgi?VPT2016) / apr. 2016). *Renaming Global Variables in C Mechanically Proved Correct*
|
|
|
* Another research report : *Memory bijections: reasoning about exact memory transformations induced by refactorings in CompCert C* : https://hal.archives-ouvertes.fr/hal-02078356/ (2019)
|
|
|
|
|
|
# Limitations
|
|
|
|
|
|
* We do not take the preprocessor into account.
|
|
|
* We do not take comments and layout into account.
|
|
|
* We transform single files (we do not take the whole project into account).
|
|
|
* The proof of correctness does not cover the whole tool, only its core development in Coq.
|
|
|
* Our proofs of correctness cannot take the preprocessor into account.
|
|
|
* Our prototype cannot preserve comments, layout and preprocessing directives.
|
|
|
* Some parts of the tool (the driver) are written directly in OCaml and cannot be taken into account by proofs of correctness.
|
|
|
|
|
|
|
|
|
# Development
|
|
|
|
|
|
Developped by Julien Cohen, Lina laboratory ([Ascola team](http://www.emn.fr/z-info/ascola/doku.php) and now Galinette team), University of Nantes (Polytech Nantes). Igor Zhirkov is also working on this project.
|
|
|
Developped by Julien Cohen, Lina laboratory (Ascola team http://www.emn.fr/z-info/ascola/doku.php), University of Nantes (Polytech Nantes).
|
|
|
The operation that removes an unused local variable is developped by Igor Zhirkov.
|
|
|
|
|
|
|
|
|
# What's new ?
|
|
|
|
|
|
### Next Version
|
|
|
### Version 0.7 (based on CompCert 2.7.1)
|
|
|
|
|
|
* New refactoring operation : add/remove a local variable, by Igor Zhirkov.
|
|
|
* Proof of correctness for renaming global variables is better structured.
|
|
|
* Correspondences between semantic constructions in programs (contexts, continuations, states...) are now represented by relations and not by functions anymore. Proofs are easier, in particular for context transformation, which needed a painful encoding before, and for continuation transformation, which was too memory and time consuming.
|
|
|
* More iterators are used to ditinguish properties coming from renaming and those coming from tree traversals.
|
|
|
|
|
|
* Based on Compcert 2.7 (for compatibility).
|
|
|
* More understandable proofs.
|
|
|
|
|
|
### Version 0.6 (based on Compcert 2.6)
|
|
|
|
... | ... | |