functor
(Value : Abstract_value.S) (Location : Abstract_location.External) (Domain :
sig
type state
type value = Value.t
type location = Location.location
type valuation
val update : valuation -> state -> state
val assign :
Cil_types.kinstr ->
location Eval.left_value ->
Cil_types.exp ->
value Eval.assigned -> valuation -> state -> state Eval.or_bottom
val assume :
Cil_types.stmt ->
Cil_types.exp -> bool -> valuation -> state -> state Eval.or_bottom
val start_call :
Cil_types.stmt ->
value Eval.call -> valuation -> state -> state Eval.call_action
val finalize_call :
Cil_types.stmt ->
value Eval.call -> pre:state -> post:state -> state Eval.or_bottom
val approximate_call :
Cil_types.stmt -> value Eval.call -> state -> state list Eval.or_bottom
val leave_scope :
Cil_types.kernel_function -> Cil_types.varinfo list -> state -> state
module Store :
sig
val register_initial_state : Value_types.callstack -> state -> unit
val register_state_before_stmt :
Value_types.callstack -> Cil_types.stmt -> state -> unit
val register_state_after_stmt :
Value_types.callstack -> Cil_types.stmt -> state -> unit
val get_initial_state :
Cil_types.kernel_function -> state Eval.or_bottom
val get_initial_state_by_callstack :
Cil_types.kernel_function ->
state Value_types.Callstack.Hashtbl.t option
val get_stmt_state : Cil_types.stmt -> state Eval.or_bottom
val get_stmt_state_by_callstack :
after:bool ->
Cil_types.stmt -> state Value_types.Callstack.Hashtbl.t option
end
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
end) (Init : sig
val initial_state :
lib_entry:bool -> Domain.state Bottom.Type.or_bottom
val initial_state_with_formals :
lib_entry:bool ->
Cil_types.kernel_function ->
Domain.state Bottom.Type.or_bottom
val initialize_var :
with_alarms:CilE.warn_mode ->
Cil_types.stmt ->
Cil_types.varinfo ->
Cil_types.init ->
Domain.state -> Domain.state Bottom.Type.or_bottom
end) (Eva : sig
type state = Domain.state
type value = Domain.value
type origin
type loc = Domain.location
module Valuation :
sig
type t = Domain.valuation
type value = value
type origin = origin
type loc = loc
val empty : t
val find :
t ->
Cil_types.exp ->
(value, origin) Eval.record_val
Eval.or_top
val add :
t ->
Cil_types.exp ->
(value, origin) Eval.record_val -> t
val fold :
(Cil_types.exp ->
(value, origin) Eval.record_val ->
'a -> 'a) ->
t -> 'a -> 'a
val find_loc :
t ->
Cil_types.lval ->
loc Eval.record_loc Eval.or_top
val remove : t -> Cil_types.exp -> t
val remove_loc : t -> Cil_types.lval -> t
end
val evaluate :
?valuation:Valuation.t ->
?reduction:bool ->
state ->
Cil_types.exp ->
(Valuation.t * value) Eval.evaluated
val copy_lvalue :
?valuation:Valuation.t ->
state ->
Cil_types.lval ->
(Valuation.t * value Eval.flagged_value)
Eval.evaluated
val lvaluate :
?valuation:Valuation.t ->
for_writing:bool ->
state ->
Cil_types.lval ->
(Valuation.t * loc * Cil_types.typ)
Eval.evaluated
val can_copy :
?valuation:Valuation.t ->
is_ret:bool ->
state ->
Kernel_function.t ->
Cil_types.lval ->
Cil_types.exp ->
(Cil_types.lval option * Valuation.t)
Eval.evaluated
val reduce :
?valuation:Valuation.t ->
state ->
Cil_types.exp ->
bool -> Valuation.t Eval.evaluated
val assume :
?valuation:Valuation.t ->
state ->
Cil_types.exp ->
value -> Valuation.t Eval.or_bottom
val split_by_evaluation :
Cil_types.exp ->
Integer.t list ->
state list ->
(Integer.t * state list * bool) list *
state list
val check_copy_lval :
Cil_types.lval * loc ->
Cil_types.lval * loc -> bool Eval.evaluated
val check_non_overlapping :
state ->
Cil_types.lval list ->
Cil_types.lval list -> unit Eval.evaluated
val eval_function_exp :
Cil_types.exp ->
state ->
(Kernel_function.t * Valuation.t) list
Eval.evaluated
end) ->
sig
type state = Domain.state
type value = Domain.value
val init :
with_alarms:CilE.warn_mode ->
state ->
Cil_types.kernel_function ->
Cil_types.stmt ->
Cil_types.varinfo -> Cil_types.init -> state Eval.or_bottom
val assign :
with_alarms:CilE.warn_mode ->
state ->
Cil_types.kernel_function ->
Cil_types.stmt ->
Cil_types.lval -> Cil_types.exp -> state Eval.or_bottom
val assume :
with_alarms:CilE.warn_mode ->
state ->
Cil_types.stmt -> Cil_types.exp -> bool -> state Eval.or_bottom
val call :
with_alarms:CilE.warn_mode ->
Cil_types.stmt ->
Cil_types.lval option ->
Cil_types.exp ->
Cil_types.exp list ->
state -> state list Eval.or_bottom * Value_types.cacheable
val split_final_states :
Cil_types.kernel_function ->
Cil_types.exp -> Integer.t list -> state list -> state list list
val check_unspecified_sequence :
with_alarms:CilE.warn_mode ->
Cil_types.stmt ->
state ->
(Cil_types.stmt * Cil_types.lval list * Cil_types.lval list *
Cil_types.lval list * Cil_types.stmt ref list)
list -> unit Eval.or_bottom
type call_result = {
states : state list Eval.or_bottom;
cacheable : Value_types.cacheable;
}
val compute_call_ref :
(Cil_types.kinstr -> value Eval.call -> state -> call_result) ref
end