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
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 |
| |
ByRefArray of int list |
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