|
# What is RefacCert ?
|
|
# What is RefacCert ?
|
|
|
|
|
|
RefacCert is a project to explore the idea of a "proven correct" refactoring tool for C source code. It relies on the CompCert C formalization in Coq : http://compcert.inria.fr .
|
|
RefacCert is a project to explore the idea of a "proven correct" refactoring tool. It is designed for C source code and is based on CompCert C : http://compcert.inria.fr .
|
|
|
|
|
|
|
|
|
|
# Contract
|
|
# Contract
|
|
|
|
|
... | @@ -10,18 +9,24 @@ Our main focus is to ensure that if the operation succeeds, the resulting progra |
... | @@ -10,18 +9,24 @@ Our main focus is to ensure that if the operation succeeds, the resulting progra |
|
Supported operations :
|
|
Supported operations :
|
|
|
|
|
|
* Renaming global variables.
|
|
* Renaming global variables.
|
|
* Swapping two global variable names (as an example of composed operation).
|
|
** And swapping two global variable names.
|
|
|
|
* Removing unused local variables.
|
|
|
|
** And adding a local variable.
|
|
|
|
|
|
|
|
|
|
# Status
|
|
# Status
|
|
|
|
|
|
This is a work in progress with the limitations given below.
|
|
This is a proof of concept. It has the limitations given below.
|
|
|
|
|
|
# Publications
|
|
# Publications
|
|
|
|
|
|
* The research report is available at https://hal.archives-ouvertes.fr/hal-01248121 (dec. 2015).
|
|
* The research report is available at https://hal.archives-ouvertes.fr/hal-01248121 (dec. 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).
|
|
|
|
|
|
|
|
* 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) : +Renaming Global Variables in C Mechanically Proved Correct+ (2016)
|
|
|
|
* 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
|
|
# Limitations
|
|
|
|
|
|
* We do not take the preprocessor into account.
|
|
* We do not take the preprocessor into account.
|
... | | ... | |