sig
type value = Main_values.CVal.t
type location = Main_locations.PLoc.location
module Transfer :
functor
(Valuation : sig
type t
type value = value
type origin = value option
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
val update : Valuation.t -> state -> state Eval.or_bottom
val assign :
Cil_types.kinstr ->
location Eval.left_value ->
Cil_types.exp ->
(location, 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 start_call :
Cil_types.stmt ->
(location, value) Eval.call ->
Valuation.t -> state -> state Eval.or_bottom
val finalize_call :
Cil_types.stmt ->
(location, value) Eval.call ->
pre:state -> post:state -> state Eval.or_bottom
val show_expr :
Valuation.t -> state -> Format.formatter -> Cil_types.exp -> unit
end
end