PulseNonDisjunctiveOperations (infer.Pulselib.PulseNonDisjunctiveOperations)

val has_copy_in : string -> bool

Check if the string includes "copy" in case-insensitive

val init_const_refable_parameters : 
  IR.Procdesc.t ->
  IR.IntegerWidths.t ->
  IR.Tenv.t ->
  Pulselib.PulseDomainInterface.ExecutionDomain.t list ->
  Pulselib.PulseDomainInterface.NonDisjDomain.t ->
  Pulselib.PulseDomainInterface.NonDisjDomain.t

Initialize candidate parameters for const refable in the non-disj domain

val call : 
  IR.IntegerWidths.t ->
  IR.Tenv.t ->
  IR.Procdesc.t ->
  Pulselib.PulseDomainInterface.PathContext.t ->
  IBase.Location.t ->
  call_exp:IR.Exp.t ->
  actuals:(IR.Exp.t * IR.Typ.t) list ->
  astates_before:Pulselib.PulseDomainInterface.AbductiveDomain.t list ->
  Pulselib.PulseDomainInterface.ExecutionDomain.t list ->
  Pulselib.PulseDomainInterface.NonDisjDomain.t ->
  Pulselib.PulseDomainInterface.NonDisjDomain.t
  * Pulselib.PulseDomainInterface.ExecutionDomain.t list

Abstract semantics for a funcation call

val mark_modified_copies_and_parameters : 
  IR.Var.t list ->
  Pulselib.PulseDomainInterface.ExecutionDomain.t list ->
  Pulselib.PulseDomainInterface.NonDisjDomain.t ->
  Pulselib.PulseDomainInterface.NonDisjDomain.t

Mark if copies and parameters has been modified so far

val mark_modified_copies_and_parameters_on_abductive : 
  IR.Var.t list ->
  Pulselib.PulseDomainInterface.AbductiveDomain.t ->
  Pulselib.PulseDomainInterface.NonDisjDomain.t ->
  Pulselib.PulseDomainInterface.NonDisjDomain.t

Similar to mark_modified_copies_and_parameters, but given by PulseAbductiveDomain.t instead