Module BO__AbsLoc.Loc
type prim
= private
|
Var of IR.Var.t
|
Allocsite of Allocsite.t
type t
= prim BO.BufferOverrunField.t
include IStdlib.PrettyPrintable.PrintableOrderedType with type PrintableOrderedType.t := t
include IStdlib.PrettyPrintable.PrintableType with type t := t
val pp : IStdlib.PrettyPrintable.F.formatter -> t -> unit
val of_allocsite : Allocsite.t -> t
val of_c_strlen : t -> t
It appends the
strlen
field.
val of_id : IR.Ident.t -> t
val of_path : BO.Symb.SymbolPath.partial -> t
val of_pvar : IR.Pvar.t -> t
val of_var : IR.Var.t -> t
val unknown : t
val exists_pvar : f:(IR.Pvar.t -> bool) -> t -> bool
It checks if a pvar in location satisfies
f
.
val exists_str : f:(string -> bool) -> t -> bool
It checks if a variable or a field name in the location path satisfies
f
.
val get_literal_string : t -> string option
val get_literal_string_strlen : t -> string option
val get_path : t -> BO.Symb.SymbolPath.partial option
val is_field_of : loc:t -> field_loc:t -> bool
It checks if
loc
is prefix offield_loc
.
val is_frontend_tmp : t -> bool
val is_global : t -> bool
val get_global_array_initializer : t -> IR.Procname.t option
Return the name of global initializer when given abstract location represents a global constant array value
val is_pretty : t -> bool
It checks if it is representable with pretty form, e.g., with a path or with a variable name.