PulseCallOperations (infer.Pulselib.PulseCallOperations)

val call : 
  IR.Tenv.t ->
  Pulselib.PulseDomainInterface.PathContext.t ->
  caller_proc_desc:IR.Procdesc.t ->
  analyze_dependency:
    (?specialization:IR.Specialization.t ->
      IR.Procname.t ->
      PulseSummary.t option) ->
  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