sig
module type S =
sig
type state
type value
type summary
val assign :
with_alarms:CilE.warn_mode ->
Transfer_stmt.S.state ->
Cil_types.kernel_function ->
Cil_types.stmt ->
Cil_types.lval ->
Cil_types.exp -> Transfer_stmt.S.state Eval.or_bottom
val assume :
with_alarms:CilE.warn_mode ->
Transfer_stmt.S.state ->
Cil_types.stmt ->
Cil_types.exp -> bool -> Transfer_stmt.S.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 ->
Transfer_stmt.S.state ->
Transfer_stmt.S.state list Eval.or_bottom * Value_types.cacheable
val return :
with_alarms:CilE.warn_mode ->
Cil_types.kernel_function ->
Cil_types.stmt ->
Cil_types.lval option ->
Transfer_stmt.S.state ->
(Transfer_stmt.S.state, Transfer_stmt.S.summary,
Transfer_stmt.S.value)
Eval.return Eval.or_bottom
val split_final_states :
Cil_types.kernel_function ->
Cil_types.exp ->
Integer.t list ->
Transfer_stmt.S.state list -> Transfer_stmt.S.state list list
val check_unspecified_sequence :
with_alarms:CilE.warn_mode ->
Transfer_stmt.S.state ->
(Cil_types.stmt * Cil_types.lval list * Cil_types.lval list *
Cil_types.lval list * Cil_types.stmt Pervasives.ref list)
list -> unit Eval.or_bottom
type res =
(Transfer_stmt.S.state, Transfer_stmt.S.summary,
Transfer_stmt.S.value)
Eval.call_result * Value_types.cacheable
val compute_call_ref :
(Cil_types.kinstr ->
Transfer_stmt.S.value Eval.call ->
Transfer_stmt.S.state -> Transfer_stmt.S.res)
Pervasives.ref
end
module Make :
functor
(Domain : Abstract_domain.Transfer) (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 filter :
(Cil_types.exp ->
(value, origin)
Eval.record_val ->
bool) ->
(Cil_types.lval ->
loc Eval.record_loc ->
bool) ->
t -> t
end
val evaluate :
?valuation:Valuation.t ->
?indeterminate:bool ->
?reduction:bool ->
state ->
Cil_types.exp ->
(Valuation.t * 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 loc_size :
loc -> Int_Base.t
val reinterpret :
Cil_types.exp ->
Cil_types.typ ->
value ->
value Eval.evaluated
val do_promotion :
src_typ:Cil_types.typ ->
dst_typ:Cil_types.typ ->
Cil_types.exp ->
value ->
value Eval.evaluated
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
type summary = Domain.summary
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 return :
with_alarms:CilE.warn_mode ->
Cil_types.kernel_function ->
Cil_types.stmt ->
Cil_types.lval option ->
state -> (state, summary, value) Eval.return Eval.or_bottom
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 ->
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 res =
(state, summary, value) Eval.call_result * Value_types.cacheable
val compute_call_ref :
(Cil_types.kinstr -> value Eval.call -> state -> res) ref
end
end