sig
module Make :
functor
(Value : Abstract_value.External) (Eva : sig
type state
type value = Value.t
type origin
type loc
module Valuation :
sig
type t
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 remove :
t ->
Cil_types.exp -> t
val remove_loc :
t ->
Cil_types.lval -> t
end
val evaluate :
?valuation:Valuation.t ->
?reduction:bool ->
state ->
Cil_types.exp ->
(Valuation.t * value)
Eval.evaluated
val copy_lvalue :
?valuation:Valuation.t ->
state ->
Cil_types.lval ->
(Valuation.t *
value Eval.flagged_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 assume :
?valuation:Valuation.t ->
state ->
Cil_types.exp ->
value ->
Valuation.t Eval.or_bottom
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 = Eva.state
type value = Value.t
type origin = Eva.origin
type loc = Eva.loc
module Valuation :
sig
type t
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 remove : t -> Cil_types.exp -> t
val remove_loc : t -> Cil_types.lval -> t
end
val evaluate :
?valuation:Valuation.t ->
?reduction:bool ->
state -> Cil_types.exp -> (Valuation.t * value) Eval.evaluated
val copy_lvalue :
?valuation:Valuation.t ->
state ->
Cil_types.lval ->
(Valuation.t * value Eval.flagged_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 assume :
?valuation:Valuation.t ->
state -> Cil_types.exp -> value -> Valuation.t Eval.or_bottom
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
end