Module Checkers.LithoDomain

val is_component_or_section_builder : IR.Typ.Name.t -> IR.Tenv.t -> bool
module LocalAccessPath : sig ... end

Access path + its parent procedure

val suffixes : IStdlib.IStd.String.Set.t
module MethodCallPrefix : sig ... end

Called procedure & location

module Mem : sig ... end
include Absint.AbstractDomain.S
include Absint.AbstractDomain.Comparable
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 subst : callsite:IBase.Location.t -> formals:(IR.Pvar.t * IR.Typ.t) list -> actuals:Absint.HilExp.t list -> ret_id_typ:Absint.AccessPath.base -> caller_pname:IR.Procname.t -> callee_pname:IR.Procname.t -> caller:t -> callee:Mem.t -> t
type summary = Mem.t

type for saving in summary payload

val assign : lhs:LocalAccessPath.t -> rhs:LocalAccessPath.t -> t -> t
val assume_null : LocalAccessPath.t -> t -> t

Semantics of null assume statement, i.e., assume(x==null)

val call_create : LocalAccessPath.t -> IR.Typ.name -> IBase.Location.t -> t -> t

Semantics of builder creation method

val call_builder : ret:LocalAccessPath.t -> receiver:LocalAccessPath.t -> MethodCallPrefix.t -> t -> t

Semantics of builder's methods, e.g. prop

val call_build_method : ret:LocalAccessPath.t -> receiver:LocalAccessPath.t -> t -> t

Semantics of builder's final build method

val call_return : t -> t

Semantics of return method

val pp_summary : Stdlib.Format.formatter -> summary -> unit
val get_summary : is_void_func:bool -> t -> summary
val check_required_props : check_on_string_set: (IR.Typ.name -> IBase.Location.t -> MethodCallPrefix.t list -> IStdlib.IStd.String.Set.t -> unit) -> summary -> summary