BufferOverrunDomain.Val
type t = {
itv : Itv.t;
Interval
*)itv_thresholds : ItvThresholds.t;
itv_updated_by : ItvUpdatedBy.t;
modeled_range : ModeledRange.t;
powloc : AbsLoc.PowLoc.t;
Simple pointers
*)arrayblk : ArrayBlk.t;
Array blocks
*)func_ptrs : FuncPtr.Set.t;
Function pointers
*)traces : BufferOverrunTrace.Set.t;
}
include Absint.AbstractDomain.S with type t := t
include Absint.AbstractDomain.Comparable with type t := t
include IStdlib.PrettyPrintable.PrintableType with type t := t
val pp : IStdlib.PrettyPrintable.F.formatter -> t -> unit
val bot : t
val unknown : t
val of_big_int : ItvThresholds.elt -> t
val of_c_array_alloc :
AbsLoc.Allocsite.t ->
stride:int option ->
offset:Itv.t ->
size:Itv.t ->
traces:BufferOverrunTrace.Set.t ->
t
Construct C array allocation. stride
is a byte size of cell, offset
is initial offset of pointer which is usually zero, and size
is a total number of cells.
val of_java_array_alloc :
AbsLoc.Allocsite.t ->
length:Itv.t ->
traces:BufferOverrunTrace.Set.t ->
t
Construct Java array allocation. size
is a total number of cells
val of_int : int -> t
val of_int_lit : IR.IntLit.t -> t
val of_itv : ?traces:BufferOverrunTrace.Set.t -> Itv.t -> t
val of_literal_string : IR.IntegerWidths.t -> string -> t
val of_loc : ?traces:BufferOverrunTrace.Set.t -> AbsLoc.Loc.t -> t
Create a value for a pointer pointing to x.
val of_pow_loc : traces:BufferOverrunTrace.Set.t -> AbsLoc.PowLoc.t -> t
Create a value for a pointer pointing to locations in powloc.
val of_func_ptrs : FuncPtr.Set.t -> t
val unknown_locs : t
val unknown_from :
IR.Typ.t ->
callee_pname:IR.Procname.t option ->
location:IBase.Location.t ->
t
Unknown return value of callee_pname
val is_bot : t -> bool
Check if the value is bottom
val is_unknown : t -> bool
Return true if the value represents an unknown value. Note that this does not mean that it is identical with Dom.Val.unknown. This is because an unknown value is bound to a particular location (this affects fields sym, offset_sym, and size_sym - see MemReach.add_heap) and a to particular assignment (this affects the field traces - see Val.add_assign_trace_elem).
val is_mone : t -> bool
Check if the value is [-1,-1]
val get_all_locs : t -> AbsLoc.PowLoc.t
Get all locations, including pointers and array blocks
val get_array_locs : t -> AbsLoc.PowLoc.t
Get locations of array blocks
val get_array_blk : t -> ArrayBlk.t
Get a range of an iterator value, for example, if iterator value is [lb,ub]
, it returns [0,ub]
.
val get_modeled_range : t -> ModeledRange.t
val get_pow_loc : t -> AbsLoc.PowLoc.t
val get_func_ptrs : t -> FuncPtr.Set.t
val get_traces : t -> BufferOverrunTrace.Set.t
val set_array_length : IBase.Location.t -> length:t -> t -> t
val set_array_offset : IBase.Location.t -> Itv.t -> t -> t
val set_modeled_range : ModeledRange.t -> t -> t
val plus_a :
?f_trace:
(BufferOverrunTrace.Set.t ->
BufferOverrunTrace.Set.t ->
BufferOverrunTrace.Set.t) ->
t ->
t ->
t
Semantics of Binop.PlusA
. f_trace
merges traces of the operands. If f_trace
is not given, it uses a default heuristic merge function.
val minus_a :
?f_trace:
(BufferOverrunTrace.Set.t ->
BufferOverrunTrace.Set.t ->
BufferOverrunTrace.Set.t) ->
t ->
t ->
t
val mult :
?f_trace:
(BufferOverrunTrace.Set.t ->
BufferOverrunTrace.Set.t ->
BufferOverrunTrace.Set.t) ->
t ->
t ->
t
val div :
?f_trace:
(BufferOverrunTrace.Set.t ->
BufferOverrunTrace.Set.t ->
BufferOverrunTrace.Set.t) ->
t ->
t ->
t
val mod_sem :
?f_trace:
(BufferOverrunTrace.Set.t ->
BufferOverrunTrace.Set.t ->
BufferOverrunTrace.Set.t) ->
t ->
t ->
t
val shiftlt :
?f_trace:
(BufferOverrunTrace.Set.t ->
BufferOverrunTrace.Set.t ->
BufferOverrunTrace.Set.t) ->
t ->
t ->
t
val shiftrt :
?f_trace:
(BufferOverrunTrace.Set.t ->
BufferOverrunTrace.Set.t ->
BufferOverrunTrace.Set.t) ->
t ->
t ->
t
val band_sem :
?f_trace:
(BufferOverrunTrace.Set.t ->
BufferOverrunTrace.Set.t ->
BufferOverrunTrace.Set.t) ->
t ->
t ->
t
Semantic function for some bit operators which are hard to express in the domain, e.g., Unop.BNot
.
Pruning semantics for Binop.Eq
. This prunes value of x
when given x == y
, i.e., prune_eq x y
.
Pruning semantics for Binop.Ne
. This prunes value of x
when given x != y
, i.e., prune_ne x y
.
Pruning semantics for Binop.Lt
. This prunes value of x
when given x < y
, i.e., prune_lt x y
.
val prune_binop : IR.Binop.t -> t -> t -> t
Prune value of x
when given x bop y
, i.e., prune_binop bop x y
val add_assign_trace_elem : IBase.Location.t -> AbsLoc.PowLoc.t -> t -> t
Add assign trace for given abstract locations
Semantics of cast. This updates type information in pointer values, rather than re-calculating sizes of array blocks.
val subst : t -> eval_sym_trace -> IBase.Location.t -> t
Substitution of symbols in the value
val transform_array_length : IBase.Location.t -> f:(Itv.t -> Itv.t) -> t -> t
Apply f
on array lengths in the value
module Itv : sig ... end