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.

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

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.

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

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.