Module `BO__BufferOverrunDomain.Mem`

type 'has_oenv t0 = | Unreachable Memory of unreachable node | ExcRaised Memory of node that can be reachable only with exception raises that we want to ignore | Reachable of 'has_oenv MemReach.t0
type no_oenv_t = IStdlib.GOption.none t0: Memory type without an environment for on-demand symbol evaluation

type t = IStdlib.GOption.some t0: 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.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 pp : Stdlib.Format.formatter -> _ t0 -> unit
val unreachable : t

type get_summary = IR.Procname.t -> no_oenv_t option

val init : get_summary -> BO.BufferOverrunOndemandEnv.t -> t
val exc_raised : t
val is_rep_multi_loc : BO.AbsLoc.Loc.t -> _ t0 -> bool: Check if an abstract location represents multiple concrete locations.

val is_stack_loc : BO.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 : BO.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 : BO.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 : BO.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 -> BO.AbsLoc.LocSet.t -> _ t0 -> BO.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 -> BO.AbsLoc.Loc.t -> Val.t -> t -> t: Add an abstract value for stack variables such as n$0

val add_stack_loc : BO.AbsLoc.Loc.t -> t -> t
val add_heap : ?⁠represents_multiple_values:bool -> BO.AbsLoc.Loc.t -> Val.t -> t -> t: Add an abstract value for non-stack variables

val add_heap_set : ?⁠represents_multiple_values:bool -> BO.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_temps : IR.Ident.t list -> t -> t: Remove given temporary variables from the abstract memory

val find : BO.AbsLoc.Loc.t -> _ t0 -> Val.t
val find_opt : BO.AbsLoc.Loc.t -> _ t0 -> Val.t option
val find_set : ?⁠typ:IR.Typ.t -> BO.AbsLoc.PowLoc.t -> _ t0 -> Val.t
val find_stack : BO.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 : BO.AbsLoc.Loc.t -> _ t0 -> AliasTargets.t: Find aliases between given abstract location

val find_simple_alias : IR.Ident.t -> _ t0 -> (BO.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 * BO.AbsLoc.Loc.t * IR.IntLit.t * BO.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.

val find_ret_alias : _ t0 -> AliasRet.t Absint.AbstractDomain.Types.bottom_lifted: Find aliases bound to the return variable

val fgets_alias : IR.Ident.t -> BO.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 -> BO.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 -> BO.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 -> BO.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 -> BO.AbsLoc.Loc.t -> t -> t: Add a size alias between ident and abstract location, i.e., ident == loc.size()

val store_simple_alias : BO.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 : BO.AbsLoc.PowLoc.t -> t -> t: Forget size aliases of given locs

val incr_size_alias : BO.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 : BO.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 : BO.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, it does strong update. Otherwise, weak update.

val strong_update : BO.AbsLoc.PowLoc.t -> Val.t -> t -> t
val update_latest_prune : updated_locs:BO.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) -> BO.AbsLoc.PowLoc.t -> t -> t: Apply f to values bound to given locs