Module Pulselib.PulseNonDisjunctiveDomain

module F = Stdlib.Format
module BaseMemory = PulseBaseMemory
module DecompilerExpr = PulseDecompilerExpr
module ExecutionDomain = PulseExecutionDomain
module PathContext = PulsePathContext
type copy_spec_t =
  1. | Copied of {
    1. source_typ : IR.Typ.t option;
    2. source_opt : DecompilerExpr.source_expr option;
    3. node : IR.Procdesc.Node.t;
    4. location : IBase.Location.t;
    5. copied_location : (IR.Procname.t * IBase.Location.t) option;
    6. heap : BaseMemory.t;
    7. from : Pulselib.PulseBasicInterface.Attribute.CopyOrigin.t;
    8. timestamp : Pulselib.PulseBasicInterface.Timestamp.t;
    }
  2. | Modified of {
    1. source_typ : IR.Typ.t option;
    2. source_opt : DecompilerExpr.source_expr option;
    3. node : IR.Procdesc.Node.t;
    4. location : IBase.Location.t;
    5. copied_location : (IR.Procname.t * IBase.Location.t) option;
    6. from : Pulselib.PulseBasicInterface.Attribute.CopyOrigin.t;
    7. copied_timestamp : Pulselib.PulseBasicInterface.Timestamp.t;
    }
type parameter_spec_t =
  1. | Unmodified of {
    1. typ : IR.Typ.t;
    2. location : IBase.Location.t;
    3. heap : BaseMemory.t;
    }
  2. | 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
val exec : t -> exec_instr: (((ExecutionDomain.t * PathContext.t) * t) -> (ExecutionDomain.t * PathContext.t) list * t) -> t
val pp_with_kind : IStdlib.Pp.print_kind -> F.formatter -> t -> unit
type summary
val make_summary : IR.ProcAttributes.t -> IBase.Location.t -> t -> summary
module Summary : sig ... end
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_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 get_loaded_locations : IR.Var.t -> t -> IBase.Location.t list
val is_lifetime_extended : IR.Var.t -> t -> bool
val remember_dropped_disjuncts : (ExecutionDomain.t * PathContext.t) list -> t -> t
val add_specialized_direct_callee : IR.Procname.t -> IR.Specialization.Pulse.t -> IBase.Location.t -> 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