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 remove : t -> Cil_types.exp -> t
val remove_loc : t -> Cil_types.lval -> t
end
val evaluate :
?valuation:Evaluation.S.Valuation.t ->
?reduction:bool ->
Evaluation.S.state ->
Cil_types.exp ->
(Evaluation.S.Valuation.t * Evaluation.S.value) Eval.evaluated
val copy_lvalue :
?valuation:Evaluation.S.Valuation.t ->
Evaluation.S.state ->
Cil_types.lval ->
(Evaluation.S.Valuation.t * Evaluation.S.value Eval.flagged_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 assume :
?valuation:Evaluation.S.Valuation.t ->
Evaluation.S.state ->
Cil_types.exp ->
Evaluation.S.value -> Evaluation.S.Valuation.t Eval.or_bottom
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_non_overlapping :
Evaluation.S.state ->
Cil_types.lval list -> Cil_types.lval list -> unit Eval.evaluated
val eval_function_exp :
Cil_types.exp ->
?args:Cil_types.exp list ->
Evaluation.S.state ->
(Kernel_function.t * Evaluation.S.Valuation.t) list Eval.evaluated
end