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 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 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 :
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 location
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 ->
state
list
Eval.or_bottom *
Value_types.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 :
state
list
Eval.or_bottom;
cacheable :
Value_types.cacheable;
builtin :
bool;
}
val compute_call_ref :
(Cil_types.stmt ->
(location,
value)
Eval.call ->
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