|
|
|
|
|
## What is RefacCert ?
|
|
|
# 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
|
|
|
|
|
|
# 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
|
|
|
Supported operations :
|
|
|
|
|
|
* Renaming global variables.
|
|
|
* Swapping two global variable names.
|
|
|
|
|
|
|
|
|
# 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
|
|
|
# Publications
|
|
|
|
|
|
The research report is available at https://hal.archives-ouvertes.fr/hal-01248121 .
|
|
|
* The research report is available at https://hal.archives-ouvertes.fr/hal-01248121 .
|
|
|
* 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).
|
|
|
|
|
|
## Limitations
|
|
|
# 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 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.
|
|
|
|
|
|
## Development
|
|
|
# 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 ?
|
|
|
# What's new ?
|
|
|
|
|
|
### Version 0.4 (based on CompCert 2.4)
|
|
|
### Version 0.6 (based on Compcert 2.6)
|
|
|
|
|
|
* BUGFIX : problematic situations with block variables are now rejected.
|
|
|
|
|
|
### 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).
|
|
|
* 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).
|
|
|
|
|
|
* Preservation of behaviors (type @program_behavior@, relation @program_behaves@).
|
|
|
* Example of static composition.
|
|
|
|
|
|
### Version 0.1 (based on CompCert 2.3pl2)
|
|
|
|
|
|
### Version 0.1 (based on Compcert 2.3pl2)
|
|
|
|
|
|
* Renaming of global variables.
|
|
|
* Preservation of transitions with a correspondence on traces is proved. |
|
|
|