PulseModelsImport (infer.Pulselib.PulseModelsImport)

type arg_payload = Pulselib.PulseBasicInterface.ValueOrigin.t

type model_data = {

analysis_data : PulseSummary.t Absint.InterproceduralAnalysis.t;
dispatch_call_eval_args : PulseSummary.t Absint.InterproceduralAnalysis.t -> Pulselib.PulseDomainInterface.PathContext.t -> (IR.Ident.t * IR.Typ.t) -> IR.Exp.t -> (IR.Exp.t * IR.Typ.t) list -> arg_payload Absint.ProcnameDispatcher.Call.FuncArg.t list -> IBase.Location.t -> IR.CallFlags.t -> Pulselib.PulseDomainInterface.AbductiveDomain.t -> Pulselib.PulseDomainInterface.NonDisjDomain.t -> IR.Procname.t option -> Pulselib.PulseDomainInterface.ExecutionDomain.t Pulselib.PulseDomainInterface.AccessResult.t list * Pulselib.PulseDomainInterface.NonDisjDomain.t;
path : Pulselib.PulseDomainInterface.PathContext.t;
callee_procname : IR.Procname.t;
location : IBase.Location.t;
ret : IR.Ident.t * IR.Typ.t;

}

type model_no_non_disj =
  model_data ->
  Pulselib.PulseDomainInterface.AbductiveDomain.t ->
  Pulselib.PulseDomainInterface.ExecutionDomain.t
    Pulselib.PulseDomainInterface.AccessResult.t
    list

type model =
  model_data ->
  Pulselib.PulseDomainInterface.AbductiveDomain.t ->
  Pulselib.PulseDomainInterface.NonDisjDomain.t ->
  Pulselib.PulseDomainInterface.ExecutionDomain.t
    Pulselib.PulseDomainInterface.AccessResult.t
    list
  * Pulselib.PulseDomainInterface.NonDisjDomain.t

val lift_model : model_no_non_disj -> model

type matcher =
  (IR.Tenv.t * IR.Procname.t, model, arg_payload)
    Absint.ProcnameDispatcher.Call.matcher

val with_non_disj : 
  ('a, model_no_non_disj, 'b) Absint.ProcnameDispatcher.Call.matcher ->
  ('a, model, 'b) Absint.ProcnameDispatcher.Call.matcher

module Hist : sig ... end

module Basic : sig ... end