5 Options
The CELIA plugin is called as follows:
frama-c-Celia.byte <Frama-C options> -celia <input C files>
The Frama-C options external to CELIA are explained in the Frama-C documentation.
The options relevant for CELIA are:
- -celia
- activates the CELIA plug-in in Frama-C,
- -celia-cinv-opt
- specifies the property file from which the options for the analysis has to be read.
The property file is a list of lines
key=value
where key specifies the option and value specifies the value of the option.
The following tuples of keys and values are known to CELIA:
- domain
- the abstract domain to use (default: shape).
- dwdomain
- abstract domain used for list segments; possible values are lsum (default),
mset, and ucons. If this appear several times with different values, it specifies a product of these domains.
- maxanon
- default maximum number of anonymous nodes per segment (default 0);
this number can be changed for each function (see option
funspec).
- maxasegm
- default maximum number of segments with anonymous nodes (default 1, may only be more);
this number can be changed for each function (see option
funspec).
- funspec
- the property file in which are given specific parameters of analysis for each function, see FunctionOptions.
- depth
- (option for Fixpoint) depth of recursive iterations (default 2, may only be more).
- guided
- (option for Fixpoint) if true, guided analysis of Gopand and Reps (default: false).
- wdelay
- (option for Fixpoint) specifies usage of widening delay steps (default: 1).
- wdesc
- specifies usage of widening number of descending steps (default: 2).
- main
- entry point function for the analysis (default: main).
Options specific for functions
The format of this file is a sequence of line, each line having the form:
function_name: n s p
where:
n gives maxanon parameter (positive integer),
s gives maxsegm parameter (strictly positive integer),
p gives patterns to be used in the UCONS domain; it is an integer value obtained from the binary or of the following values:
- 1
for pattern forall y in n (default value)
- 2
for pattern forall y1 in n1, y2 in n2. y1==y2
- 4
for pattern forall y1,y2 in n1. y1<=y2