RPP

Overview

RPP (Relational Property Prover) is a plug-in dedicated to verifying Relational Properties, that is, properties that concern several executions of one or more functions. A simple example is the case of a compare function, for which one would like to check that is anti-symmetric (that is, if called with arguments x and y, it returns an opposite result than if called with y and x), or transitive (if it says that x is smaller than y and y smaller than z, it should also say that x is smaller than z).

Such properties cannot be easily described through standard function contracts. RPP introduces an ACSL extension to let users specify their relational properties, and relies on WP over an instrumented version of the code to perform the proofs and use the proven properties as hypotheses in other proofs.

Usage

An earlier version of the plug-in is available on Github, compatible with Frama-C 17.0 Chlorine. A version for newer Frama-C releases can be made available upon request.

In order to use the plug-in, one has to write relational properties for their functions. Then:

frama-c -rpp file.c

will take care of generating the instrumented version of the code and launching WP on it.