Module BufferOverrunDomain.Val

type t = {
  1. itv : Itv.t;
    (*

    Interval

    *)
  2. itv_thresholds : ItvThresholds.t;
  3. itv_updated_by : ItvUpdatedBy.t;
  4. modeled_range : ModeledRange.t;
  5. powloc : AbsLoc.PowLoc.t;
    (*

    Simple pointers

    *)
  6. arrayblk : ArrayBlk.t;
    (*

    Array blocks

    *)
  7. func_ptrs : FuncPtr.Set.t;
    (*

    Function pointers

    *)
  8. 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 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 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 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 -> 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

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_pi : t -> t -> t
val minus_pp : 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 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