sig
module type Forward_Evaluation =
sig
type value
type valuation
type context
val evaluate :
subdivided:bool ->
Subdivided_evaluation.Forward_Evaluation.context ->
Subdivided_evaluation.Forward_Evaluation.valuation ->
Cil_types.exp ->
(Subdivided_evaluation.Forward_Evaluation.valuation *
Subdivided_evaluation.Forward_Evaluation.value)
Eval.evaluated
end
module Make :
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 replace_base : Base.substitution -> location -> location
val assume_no_overlap :
partial:bool ->
location ->
location -> (location * location) Abstract_location.truth
val assume_valid_location :
for_writing:bool ->
bitfield:bool ->
location -> location Abstract_location.truth
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 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 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 context
val evaluate :
subdivided:bool ->
context ->
Valuation.t ->
Cil_types.exp -> (Valuation.t * Value.t) Eval.evaluated
end)
->
sig
val evaluate :
Eva.context ->
Valuation.t ->
subdivnb:int ->
Cil_types.exp -> (Valuation.t * Value.t) Eval.evaluated
val reduce_by_enumeration :
Eva.context ->
Valuation.t -> Cil_types.exp -> bool -> Valuation.t Eval.or_bottom
end
end