sig
module type S =
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
module type Value =
sig
type t
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
val top : t
val is_included : t -> t -> bool
val join : t -> t -> t
val join_and_is_included : t -> t -> t * bool
val narrow : t -> t -> t Eval.or_bottom
val zero : t
val float_zeros : t
val top_int : t
val inject_int : Cil_types.typ -> Integer.t -> t
val all_values : Cil_types.typ -> t
val constant : Cil_types.exp -> Cil_types.constant -> t Eval.evaluated
val forward_unop :
context:Eval.unop_context ->
Cil_types.typ -> Cil_types.unop -> t -> t Eval.evaluated
val forward_binop :
context:Eval.binop_context ->
Cil_types.typ -> Cil_types.binop -> t -> t -> t Eval.evaluated
val backward_binop :
input_type:Cil_types.typ ->
resulting_type:Cil_types.typ ->
Cil_types.binop ->
left:t -> right:t -> result:t -> (t option * t option) Eval.or_bottom
val backward_unop :
typ_arg:Cil_types.typ ->
Cil_types.unop -> arg:t -> res:t -> t option Eval.or_bottom
val backward_cast :
src_typ:Cil_types.typ ->
dst_typ:Cil_types.typ ->
src_val:t -> dst_val:t -> t option Eval.or_bottom
val reinterpret :
Cil_types.exp -> Cil_types.typ -> t -> t Eval.evaluated
val do_promotion :
src_typ:Cil_types.typ ->
dst_typ:Cil_types.typ -> Cil_types.exp -> t -> t Eval.evaluated
val resolve_functions :
typ_pointer:Cil_types.typ ->
t -> Kernel_function.Hptset.t Eval.or_top * bool
val mem : 'a Abstract_value.key -> bool
val get : 'a Abstract_value.key -> (t -> 'a) option
val set : 'a Abstract_value.key -> 'a -> t -> t
val reduce : t -> t
end
module Make :
functor
(Value : Value) (Loc : sig
type value = Value.t
type location
type offset
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 partially_overlap :
location -> location -> bool
val check_non_overlapping :
(Cil_types.lval * location) list ->
(Cil_types.lval * location) list ->
unit Eval.evaluated
val offset_cardinal_zero_or_one :
offset -> bool
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 reduce_index_by_array_size :
size_expr:Cil_types.exp ->
index_expr:Cil_types.exp ->
Integer.t -> value -> value Eval.evaluated
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 reduce_loc_by_validity :
for_writing:bool ->
bitfield:bool ->
Cil_types.lval ->
location -> location Eval.evaluated
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 :
(Cil_types.exp ->
value Eval.evaluated) ->
state ->
Cil_types.exp ->
(value * origin)
Eval.evaluated
val extract_lval :
(Cil_types.exp ->
value Eval.evaluated) ->
state ->
Cil_types.lval ->
Cil_types.typ ->
location ->
(value * origin)
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
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 filter :
(Cil_types.exp -> (value, origin) Eval.record_val -> bool) ->
(Cil_types.lval -> loc Eval.record_loc -> bool) -> t -> t
end
val evaluate :
?valuation:Valuation.t ->
?indeterminate:bool ->
?reduction:bool ->
state -> Cil_types.exp -> (Valuation.t * 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 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