sig
type state = G.t
type t = state
val ty : t Type.t
val name : string
val descr : t Descr.t
val packed_descr : Structural_descr.pack
val reprs : t list
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val pretty_code : Format.formatter -> t -> unit
val internal_pretty_code : Type.precedence -> Format.formatter -> t -> unit
val pretty : Format.formatter -> t -> unit
val varname : t -> string
val mem_project : (Project_skeleton.t -> bool) -> t -> bool
val copy : t -> t
module Set = D_Impl.Set
module Map = D_Impl.Map
module Hashtbl = D_Impl.Hashtbl
val top : t
val is_included : t -> t -> bool
val join : t -> t -> t
val join_and_is_included : t -> t -> t * bool
val widen : Cil_types.kernel_function -> Cil_types.stmt -> t -> t -> t
type value = Cvalue.V.t
type location = Precise_locs.precise_location
type origin = D_Impl.origin
val extract_expr :
(Cil_types.exp -> value Eval.evaluated) ->
t -> Cil_types.exp -> (value * origin) Eval.evaluated
val extract_lval :
(Cil_types.exp -> value Eval.evaluated) ->
t ->
Cil_types.lval ->
Cil_types.typ -> location -> (value * origin) Eval.evaluated
val backward_location :
t ->
Cil_types.lval ->
Cil_types.typ -> location -> value -> (location * value) Eval.or_bottom
val reduce_further :
t -> Cil_types.exp -> value -> (Cil_types.exp * value) list
type return = D_Impl.return
module Return = D_Impl.Return
module Transfer = D_Impl.Transfer
val compute_using_specification :
Cil_types.kinstr ->
Cil_types.kernel_function * Cil_types.funspec ->
t -> (t, return, value) Eval.call_result
type eval_env = D_Impl.eval_env
val env_current_state : eval_env -> t Eval.or_bottom
val env_annot : pre:t -> here:t -> unit -> eval_env
val env_pre_f : pre:t -> unit -> eval_env
val env_post_f :
pre:t -> post:t -> result:Cil_types.varinfo option -> unit -> eval_env
val eval_predicate : eval_env -> Cil_types.predicate -> Alarmset.status
val reduce_by_predicate :
eval_env -> bool -> Cil_types.predicate -> eval_env
val enter_scope :
Cil_types.kernel_function -> Cil_types.varinfo list -> t -> t
val leave_scope :
Cil_types.kernel_function -> Cil_types.varinfo list -> t -> t
val empty : unit -> t
val initialize_var :
t -> Cil_types.lval -> location -> (value * bool) Eval.or_bottom -> t
val initialize_var_using_type : t -> Cil_types.varinfo -> t
val global_state : unit -> t Eval.or_bottom option
val filter_by_bases : Base.Hptset.t -> t -> t
val reuse : current_input:t -> previous_output:t -> t
val structure : t Abstract_domain.structure
module Store :
sig
val register_initial_state : Value_types.callstack -> G.t -> unit
val register_state_before_stmt :
Value_types.callstack -> Cil_types.stmt -> G.t -> unit
val register_state_after_stmt :
Value_types.callstack -> Cil_types.stmt -> G.t -> unit
val get_initial_state : Cil_types.kernel_function -> G.t Eval.or_bottom
val get_initial_state_by_callstack :
Cil_types.kernel_function ->
G.t Value_types.Callstack.Hashtbl.t option
val get_stmt_state : Cil_types.stmt -> G.t Eval.or_bottom
val get_stmt_state_by_callstack :
after:bool ->
Cil_types.stmt -> G.t Value_types.Callstack.Hashtbl.t option
end
end