sig
type state
type value
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 filter :
(Cil_types.exp -> (value, origin) Eval.record_val -> bool) ->
(Cil_types.lval -> loc Eval.record_loc -> bool) -> t -> t
end
val evaluate :
?valuation:Evaluation.S.Valuation.t ->
?indeterminate:bool ->
?reduction:bool ->
Evaluation.S.state ->
Cil_types.exp ->
(Evaluation.S.Valuation.t * Evaluation.S.value) Eval.evaluated
val lvaluate :
?valuation:Evaluation.S.Valuation.t ->
for_writing:bool ->
Evaluation.S.state ->
Cil_types.lval ->
(Evaluation.S.Valuation.t * Evaluation.S.loc * Cil_types.typ)
Eval.evaluated
val reduce :
?valuation:Evaluation.S.Valuation.t ->
Evaluation.S.state ->
Cil_types.exp -> bool -> Evaluation.S.Valuation.t Eval.evaluated
val loc_size : Evaluation.S.loc -> Int_Base.t
val reinterpret :
Cil_types.exp ->
Cil_types.typ -> Evaluation.S.value -> Evaluation.S.value Eval.evaluated
val do_promotion :
src_typ:Cil_types.typ ->
dst_typ:Cil_types.typ ->
Cil_types.exp -> Evaluation.S.value -> Evaluation.S.value Eval.evaluated
val split_by_evaluation :
Cil_types.exp ->
Integer.t list ->
Evaluation.S.state list ->
(Integer.t * Evaluation.S.state list * bool) list *
Evaluation.S.state list
val check_copy_lval :
Cil_types.lval * Evaluation.S.loc ->
Cil_types.lval * Evaluation.S.loc -> bool Eval.evaluated
val check_non_overlapping :
Evaluation.S.state ->
Cil_types.lval list -> Cil_types.lval list -> unit Eval.evaluated
val eval_function_exp :
Cil_types.exp ->
Evaluation.S.state ->
(Kernel_function.t * Evaluation.S.Valuation.t) list Eval.evaluated
end