Module BufferOverrunDomain.Mem

type 'has_oenv t0 =
  1. | Unreachable
    (*

    Memory of unreachable node

    *)
  2. | ExcRaised
    (*

    Memory of node that can be reachable only with exception raises that we want to ignore

    *)
  3. | Reachable of 'has_oenv MemReach.t0
type no_oenv_t = IStdlib.GOption.none t0

Memory type without an environment for on-demand symbol evaluation

Memory type with an environment for on-demand symbol evaluation

val unset_oenv : t -> no_oenv_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 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 pp : Stdlib.Format.formatter -> _ t0 -> unit
val unreachable : t
val is_reachable : t -> bool
type get_summary = IR.Procname.t -> no_oenv_t option
val exc_raised : t
val is_rep_multi_loc : AbsLoc.Loc.t -> _ t0 -> bool

Check if an abstract location represents multiple concrete locations.

val is_stack_loc : AbsLoc.Loc.t -> _ t0 -> bool

Check if an abstract location is a stack variable, e.g., n$0.

val set_prune_pairs : PrunePairs.t -> t -> t
val set_latest_prune : LatestPrune.t -> t -> t
val set_first_idx_of_null : AbsLoc.Loc.t -> Val.t -> t -> t

In C string, set the index of the first null character, i.e., end of string, when called by set_first_idx_of_null loc_to_string index_value mem.

val unset_first_idx_of_null : AbsLoc.Loc.t -> Val.t -> t -> t

In C string, unset the index of the first null character, i.e., end of string, when called by unset_first_idx_of_null loc_to_string index_value mem. This is unsound because the index can be assigned as previous index + 1 that is a heuristic to keep string lengths in some loops.

val get_c_strlen : AbsLoc.PowLoc.t -> _ t0 -> Val.t

Get C string length that is set/unset by set_first_idex_of_null and unset_first_idex_of_null

val get_latest_prune : _ t0 -> LatestPrune.t
val get_reachable_locs_from : (IR.Pvar.t * IR.Typ.t) list -> AbsLoc.LocSet.t -> _ t0 -> AbsLoc.LocSet.t

Get reachable locations from formals and locs when called get_reachable_locs_from formals locs mem

val add_stack : ?represents_multiple_values:bool -> AbsLoc.Loc.t -> Val.t -> t -> t

Add an abstract value for stack variables such as n$0

val add_stack_loc : AbsLoc.Loc.t -> t -> t
val add_heap : ?represents_multiple_values:bool -> AbsLoc.Loc.t -> Val.t -> t -> t

Add an abstract value for non-stack variables

val add_heap_set : ?represents_multiple_values:bool -> AbsLoc.PowLoc.t -> Val.t -> t -> t
val add_unknown : (IR.Ident.t * IR.Typ.t) -> location:IBase.Location.t -> t -> t

Add an unknown value for stack variables

val add_unknown_from : (IR.Ident.t * IR.Typ.t) -> callee_pname:IR.Procname.t -> location:IBase.Location.t -> t -> t

Add an unknown return value of callee_pname for stack variables

val remove_vars : IR.Var.t list -> t -> t

Remove temporary variables and if Config.bo_exit_frontend_gener_vars is true also frontend generated variables

val find : AbsLoc.Loc.t -> _ t0 -> Val.t
val find_opt : AbsLoc.Loc.t -> _ t0 -> Val.t option
val find_set : ?typ:IR.Typ.t -> AbsLoc.PowLoc.t -> _ t0 -> Val.t
val find_stack : AbsLoc.Loc.t -> _ t0 -> Val.t
val find_alias_id : IR.Ident.t -> _ t0 -> AliasTargets.t

Find aliases between given ident

val find_alias_loc : AbsLoc.Loc.t -> _ t0 -> AliasTargets.t

Find aliases between given abstract location

val find_simple_alias : IR.Ident.t -> _ t0 -> (AbsLoc.Loc.t * IR.IntLit.t) list

Find simple aliases between given ident. It returns a list of pairs of abstract locations and integer which represent aliases id == x + i.

val find_size_alias : IR.Ident.t -> _ t0 -> (AliasTarget.alias_typ * AbsLoc.Loc.t * IR.IntLit.t * AbsLoc.Loc.t option) list

Find size aliases between given ident. It returns a list of four elements, alias type == or >=, location x, integer i, java temporary variable $irvar0. This represents id == $irvar0 (== or >=) x.size() + i.

Find aliases bound to the return variable

val fgets_alias : IR.Ident.t -> AbsLoc.PowLoc.t -> t -> t

Set fgets alias between an ident and an abstract location

val apply_latest_prune : IR.Exp.t -> t -> t * PrunePairs.t

Apply latest_prunes when given e : Exp.t is true. It returns pruned memory and pairs of pruned locations and values.

val load_alias : IR.Ident.t -> AbsLoc.Loc.t -> AliasTarget.t -> t -> t

Add an alias between ident and abstract location with given alias target

val load_empty_alias : IR.Ident.t -> AbsLoc.Loc.t -> t -> t

Add an empty alias between ident and abstract location, i.e., ident == loc.empty()

val load_simple_alias : IR.Ident.t -> AbsLoc.Loc.t -> t -> t

Add a simple alias between ident and abstract location, i.e., ident == loc

val load_size_alias : IR.Ident.t -> AbsLoc.Loc.t -> t -> t

Add a size alias between ident and abstract location, i.e., ident == loc.size()

val store_simple_alias : AbsLoc.Loc.t -> IR.Exp.t -> t -> t

Add a simple alias between abstract location and expression, i.e., loc == exp

val forget_size_alias : AbsLoc.PowLoc.t -> t -> t

Forget size aliases of given locs

val incr_size_alias : AbsLoc.PowLoc.t -> t -> t

Update size aliases when the size of loc is increased by one. For example if there was an alias ident == loc.size() + i, this changes it to ident == loc.size() + i - 1, since loc.size() has been increased.

val incr_or_not_size_alias : AbsLoc.PowLoc.t -> t -> t

Update size aliases when the size of loc may be increased by one. For example if there was an alias ident == loc.size() + i, this changes it to ident >= loc.size() + i - 1

val add_iterator_has_next_alias : IR.Ident.t -> IR.Exp.t -> t -> t

Add an AliasTarget.IteratorHasNext alias when ident = iterator.hasNext() is called

val add_iterator_next_object_alias : ret_id:IR.Ident.t -> iterator:IR.Ident.t -> t -> t

Add an AliasTarget.IteratorNextObject alias when ident = iterator.nextObject() is called

val incr_iterator_simple_alias_on_call : eval_sym_trace -> callee_exit_mem:no_oenv_t -> t -> t

Update AliasTarget.IteratorSimple alias at function calls

val add_iterator_alias : IR.Ident.t -> t -> t

Add AliasTarget.IteratorSimple and AliasTarget.IteratorOffset aliases when Iteratable.iterator() is called

val incr_iterator_offset_alias : IR.Exp.t -> t -> t

Update iterator offset alias when iterator.next() is called

val update_mem : ?force_strong_update:IStdlib.IStd.Bool.t -> AbsLoc.PowLoc.t -> Val.t -> t -> t

Add a map from locations to a value. If the given set of locations is a singleton set and the only element represents one concrete abstract location or force_strong_update is true, it does strong update. Otherwise, weak update.

val strong_update : AbsLoc.PowLoc.t -> Val.t -> t -> t
val update_latest_prune : updated_locs:AbsLoc.PowLoc.t -> IR.Exp.t -> IR.Exp.t -> t -> t

Update latest prunes when store(x,1) or store(x,0) is called after assume statement

val forget_unreachable_locs : formals:(IR.Pvar.t * IR.Typ.t) list -> t -> t

Forget unreachable locations from formals

val transform_mem : f:(Val.t -> Val.t) -> AbsLoc.PowLoc.t -> t -> t

Apply f to values bound to given locs

val add_cpp_iterator_cmp_alias : IR.Ident.t -> iter_lhs:IR.Pvar.t -> iter_rhs:IR.Pvar.t -> t -> t

Add a compare alias from ret_id to iter_lhs: Pvar.t and iter_rhs: Pvar.t comparison, i.e., ret_id -> {iter_lhs != iter_rhs} where the meaning of != is determined by whether iter_rhs is coming from begin or end

val add_cpp_iter_begin_alias : IR.Pvar.t -> t -> t

Add a begin alias for pvar

val add_cpp_iter_end_alias : IR.Pvar.t -> t -> t

Add a end alias for pvar

val find_cpp_iterator_alias : IR.Ident.t -> t -> (IR.Pvar.t * IR.Pvar.t * IR.Binop.t) option

Find the cpp iterator alias ret_id -> {iter_lhs (binop) iter_rhs}

val propagate_cpp_iter_begin_or_end_alias : new_pvar:IR.Pvar.t -> existing_pvar:IR.Pvar.t -> t -> t

Propagate the being/end alias information from existing to new