module Variables_analysis:sig
..end
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 |
| |
ARpar of |
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 refval precondition_compute : unit -> unit
precondition_compute ()
adds warnings and precondition suitable
to the current optimisations which are activatedval 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