functor
(Value : Abstract_value.External) (Loc : sig
type value = Value.t
type location
type offset
val top : location
val equal_loc :
location -> location -> bool
val equal_offset :
offset -> offset -> bool
val pretty_loc :
Format.formatter ->
location -> unit
val pretty_offset :
Format.formatter ->
offset -> unit
val to_value : location -> value
val size :
location -> Int_Base.t
val partially_overlap :
location -> location -> bool
val check_non_overlapping :
(Cil_types.lval * location)
list ->
(Cil_types.lval * location)
list -> unit Eval.evaluated
val no_offset : offset
val forward_field :
Cil_types.typ ->
Cil_types.fieldinfo ->
offset -> offset
val forward_index :
Cil_types.typ ->
value -> offset -> offset
val reduce_index_by_array_size :
size_expr:Cil_types.exp ->
index_expr:Cil_types.exp ->
Integer.t ->
value -> value Eval.evaluated
val forward_variable :
Cil_types.typ ->
Cil_types.varinfo ->
offset ->
location Eval.or_bottom
val forward_pointer :
Cil_types.typ ->
value ->
offset ->
location Eval.or_bottom
val eval_varinfo :
Cil_types.varinfo -> location
val reduce_loc_by_validity :
for_writing:bool ->
bitfield:bool ->
Cil_types.lval ->
location ->
location Eval.evaluated
val backward_variable :
Cil_types.varinfo ->
location ->
offset Eval.or_bottom
val backward_pointer :
value ->
offset ->
location ->
(value * offset)
Eval.or_bottom
val backward_field :
Cil_types.typ ->
Cil_types.fieldinfo ->
offset ->
offset Eval.or_bottom
val backward_index :
Cil_types.typ ->
index:value ->
remaining:offset ->
offset ->
(value * offset)
Eval.or_bottom
end) (Valuation : sig
type t
type value =
Value.t
type origin
type loc =
Loc.location
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) (Eva :
sig
type state
val evaluate :
?valuation:Valuation.t ->
fuel:int ->
state -> Cil_types.exp -> (Valuation.t * Value.t) Eval.evaluated
end) ->
sig
val evaluate :
?valuation:Valuation.t ->
fuel:int ->
Eva.state -> Cil_types.exp -> (Valuation.t * Value.t) Eval.evaluated
val reduce_by_enumeration :
Valuation.t ->
Eva.state -> Cil_types.exp -> bool -> Valuation.t Eval.or_bottom
end