PulseInterproc (infer.Pulselib.PulseInterproc)

type call_state

type contradiction = private

| Aliasing of {
1. addr_caller : Pulselib.PulseBasicInterface.AbstractValue.t;
2. addr_callee : Pulselib.PulseBasicInterface.AbstractValue.t;
3. addr_callee' : Pulselib.PulseBasicInterface.AbstractValue.t;
4. call_state : call_state;
}
(*
raised when the precondition and the current state disagree on the aliasing, i.e. some addresses callee_addr and callee_addr' that are distinct in the pre are aliased to a single address caller_addr in the caller's current state. Typically raised when calling foo(z,z) where the spec for foo(x,y) says that x and y are disjoint. We only raise this information if we have found this alias through a heap path that is not supported by our current abstraction (like array accesses).
*)
| AliasingWithAllAliases of IR.Specialization.HeapPath.t list list
(*
similar to Aliasing case above but we have collected in a list of alias classes all alias information before raising and all of them rely on heap paths that we support.
*)
| DynamicTypeNeeded of Pulselib.PulseBasicInterface.AbstractValue.t IR.Specialization.HeapPath.Map.t
(*
A map path -> value such that each path leads to a value (in the caller space) that requires dynamic type specialization
*)
| CapturedFormalActualLength of {
1. captured_formals : (IR.Pvar.t * IR.Typ.t) list;
2. captured_actuals : ((Pulselib.PulseBasicInterface.AbstractValue.t * Pulselib.PulseBasicInterface.ValueHistory.t) * IR.Typ.t) list;
}
| FormalActualLength of {
1. formals : (IR.Pvar.t * IR.Typ.t) list;
2. actuals : ((Pulselib.PulseBasicInterface.AbstractValue.t * Pulselib.PulseBasicInterface.ValueHistory.t) * IR.Typ.t) list;
}
| PathCondition

val is_dynamic_type_needed_contradiction : 
  contradiction ->
  Pulselib.PulseBasicInterface.AbstractValue.t IR.Specialization.HeapPath.Map.t
    option

val merge_contradictions : 
  contradiction option ->
  contradiction option ->
  contradiction option

applying a summary in the caller context may lead to a contradiction; if the summary is a non-trivial list of disjuncts, we will merge all possible contradictions, in each disjunct, into a single one, using this merge_contradictions function.

val apply_summary : 
  Pulselib.PulseDomainInterface.PathContext.t ->
  IR.Procname.t ->
  IBase.Location.t ->
  callee_summary:Pulselib.PulseDomainInterface.AbductiveDomain.Summary.t ->
  captured_formals:(IR.Pvar.t * IR.Typ.t) list ->
  captured_actuals:
    ((Pulselib.PulseBasicInterface.AbstractValue.t
      * Pulselib.PulseBasicInterface.ValueHistory.t)
     * IR.Typ.t)
      list ->
  formals:(IR.Pvar.t * IR.Typ.t) list ->
  actuals:
    ((Pulselib.PulseBasicInterface.AbstractValue.t
      * Pulselib.PulseBasicInterface.ValueHistory.t)
     * IR.Typ.t)
      list ->
  Pulselib.PulseDomainInterface.AbductiveDomain.t ->
  (Pulselib.PulseDomainInterface.AbductiveDomain.t
   * (Pulselib.PulseBasicInterface.AbstractValue.t
      * Pulselib.PulseBasicInterface.ValueHistory.t)
       option
   * (Pulselib.PulseBasicInterface.AbstractValue.t
      * Pulselib.PulseBasicInterface.ValueHistory.t)
       Pulselib.PulseBasicInterface.AbstractValue.Map.t
   * Pulselib.PulseBasicInterface.ValueHistory.t
       Pulselib.PulseBasicInterface.CellId.Map.t)
    Pulselib.PulseDomainInterface.AccessResult.t
    Pulselib.PulseBasicInterface.SatUnsat.t
  * contradiction option

result of applying one pre/post pair of a callee's summary:

PulseSatUnsat.t.Unsat if that path in the callee is infeasible
otherwise, there can be an error detected
otherwise, the result is a new abstract state, an optional return value, and a substitution callee_abstract_value -> caller_abstract_value mapping callee's abstract values to what they became in the new (caller) state