Module VarUsage

module VarUsage: sig .. end
Usage Variable Analysis

module WpMain: Wp_parameters
val dkey : Log.category
exception NoSize
val pp_box : Format.formatter -> int list -> unit
val pp_dim : Format.formatter -> int list -> unit
val size_of_char : char -> Integer.t
val size : Cil_types.exp -> Integer.t
val size_int : Cil_types.exp -> int
val _merge_dim : 'a list -> 'a list -> 'a list
val merge_box : 'a list -> 'a list -> 'a list
val leq_box : 'a list -> 'a list -> bool
val addbox_of_type : int list -> Cil_types.typ -> int list
val box_of_type : Cil_types.typ -> int list
val dim_of_type : Cil_types.typ -> int list
val cells_in_type : Cil_types.typ -> Integer.t
Number of cells in the type (raise NoSize for unknown size)
val type_of_cells : Cil_types.typ -> Cil_types.typ
Type of multi-dimensional array cells
val alloc_for_type : Cil_types.typ -> int list
Size of dimensions in the type (0 for unknown size)
val degree_of_type : Cil_types.typ -> int
Dimensions in the type (0 for non-array)
val shape : Cil_types.typ -> (Cil_types.typ * int list) option
val compatible : Cil_types.typ -> Cil_types.typ -> bool
val reshape : Cil_types.typ -> Cil_types.typ -> int list option
module Root: sig .. end
module Model: sig .. end
module Context: sig .. end
module Usage: sig .. end
module Occur: sig .. end
module Omap: FCMap.Make(Root)
module Domain: Datatype.Make(sig
type t = VarUsage.Occur.t VarUsage.Omap.t 
include Datatype.Serializable_undefined
val reprs : 'a VarUsage.Omap.t list
val name : string
end)
module U: State_builder.Ref(Domain)(sig
val name : string
val dependencies : State.t list
val default : unit -> 'a VarUsage.Omap.t
end)
val occur : Omap.key -> Occur.t
val get_formal : Omap.key -> Usage.domain
val occurrence : Context.target * Context.delta list ->
Omap.key -> unit
val fixpoint : unit -> unit
val expr : Context.t -> Cil_types.exp -> unit
val lvalue : Context.t -> Cil_types.lval -> unit
val lval_option : Context.t -> Cil_types.lval option -> unit
val lval_host : Context.t -> Cil_types.lhost -> unit
val lval_offset : Context.t -> Cil_types.typ -> Cil_types.offset -> Context.t
val funcall_params : Cil_types.kernel_function ->
Cil_types.varinfo list -> Cil_types.exp list -> unit
val funcall : Cil_types.exp -> Cil_types.exp list -> unit
val term : Context.t -> Cil_types.term -> unit
val term_option : Context.t -> Cil_types.term option -> unit
val term_lval : Context.t -> Cil_types.term_lval -> unit
val term_coffset : Context.t ->
Cil_types.typ -> Cil_types.term_offset -> Context.t
val term_indices : Cil_types.term_offset -> unit
val term_host : Context.t -> Cil_types.term_lhost -> unit
val logic_call : Cil_types.logic_info ->
Cil_types.logic_var list -> Cil_types.term list -> unit
val identified_term : Context.t -> Cil_types.identified_term -> unit
val named_predicate : Cil_types.predicate Cil_types.named -> unit
val predicate : Cil_types.predicate -> unit
val logic_body : Cil_types.logic_body -> unit
class visitor : object .. end
val compute : unit -> unit
val of_cvar : Cil_types.varinfo -> usage
val of_formal : Cil_types.varinfo -> usage
val of_lvar : Cil_types.logic_var -> usage
val validated_cvar : Cil_types.varinfo -> bool
val validated_lvar : Cil_types.logic_var -> bool
val dump_lvar : Format.formatter -> Cil_types.logic_var -> unit
val dump : unit -> unit
type usage = 
| NotUsed
| ByValue
| ByAddress
| ByReference
| ByArray of int list (*Dimension*)
| ByRefArray of int list (*Dimension*)
val usage : Usage.domain -> usage
val of_cvar : Cil_types.varinfo -> usage
val of_formal : Cil_types.varinfo -> usage
val of_lvar : Cil_types.logic_var -> usage
val validated_cvar : Cil_types.varinfo -> bool
val validated_lvar : Cil_types.logic_var -> bool
val pretty : name:string -> Format.formatter -> usage -> unit