PulseNonDisjunctiveDomain (infer.Pulselib.PulseNonDisjunctiveDomain)

module BaseMemory = PulseBaseMemory

module DecompilerExpr = PulseDecompilerExpr

module ExecutionDomain = PulseExecutionDomain

module PathContext = PulsePathContext

type copy_spec_t =

| Copied of {
1. source_typ : IR.Typ.t option;
2. source_opt : DecompilerExpr.source_expr option;
3. location : IBase.Location.t;
4. copied_location : (IR.Procname.t * IBase.Location.t) option;
5. heap : BaseMemory.t;
6. from : Pulselib.PulseBasicInterface.Attribute.CopyOrigin.t;
7. timestamp : Pulselib.PulseBasicInterface.Timestamp.t;
}
| Modified of {
1. source_typ : IR.Typ.t option;
2. source_opt : DecompilerExpr.source_expr option;
3. location : IBase.Location.t;
4. copied_location : (IR.Procname.t * IBase.Location.t) option;
5. from : Pulselib.PulseBasicInterface.Attribute.CopyOrigin.t;
6. copied_timestamp : Pulselib.PulseBasicInterface.Timestamp.t;
}

type parameter_spec_t =

| Unmodified of {
1. typ : IR.Typ.t;
2. location : IBase.Location.t;
3. heap : BaseMemory.t;
}
| Modified

include Absint.AbstractDomain.WithBottomTop

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 bottom : t

val is_bottom : t -> bool

val top : t

val is_top : t -> bool

type summary

val make_summary : t -> summary

module Summary : sig ... end

val add_var : 
  Pulselib.PulseBasicInterface.Attribute.CopiedInto.t ->
  source_addr_opt:Pulselib.PulseBasicInterface.AbstractValue.t option ->
  copy_spec_t ->
  t ->
  t

val remove_var : IR.Var.t -> t -> t

val add_field : 
  IR.Fieldname.t ->
  source_addr_opt:Pulselib.PulseBasicInterface.AbstractValue.t option ->
  copy_spec_t ->
  t ->
  t

val add_parameter : IR.Var.t -> parameter_spec_t -> t -> t

val checked_via_destructor : IR.Var.t -> t -> t

val mark_copy_as_modified : 
  is_modified:
    (BaseMemory.t -> Pulselib.PulseBasicInterface.Timestamp.t -> bool) ->
  copied_into:Pulselib.PulseBasicInterface.Attribute.CopiedInto.t ->
  source_addr_opt:Pulselib.PulseBasicInterface.AbstractValue.t option ->
  t ->
  t

val mark_parameter_as_modified : 
  is_modified:
    (BaseMemory.t -> Pulselib.PulseBasicInterface.Timestamp.t -> bool) ->
  var:IR.Var.t ->
  t ->
  t

val get_copied : 
  ref_formals:(IR.Pvar.t * IR.Typ.t) list ->
  ptr_formals:(IR.Pvar.t * IR.Typ.t) list ->
  t ->
  (Pulselib.PulseBasicInterface.Attribute.CopiedInto.t
   * IR.Typ.t option
   * DecompilerExpr.source_expr option
   * IBase.Location.t
   * (IR.Procname.t * IBase.Location.t) option
   * Pulselib.PulseBasicInterface.Attribute.CopyOrigin.t)
    list

val get_const_refable_parameters : 
  t ->
  (IR.Var.t * IR.Typ.t * IBase.Location.t) list

val is_checked_via_destructor : IR.Var.t -> t -> bool

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

val set_locked : t -> t

val is_locked : t -> bool

val set_load : 
  IBase.Location.t ->
  Pulselib.PulseBasicInterface.Timestamp.t ->
  IR.Ident.t ->
  IR.Var.t ->
  t ->
  t

val set_store : 
  IBase.Location.t ->
  Pulselib.PulseBasicInterface.Timestamp.t ->
  IR.Pvar.t ->
  t ->
  t

val get_loaded_locations : IR.Var.t -> t -> IBase.Location.t list

val set_passed_to : 
  IBase.Location.t ->
  Pulselib.PulseBasicInterface.Timestamp.t ->
  IR.Exp.t ->
  (IR.Exp.t * IR.Typ.t) list ->
  t ->
  t

val is_lifetime_extended : IR.Var.t -> t -> bool

val remember_dropped_disjuncts : 
  (ExecutionDomain.t * PathContext.t) list ->
  t ->
  t

val apply_summary : 
  callee_pname:IR.Procname.t ->
  call_loc:IBase.Location.t ->
  skip_transitive_accesses:bool ->
  t ->
  summary ->
  t

val bind : ('a list * t) -> f:('a -> t -> 'b list * t) -> 'b list * t

bind ([astate1; astate2; ...; astateN], non_disj) f =
    (astates1 \@ astate2 \@ ... \@ astatesN, non_disj1 U non_disj2 U ... U non_disjN)
with
  (astates1, non_disj1) = f astate1 non_disj
  (astates2, non_disj2) = f astate2 non_disj
  ...
  (astatesN, non_disjN) = f astateN non_disj