Frama-C-RPP

This is the RPP (Relational Property Prover) plug-in of Frama-C.

Relational Properties

Relational properties are properties invoking any finite number of function calls of possibly dissimilar functions with possible nested calls. Examples:

   ∀ x1,x2; x1 < x2 ⇒ f(x1) < f(x2)
   
   ∀ message, key; message = Decrypt(Encrypt(message,key),key)

A Relational Property Prover

RPP is a Frama-C plug-in designed for the proof of relational properties. It is based on the technique of self-composition and works like a preprocessor for WP plug-in. After its execution on a project containing relational properties annotations, the proof on the generated code proceeds like any other proof with WP: proof obligations are generated and can be either discharged automatically by automatic theorem provers (e.g. Alt-Ergo, CVC4, Z3) or proven interactively (e.g. in Coq). The plug-in also generates an axiomatic definition and additional annotations that allow to use a relational property as a hypothesis for the proof of other properties in a completely automatic and transparent way.

Installation

RPP v0.0.1 requires Frama-C v17.0 Chlorine. For more information see Frama-C.

For installation, run following commands in the RPP directory:

    make
    make install

Usage

• For command ligne interface:

        frama-c -rpp file.c
  

• For graphic user interface (call from terminal):

        frama-c-gui -rpp file.c
  

• For graphic user interface (call from gui): select a relational clause in the gui, right click and select RPP. A new project will be generated ("RPP proof system").

• For generating only the self-composition transformation:

       frama-c -rpp -rpp-pro file.c
  

• For generating only the acsl annotations:

       frama-c -rpp -rpp-hyp file.c
  

Example of relational properties specification

Concider function f:

        int f(int x){
            return x + 1;
        }

If we want to specify monotony on function f we can write:

         /*@ relational \forall int x1,x2; \callset(\call(f,x1,id1),\call(f,x2,id2)),x1 < x2 ==> \callresult(id1) < \callresult(id2);*/

Or, because f has no side effect, we can also write a shorter form for pure functions:

        /*@ relational \forall int x1,x2 ; x1 < x2 ==> \callpure(f,x1) < \callpure(f,x2);*/

If we now consider function g and global variable y:

        int y;

        int g(){
            y = y + 1;
        }

The specification of monotony on g can be written as follows:

       /*@ relational \callset(\call(f,id1),\call(f,id2)),\at(y,Pre_id1) < \at(y,Pre_id2) ==> \at(y,Post_id1) < \at(y,Post_id2);*/

More examples are available in :

    test/rpp/

More documentations can be found in:

     doc/