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 <str>  sets the name of the constants used in invariants
                    (default __PILAT__)
-pilat-degree <n>   sets the maximum degree of the invariants (default : 2)
-pilat-ev <n>       sets the maximal eigenvalue searched for when using
                    zarith
-pilat-optim-epsilon <str>  Tolerance of error during optimization (default
                    0.05)
-pilat-optim-iters <n>  sets the maximal number of iterations performed
                    during the optimisation (default 10)
-pilat-optim-start <n>  sets the initial value of k during the optimisation
                    (default 50)
-pilat-output <s>   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 <x:y:...>  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)