Module Variables_analysis

module Variables_analysis: sig .. end
This analysis performs a classification of the variables of the input program. The aim of this classification is to optimize the translation of variables by WP: 1) optimization of the by-reference call and 2) functional variables.


At the end, the analysis associates an var_kind information to each variables: 1) Fvar functional variable, variable such as its address is never taken,

2) PRarg by_pointer_reference argument, variable such as its address is only taken in by reference calls (one or more),

3) ARarg by_array_reference argument, variable such as its address is only taken in by array reference calls (one or more),

4) PRpar n by_pointer_reference parameter of arity , variable which is a formal parameter use for a by reference call and can be invoked in a chain of by reference call such as their arity are less or equal than n,

5) ARpar n by_array_reference parameter of arity , variable which is a formal parameter use for a by array reference call and can be invoked in a chain of by array reference call such as their arity are less or equal than n,

6) Cvar other variable.


type var_kind = 
| Fvar
| Cvar
| PRarg
| ARarg
| PRpar of int
| ARpar of int
val dispatch_cvar : Cil_types.varinfo -> var_kind
dispatch_cvar v returns the var_kind associated to the C variable v according the current optimisations activated.
val dispatch_lvar : Cil_types.logic_var -> var_kind
dispatch_lvar v returns the var_kind associated to the logic variable v according the current optimisations activated.
val is_to_scope : Cil_types.varinfo -> bool
is_to_scope v returns true if v has to been scoped into the inner memory model : cvar of ref
val precondition_compute : unit -> unit
precondition_compute () adds warnings and precondition suitable to the current optimisations which are activated
val brackets_typ : Cil_types.typ -> int
brackets_typ typ returns the numbre of brackets of the type typ.
val is_user_formal_in_builtin : Cil_types.logic_var -> bool
is_user_formal_in_builtins lv tests if the address of the by-reference formal lv of user definition is an argument of (one or more) ACSL builtin predicate(s) or function : valid and family, separated, block_length, initialized