|
|
|
|
|
## What is RefacCert ?
|
|
|
|
|
|
RefacCert is a project to build a "proven correct" refactoring tool for C source code. It is based on CompCert C : http://compcert.inria.fr .
|
|
|
|
|
|
## Contract
|
|
|
|
|
|
Our main focus is to ensure that if the operation succeeds, the resulting program will have the same behavior as the original program. It the operation fails, the program is left unchanged.
|
|
|
|
|
|
## Status
|
|
|
|
|
|
This is a work in progress: the first version has a single refactoring operation to rename global variables. It also has the limitations given below.
|
|
|
|
|
|
## Publications
|
|
|
|
|
|
The research report is available at https://hal.archives-ouvertes.fr/hal-01248121 .
|
|
|
|
|
|
## Limitations
|
|
|
|
|
|
* We do not take the preprocessor into account.
|
|
|
* We do not take comments and layout into account.
|
|
|
* We transform single files.
|
|
|
|
|
|
## Development
|
|
|
|
|
|
Developped by Julien Cohen, Lina laboratory (Ascola team http://www.emn.fr/z-info/ascola/doku.php), University of Nantes (Polytech Nantes).
|
|
|
|
|
|
## What's new ?
|
|
|
|
|
|
### Version 0.4 (based on CompCert 2.4)
|
|
|
|
|
|
* Added an operation 'swap' to swap two global variable names. This operation relies on the base operation that renames global variables.
|
|
|
* A sufficient precondition for Swap is proved.
|
|
|
|
|
|
### Version 0.3
|
|
|
|
|
|
* The transformation is proved invertible. This simplifies some results for bisimulation (in particular backward simulation comes for free from forward simulation).
|
|
|
|
|
|
### Version 0.2
|
|
|
|
|
|
* Preservation of behaviors (type program_behavior, relation program_behaves).
|
|
|
* Example of static composition.
|
|
|
|
|
|
### Version 0.1 (based on CompCert 2.3pl2)
|
|
|
|
|
|
* Renaming of global variables.
|
|
|
* Preservation of transitions with a correspondence on traces is proved.
|
|
|
|