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
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