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 to_domain_valuation :
Evaluation.S.Valuation.t ->
(Evaluation.S.value, Evaluation.S.loc, Evaluation.S.origin)
Abstract_domain.valuation
val evaluate :
?valuation:Evaluation.S.Valuation.t ->
?reduction:bool ->
?subdivnb:int ->
Evaluation.S.state ->
Cil_types.exp ->
(Evaluation.S.Valuation.t * Evaluation.S.value) Eval.evaluated
val copy_lvalue :
?valuation:Evaluation.S.Valuation.t ->
?subdivnb:int ->
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 ->
?subdivnb:int ->
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 eval_function_exp :
?subdivnb:int ->
Cil_types.exp ->
?args:Cil_types.exp list ->
Evaluation.S.state ->
(Kernel_function.t * Evaluation.S.Valuation.t) list Eval.evaluated
val interpret_truth :
alarm:(unit -> Alarms.t) ->
'a -> 'a Abstract_value.truth -> 'a Eval.evaluated
end