Module 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 : BO.FuncPtr.Set.t;

Function pointers

traces : BufferOverrunTrace.Set.t;
}
include Absint.AbstractDomain.S with type t := t
include Absint.AbstractDomain.NoJoin
include IStdlib.PrettyPrintable.PrintableType
type t
val pp : IStdlib.PrettyPrintable.F.formatter -> t -> unit
val leq : lhs:t -> rhs:t -> bool

the implication relation: lhs <= rhs means lhs |- rhs

val join : t -> t -> t
val widen : prev:t -> next:t -> num_iters:int -> t
val bot : 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.Typ.IntegerWidths.t -> string -> t
val of_loc : ?⁠traces:BufferOverrunTrace.Set.t -> AbsLoc.Loc.t -> t
val of_pow_loc : traces:BufferOverrunTrace.Set.t -> AbsLoc.PowLoc.t -> t
val of_func_ptrs : BO.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_mone : t -> bool

Check if the value is [-1,-1]

val array_sizeof : t -> Itv.t

Get array size

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
val get_range_of_iterator : t -> t

Get a range of an iterator value, for example, if iterator value is [lb,ub], it returns [0,ub].

val get_itv : t -> Itv.t
val get_modeled_range : t -> ModeledRange.t
val get_pow_loc : t -> AbsLoc.PowLoc.t
val get_func_ptrs : t -> BO.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_array_stride : Z.t -> t -> t
val set_itv_updated_by_addition : t -> t
val set_itv_updated_by_multiplication : t -> t
val set_itv_updated_by_unknown : t -> t
val set_modeled_range : ModeledRange.t -> t -> t
val (lnot) : t -> t
val neg : 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 plus_pi : t -> t -> t
val minus_a : ?⁠f_trace:(BufferOverrunTrace.Set.t -> BufferOverrunTrace.Set.t -> BufferOverrunTrace.Set.t) -> t -> t -> t
val minus_pi : t -> t -> t
val minus_pp : 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 lt_sem : t -> t -> t
val gt_sem : t -> t -> t
val le_sem : t -> t -> t
val ge_sem : t -> t -> t
val eq_sem : t -> t -> t
val ne_sem : t -> t -> t
val band_sem : ?⁠f_trace:(BufferOverrunTrace.Set.t -> BufferOverrunTrace.Set.t -> BufferOverrunTrace.Set.t) -> t -> t -> t
val land_sem : t -> t -> t
val lor_sem : t -> t -> t
val unknown_bit : t -> t

Semantic function for some bit operators which are hard to express in the domain, e.g., Unop.BNot.

val prune_eq : t -> t -> t

Pruning semantics for Binop.Eq. This prunes value of x when given x == y, i.e., prune_eq x y.

val prune_ne : t -> t -> t

Pruning semantics for Binop.Ne. This prunes value of x when given x != y, i.e., prune_ne x y.

val prune_lt : t -> t -> t

Pruning semantics for Binop.Lt. This prunes value of x when given x < y, i.e., prune_lt x y.

val prune_ne_zero : t -> t

Prune value of x when given x != 0

val prune_eq_zero : t -> t

Prune value of x when given x == 0

val prune_ge_one : t -> t

Prune value of x when given x >= 1

val prune_length_lt : t -> Itv.t -> t

Prune length of x when given x.length() < i

val prune_length_le : t -> Itv.t -> t

Prune length of x when given x.length() <= i

val prune_length_eq : t -> Itv.t -> t

Prune length of x when given x.length() == i

val prune_length_eq_zero : t -> t

Prune length of x when given x.length() == 0

val prune_length_ge_one : t -> t

Prune length of x when given x.length() >= 1

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

val cast : IR.Typ.t -> t -> t

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