functor
(Valuation : sig
type t
type value = value
type origin = bool
type loc = location
val find :
t ->
Cil_types.exp ->
(value, origin) Eval.record_val Eval.or_top
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
end) ->
sig
type state = Cvalue.Model.t
type summary = Cvalue.V_Offsetmap.t option
val update : Valuation.t -> state -> state
val assign :
Cil_types.kinstr ->
location Eval.left_value ->
Cil_types.exp ->
value Eval.assigned -> Valuation.t -> state -> state Eval.or_bottom
val assume :
Cil_types.stmt ->
Cil_types.exp -> bool -> Valuation.t -> state -> state Eval.or_bottom
val summarize :
Cil_types.kernel_function ->
Cil_types.stmt ->
returned:(location Eval.left_value * value Eval.copied) option ->
state -> (summary * state) Eval.or_bottom
val resolve_call :
Cil_types.stmt ->
value Eval.call ->
assigned:(location Eval.left_value * value Eval.copied) option ->
Valuation.t ->
pre:state -> post:summary * state -> state Eval.or_bottom
val default_call :
Cil_types.stmt ->
value Eval.call -> state -> (state, summary, value) Eval.call_result
val call_action :
Cil_types.stmt ->
Cvalue_transfer.value Eval.call ->
Valuation.t ->
state ->
(state, summary, Cvalue_transfer.value) Eval.action * Base.SetLattice.t
end