search

Stevendeo / Pilat

Invariant generator for polynomial loops
GNU Lesser General Public License v2.1
8 stars 2 forks source link

readme 

            ------
            README
            ------

This package contains PILAT, the Frama-C plugin for generating loop invariant. If you have no clue of what is Frama-C, please visit http://frama-c.com.

This tool is based on the results of the article "Polynomial invariants by linear algebra", available at https://arxiv.org/abs/1611.07726.

Please consult file INSTALL for details about the installation procedure of Frama-C.

             -----
             USAGE
             -----

Pilat is a part of the Frama-C platform, i.e. it is one of its options. To activate it, just type :

frama-c your_file.c -pilat

This will generate by default the "whole_program_annot.c" file with degree 2 invariants written in ACSL, the specification language used by Frama-C plugins. You can select any degree by using the option -pilat-degree.

Most options of the form '-pilat-option-name' and without any parameter have an opposite with the name '-pilat-no-option-name'.

Most options of the form '-option-name' and without any parameter have an opposite with the name '-no-option-name'.

Options taking a string as argument should preferably be written -option-name="argument".

***** LIST OF AVAILABLE OPTIONS:

-pilat when on, generates polynomial invariants for each solvable loop of the program (opposite option is -no-pilat) -pilat-const-name sets the name of the constants used in invariants (default PILAT) -pilat-degree sets the maximum degree of the invariants (default : 2) -pilat-ev sets the maximal eigenvalue searched for when using zarith -pilat-optim-epsilon Tolerance of error during optimization (default 0.05) -pilat-optim-iters sets the maximal number of iterations performed during the optimisation (default 10) -pilat-optim-start sets the initial value of k during the optimisation (default 50) -pilat-output specifies generated file name for annotated C code -pilat-prove when on, tries to prove already existing loop invariants (opposite option is -pilat-no-prove) -pilat-vars specifies which variables will be analyzed. -pilat-z when on, uses zarith library. Recommended if searching for integer relations but depreciated when searching for floating point relations. (set by default, opposite option is -pilat-no-z)