Pulselib.PulseCallOperations
val call :
PulseSummary.t Absint.InterproceduralAnalysis.t ->
Pulselib.PulseDomainInterface.PathContext.t ->
IBase.Location.t ->
IR.Procname.t ->
ret:(IR.Ident.t * IR.Typ.t) ->
actuals:
((Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t)
* IR.Typ.t)
list ->
formals_opt:(IR.Pvar.t * IR.Typ.t) list option ->
call_kind:PulseOperations.call_kind ->
Pulselib.PulseDomainInterface.AbductiveDomain.t ->
?call_flags:IR.CallFlags.t ->
Pulselib.PulseDomainInterface.NonDisjDomain.t ->
Pulselib.PulseDomainInterface.ExecutionDomain.t
Pulselib.PulseDomainInterface.AccessResult.t
list
* Pulselib.PulseDomainInterface.NonDisjDomain.t
* PulseInterproc.contradiction option
* [ `KnownCall | `UnknownCall ]
perform an interprocedural call: apply the summary for the call proc name passed as argument if it exists
val unknown_call :
IR.Tenv.t ->
Pulselib.PulseDomainInterface.PathContext.t ->
IBase.Location.t ->
Pulselib.PulseBasicInterface.CallEvent.t ->
IR.Procname.t option ->
ret:(IR.Ident.t * IR.Typ.t) ->
actuals:
((Pulselib.PulseBasicInterface.AbstractValue.t
* Pulselib.PulseBasicInterface.ValueHistory.t)
* IR.Typ.t)
list ->
formals_opt:(IR.Pvar.t * IR.Typ.t) list option ->
Pulselib.PulseDomainInterface.AbductiveDomain.t ->
Pulselib.PulseDomainInterface.AbductiveDomain.t
Pulselib.PulseDomainInterface.AccessResult.t
Pulselib.PulseBasicInterface.SatUnsat.t
performs a call to a function with no summary by optimistically havoc'ing the by-ref actuals and the return value as appropriate
module GlobalForStats : sig ... end