sig
module type S =
sig
type state
val initial_state :
lib_entry:bool -> Initialization.S.state Bottom.Type.or_bottom
val initial_state_with_formals :
lib_entry:bool ->
Cil_types.kernel_function ->
Initialization.S.state Bottom.Type.or_bottom
val initialize_local_variable :
Cil_types.stmt ->
Cil_types.varinfo ->
Cil_types.init ->
Initialization.S.state ->
Initialization.S.state Bottom.Type.or_bottom
end
module Make :
functor (Domain : Abstract.Domain.External)
(Eva : sig
type state = Domain.state
type value
type origin
type loc = Domain.location
module Valuation :
sig
type t
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 to_domain_valuation :
Valuation.t ->
(value, loc, origin) Abstract_domain.valuation
val evaluate :
?valuation:Valuation.t ->
?reduction:bool ->
?subdivnb:int ->
state ->
Cil_types.exp -> (Valuation.t * value) Eval.evaluated
val copy_lvalue :
?valuation:Valuation.t ->
?subdivnb:int ->
state ->
Cil_types.lval ->
(Valuation.t * value Eval.flagged_value) Eval.evaluated
val lvaluate :
?valuation:Valuation.t ->
?subdivnb:int ->
for_writing:bool ->
state ->
Cil_types.lval ->
(Valuation.t * loc * Cil_types.typ) 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 eval_function_exp :
?subdivnb:int ->
Cil_types.exp ->
?args:Cil_types.exp list ->
state ->
(Kernel_function.t * Valuation.t) list Eval.evaluated
val interpret_truth :
alarm:(unit -> Alarms.t) ->
'a -> 'a Abstract_value.truth -> 'a Eval.evaluated
end)
(Transfer : sig
type state = Domain.t
type value
type loc
val assign :
state ->
Cil_types.kinstr ->
Cil_types.lval -> Cil_types.exp -> state Eval.or_bottom
val assume :
state ->
Cil_types.stmt ->
Cil_types.exp -> bool -> state Eval.or_bottom
val call :
Cil_types.stmt ->
Cil_types.lval option ->
Cil_types.exp ->
Cil_types.exp list ->
state -> (Partition.key * state) list * Eval.cacheable
val check_unspecified_sequence :
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
val enter_scope :
Cil_types.kernel_function ->
Cil_types.varinfo list -> state -> state
type call_result = {
states : (Partition.key * state) list;
cacheable : Eval.cacheable;
builtin : bool;
}
val compute_call_ref :
(Cil_types.stmt ->
(loc, value) Eval.call ->
Eval.recursion option -> state -> call_result)
ref
end)
->
sig
val initial_state : lib_entry:bool -> Domain.t Bottom.Type.or_bottom
val initial_state_with_formals :
lib_entry:bool ->
Cil_types.kernel_function -> Domain.t Bottom.Type.or_bottom
val initialize_local_variable :
Cil_types.stmt ->
Cil_types.varinfo ->
Cil_types.init -> Domain.t -> Domain.t Bottom.Type.or_bottom
end
end