Next: , Previous: Inputs, Up: Top


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: