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.

val dkey : Log.category
val debug : ?level:int -> 'a Log.pretty_printer
val dkey : Log.category
val oracle : ?level:int -> 'a Log.pretty_printer
type var_kind = 
| Fvar
| Cvar
| PRarg
| ARarg
| PRpar of int
| ARpar of int
val stars_typ : Cil_types.typ -> int
val brackets_typ : Cil_types.typ -> int
brackets_typ typ returns the numbre of brackets of the type typ.
val brackets_and_stars_typ : Cil_types.typ -> int
val stars_lv_typ : Cil_types.logic_type -> int
val brackets_lv_typ : Cil_types.logic_type -> int
val brackets_and_stars_lv_typ : Cil_types.logic_type -> int
val stars_exp : Cil_types.exp_node -> (Cil_types.varinfo * Cil_types.typ * int) option
val stars_term : Cil_types.term_node ->
(Cil_types.logic_var * Cil_types.logic_type * int) option
val brackets_off : Cil_types.offset -> int option
val brackets_toff : Cil_types.term_offset -> int option
val bracket_exp : Cil_types.exp_node -> (Cil_types.varinfo * int) option
val bracket_term : Cil_types.term_node -> (Cil_types.logic_var * int) option
val delta_ptr : Cil_types.exp_node -> (Cil_types.varinfo * int) option
val delta_ptr_term : Cil_types.term_node -> (Cil_types.logic_var * int) option
val delta_array : Cil_types.exp_node -> (Cil_types.varinfo * int) option
val delta_array_term : Cil_types.term_node -> (Cil_types.logic_var * int) option
module LogicParam: State_builder.Hashtbl(Cil_datatype.Logic_var.Hashtbl)(Datatype.Bool)(sig
val name : string
val dependencies : State.t list
val size : int
end)
val logic_param_memory_info : LogicParam.key -> unit
type var_type = 
| Cv of Cil_types.varinfo
| Lv of Cil_types.logic_var
| Prop
val is_lformal : LogicParam.key -> bool
val var_type_of_lvar : Cil_types.logic_var -> var_type
val pp_var_type : Format.formatter -> var_type -> unit
val _brackets_var_type_typ : var_type -> int
val brackets_and_stars_var_type_typ : var_type -> int
val stars_var_type_typ : var_type -> int
val isVarTypePointerType : var_type -> bool
val is_formal_var_type : var_type -> bool
module VarType: Datatype.Make_with_collections(sig
include Datatype.Serializable_undefined
val name : string
type t = Variables_analysis.var_type 
val reprs : Variables_analysis.var_type list
val equal : Variables_analysis.var_type -> Variables_analysis.var_type -> bool
val compare : Variables_analysis.var_type -> Variables_analysis.var_type -> int
val hash : Variables_analysis.var_type -> int
end)
module AnyVar: State_builder.Hashtbl(VarType.Hashtbl)(Datatype.Unit)(sig
val name : string
val dependencies : State.t list
val size : int
end)
val add_logics_value : Cil_types.logic_var list -> unit
module AddrTaken: State_builder.Hashtbl(VarType.Hashtbl)(Datatype.Pair(Datatype.Int)(Datatype.Int))(sig
val name : string
val dependencies : State.t list
val size : int
end)
val string_addr : bool -> string
val incr_addr_taken : AddrTaken.key -> unit
val decr_addr_taken : AddrTaken.key -> unit
val decr_addr_taken_bool : AddrTaken.key -> bool -> unit
class logic_parameters_and_addr_taken_collection : ( object
Inherits

method vexpr : Cil_types.exp -> Cil_types.exp Cil.visitAction
method vterm : Cil_types.term -> Cil_types.term Cil.visitAction
method vpredicate : Cil_types.predicate -> Cil_types.predicate Cil.visitAction
method vannotation : Cil_types.global_annotation -> Cil_types.global_annotation Cil.visitAction
end : object ... end )
val compute_logic_params : unit -> unit
module ChainCalls: Datatype.List(Datatype.Pair(Datatype.Int)(Datatype.Pair(Datatype.Bool)(VarType)))
val pp_call : Format.formatter -> int * (bool * var_type) -> unit
val pp_chaincall : Format.formatter -> (int * (bool * var_type)) list -> unit
module ByPReference: State_builder.Hashtbl(VarType.Hashtbl)(Datatype.Pair(Datatype.Int)(ChainCalls))(sig
val name : string
val dependencies : State.t list
val size : int
end)
module ByAReference: State_builder.Hashtbl(VarType.Hashtbl)(Datatype.Pair(Datatype.Int)(ChainCalls))(sig
val name : string
val dependencies : State.t list
val size : int
end)
module ByValue: State_builder.Hashtbl(VarType.Hashtbl)(Datatype.Unit)(sig
val name : string
val dependencies : State.t list
val size : int
end)
val is_pure_logic : var_type -> bool
val add_ptr_reference_param : ByPReference.key -> Datatype.Int.t -> unit
val remove_ptr_reference_param : ByPReference.key -> unit
val add_array_reference_param : ByAReference.key -> Datatype.Int.t -> unit
val remove_array_reference_param : ByAReference.key -> unit
type 'a usage = 
| Ok of 'a
| Ko of 'a
| Any
val by_pointer_reference_usage : Cil_types.exp_node -> (Cil_types.varinfo * int) usage
val by_pointer_reference_usage_term : Cil_types.term_node -> (Cil_types.logic_var * int) usage
val by_array_reference_usage : Cil_types.exp_node -> (Cil_types.varinfo * int) usage
val by_array_reference_usage_term : Cil_types.term_node -> (Cil_types.logic_var * int) usage
val reference_parameter_usage : Cil_types.exp_node -> bool
val reference_parameter_usage_lval : Cil_types.lval -> bool
val reference_parameter_usage_term : Cil_types.term_node -> bool
class parameters_call_kind_analysis : ( object
Inherits

method vinst : Cil_types.instr -> Cil_types.instr list Cil.visitAction
method vexpr : Cil_types.exp -> Cil_types.exp Cil.visitAction
method vterm : Cil_types.term -> Cil_types.term Cil.visitAction
method vpredicate : Cil_types.predicate -> Cil_types.predicate Cil.visitAction
end : object ... end )
val compute_parameters_usage : unit -> unit
val by_pointer_reference_pattern : Cil_types.exp_node ->
(Cil_types.varinfo * bool * int) usage
val by_pointer_reference_pattern_term : Cil_types.term_node ->
(Cil_types.logic_var * bool * int) usage
val help_by_array_reference_pattern : Cil_types.exp_node ->
(Cil_types.varinfo * bool * int) usage
val by_array_reference_pattern : Cil_types.exp_node ->
(Cil_types.varinfo * bool * int) usage
val help_array_reference_pattern_term : string ->
Cil_types.term_node ->
(Cil_types.logic_var * bool * int) usage
val by_array_reference_pattern_term : Cil_types.term_node ->
(Cil_types.logic_var * bool * int) usage
module ArgPReference: State_builder.Hashtbl(VarType.Hashtbl)(Datatype.Pair(Datatype.Int)(ChainCalls))(sig
val name : string
val dependencies : State.t list
val size : int
end)
module ArgAReference: State_builder.Hashtbl(VarType.Hashtbl)(Datatype.Pair(Datatype.Int)(ChainCalls))(sig
val name : string
val dependencies : State.t list
val size : int
end)
val add_ptr_reference_arg : AnyVar.key -> Datatype.Int.t -> unit
val remove_ptr_reference_arg : ArgPReference.key -> unit
val add_array_reference_arg : AnyVar.key -> Datatype.Int.t -> unit
val remove_array_reference_arg : ArgAReference.key -> unit
val collect_formal_array_call : string ->
ByAReference.key ->
Datatype.Int.t -> Datatype.Bool.t -> VarType.t -> unit
val collect_arg_ptr_call : string ->
AnyVar.key ->
Datatype.Int.t -> Datatype.Bool.t -> VarType.t -> unit
val collect_arg_array_call : string ->
AnyVar.key ->
Datatype.Int.t -> Datatype.Bool.t -> VarType.t -> unit
val collect_formal_ptr_call : string ->
ByPReference.key ->
Datatype.Int.t -> Datatype.Bool.t -> VarType.t -> unit
val collect_calls_rec : Cil_types.exp list * Cil_types.varinfo list -> unit
val collect_calls : Cil_types.varinfo -> Cil_types.exp list -> unit
val ok_array_term_formal : string ->
ByAReference.key ->
Datatype.Int.t -> Datatype.Bool.t -> VarType.t -> unit
val ok_array_term_arg : string ->
AnyVar.key ->
Datatype.Int.t -> Datatype.Bool.t -> VarType.t -> unit
val ok_array_term : string ->
ByAReference.key ->
Datatype.Int.t -> Datatype.Bool.t -> VarType.t -> unit
val ok_ptr_term_formal : string ->
ByPReference.key ->
Datatype.Int.t -> Datatype.Bool.t -> VarType.t -> unit
val ok_ptr_term_arg : string ->
AnyVar.key ->
Datatype.Int.t -> Datatype.Bool.t -> VarType.t -> unit
val ok_pointer_term : string ->
ByPReference.key ->
Datatype.Int.t -> Datatype.Bool.t -> VarType.t -> unit
val collect_apps_rec : Cil_types.term list * Cil_types.logic_var list -> unit
val collect_apps : Cil_types.logic_info -> Cil_types.term list -> unit
val collect_apps_builtin : Cil_types.term list -> unit
val calls_collection_computed : bool Pervasives.ref
class calls_collection : ( object
Inherits

method vinst : Cil_types.instr -> Cil_types.instr list Cil.visitAction
method vterm : Cil_types.term -> Cil_types.term Cil.visitAction
method vpredicate : Cil_types.predicate -> Cil_types.predicate Cil.visitAction
end : object ... end )
val compute_calls_collection : unit -> unit
val by_ptr_reference : ByPReference.key ->
Datatype.Int.t -> ChainCalls.t -> unit
val by_array_reference : ByAReference.key ->
Datatype.Int.t -> ChainCalls.t -> unit
val resolved_call_chain_param : unit -> unit
val ptr_reference : ArgPReference.key ->
Datatype.Int.t ->
(Datatype.Int.t * (bool * ByPReference.key)) list -> unit
val array_reference : ArgAReference.key ->
Datatype.Int.t ->
(Datatype.Int.t * (bool * ByPReference.key)) list -> unit
val resolved_call_chain_arg : unit -> unit
val resolve_addr_taken : unit -> unit
val deref : Cil_datatype.Location.t -> Cil_types.term -> Cil_types.term
type formal_kind = 
| Formal_Value
| Formal_Ref of int
| Formal_Array of int
val kind_of_formal : Cil_types.varinfo -> formal_kind
val collect_sepstars : Cil_datatype.Location.t ->
int -> Cil_types.term -> Cil_types.term list -> Cil_types.term list
val pp_formals : Format.formatter -> Cil_types.varinfo list -> unit
val collect_refparams : Kernel_function.t ->
Cil_datatype.Location.t ->
Cil_types.varinfo list ->
Cil_types.varinfo list ->
Cil_types.term list ->
Cil_types.varinfo list -> Cil_types.identified_predicate option
val emitter : Emitter.t
val add_requires : Cil_types.identified_predicate -> Cil_types.kernel_function -> unit
val kernel_functions_separation_hyps : unit -> unit
type case = 
| All
| Nothing
| Half
val case_of_optimization : logicvar:bool -> refvar:bool -> case
val not_half_computed : unit -> bool
val not_param_computed : unit -> bool
val not_arg_computed : unit -> bool
val not_computed : unit -> bool
val compute : unit -> unit
val dispatch_var : AddrTaken.key -> var_kind
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_user_formal_in_builtin : LogicParam.key -> LogicParam.data
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
val is_memvar : case -> Cil_types.varinfo -> bool
val is_ref : case -> Cil_types.varinfo -> bool
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