functor (Value : Value)
(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)
(Domain : sig
type state
type value = Value.t
type location = Loc.location
type origin
val extract_expr :
oracle:(Cil_types.exp -> value Eval.evaluated) ->
Abstract_domain.evaluation_context ->
state ->
Cil_types.exp -> (value * origin option) Eval.evaluated
val extract_lval :
oracle:(Cil_types.exp -> value Eval.evaluated) ->
Abstract_domain.evaluation_context ->
state ->
Cil_types.lval ->
Cil_types.typ ->
location -> (value * origin option) Eval.evaluated
val backward_location :
state ->
Cil_types.lval ->
Cil_types.typ ->
location -> value -> (location * value) Eval.or_bottom
val reduce_further :
state ->
Cil_types.exp -> value -> (Cil_types.exp * value) list
type t = state
val ty : t Type.t
val name : string
val descr : t Descr.t
val packed_descr : Structural_descr.pack
val reprs : t list
val equal : t -> t -> bool
val compare : t -> t -> int
val hash : t -> int
val pretty_code : Format.formatter -> t -> unit
val internal_pretty_code :
Type.precedence -> Format.formatter -> t -> unit
val pretty : Format.formatter -> t -> unit
val varname : t -> string
val mem_project : (Project_skeleton.t -> bool) -> t -> bool
val copy : t -> t
end)
->
sig
type state = Domain.state
type value = Value.t
type origin = Domain.origin
type loc = Loc.location
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 :
Valuation.t -> (value, loc, origin) Abstract_domain.valuation
val evaluate :
?valuation:Valuation.t ->
?reduction:bool ->
?subdivnb:int ->
state -> Cil_types.exp -> (Valuation.t * value) Eval.evaluated
val copy_lvalue :
?valuation:Valuation.t ->
?subdivnb:int ->
state ->
Cil_types.lval ->
(Valuation.t * value Eval.flagged_value) Eval.evaluated
val lvaluate :
?valuation:Valuation.t ->
?subdivnb:int ->
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 eval_function_exp :
?subdivnb:int ->
Cil_types.exp ->
?args:Cil_types.exp list ->
state -> (Kernel_function.t * Valuation.t) list Eval.evaluated
val interpret_truth :
alarm:(unit -> Alarms.t) ->
'a -> 'a Abstract_value.truth -> 'a Eval.evaluated
end