Class/Object

ap.interpolants

NonInterferenceChecker2

Related Docs: object NonInterferenceChecker2 | package interpolants

Permalink

class NonInterferenceChecker2 extends SoftwareInterpolationFramework

Linear Supertypes
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. NonInterferenceChecker2
  2. SoftwareInterpolationFramework
  3. AnyRef
  4. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Instance Constructors

  1. new NonInterferenceChecker2(progCtor: (FrameworkVocabulary) ⇒ (IFormula, StructuredProgram), id: ConstantTerm, lVars: Seq[ConstantTerm], gVars: Seq[ConstantTerm])

    Permalink

Type Members

  1. class ModelChecker extends AnyRef

    Permalink
  2. case class NIAssertion(globalState: Renaming, localState1: Renaming, localState2: Renaming)(implicit st: SigTracker) extends Product with Serializable

    Permalink
  3. case class NICheck(inv1: IFormula, inv2: IFormula)(implicit st: SigTracker) extends Product with Serializable

    Permalink
  4. case class NIInterpolation(inv1: IFormula, inv2: IFormula, path1: Int, path2: Int)(implicit st: SigTracker) extends Product with Serializable

    Permalink
  5. case class OwickiGriesCheck(inv1: IFormula, inv2: IFormula)(implicit st: SigTracker) extends Product with Serializable

    Permalink

Value Members

  1. final def !=(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any
  2. final def ##(): Int

    Permalink
    Definition Classes
    AnyRef → Any
  3. final def ==(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any
  4. object InterferenceException extends Exception

    Permalink
  5. object OwickiGriesException extends Exception

    Permalink
  6. object SelectStoreCollector extends CollectingVisitor[Unit, Seq[ITerm]]

    Permalink
  7. val allGVars: Seq[ConstantTerm]

    Permalink
  8. val allLVars: Seq[ConstantTerm]

    Permalink
  9. final def asInstanceOf[T0]: T0

    Permalink
    Definition Classes
    Any
  10. def assignReadWriteTrackers(prog: StructuredProgram): StructuredProgram

    Permalink
  11. def assignTrackers(accesses: Seq[ITerm], Op: IFunction, tRec: ConstantTerm, t1: ConstantTerm, t2: ConstantTerm): StructuredProgram

    Permalink
  12. val basicSig: Signature

    Permalink
  13. def checkReadWriteTrackers(prog: StructuredProgram): StructuredProgram

    Permalink
  14. def checkTrackers(accesses: Seq[ITerm], Op: IFunction, tRec: ConstantTerm, t1: ConstantTerm, t2: ConstantTerm): StructuredProgram

    Permalink
  15. val checkingProgram: StructuredProgram

    Permalink
  16. def clone(): AnyRef

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  17. def dumpInterpolationProblem(transitionParts: Map[PartName, Conjunction], sig: Signature): Unit

    Permalink
    Attributes
    protected
    Definition Classes
    SoftwareInterpolationFramework
  18. final def eq(arg0: AnyRef): Boolean

    Permalink
    Definition Classes
    AnyRef
  19. def equals(arg0: Any): Boolean

    Permalink
    Definition Classes
    AnyRef → Any
  20. def finalize(): Unit

    Permalink
    Attributes
    protected[java.lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  21. val frameworkVocabulary: FrameworkVocabulary

    Permalink
    Attributes
    protected
    Definition Classes
    SoftwareInterpolationFramework
  22. val gVarNums: Map[ConstantTerm, Int]

    Permalink
  23. def genInterpolants(formulas: Seq[Conjunction], commonFormula: Conjunction, order: TermOrder): Either[Conjunction, Iterator[Conjunction]]

    Permalink
    Attributes
    protected
    Definition Classes
    SoftwareInterpolationFramework
  24. final def getClass(): Class[_]

    Permalink
    Definition Classes
    AnyRef → Any
  25. def hashCode(): Int

    Permalink
    Definition Classes
    AnyRef → Any
  26. val init: IFormula

    Permalink
  27. var interpolationProblemBasename: String

    Permalink
    Attributes
    protected
    Definition Classes
    SoftwareInterpolationFramework
  28. var interpolationProblemNum: Int

    Permalink
    Attributes
    protected
    Definition Classes
    SoftwareInterpolationFramework
  29. lazy val interpolationProver: IncProver

    Permalink
    Attributes
    protected
    Definition Classes
    SoftwareInterpolationFramework
  30. final def isInstanceOf[T0]: Boolean

    Permalink
    Definition Classes
    Any
  31. final def ne(arg0: AnyRef): Boolean

    Permalink
    Definition Classes
    AnyRef
  32. final def notify(): Unit

    Permalink
    Definition Classes
    AnyRef
  33. final def notifyAll(): Unit

    Permalink
    Definition Classes
    AnyRef
  34. def parseAndSimplify(input: Reader): (Map[PartName, Conjunction], Signature)

    Permalink

    Read a given problem, split it into the different parts, try to simplify bitvector expressions as far as possible, and convert it to internal presentation.

    Read a given problem, split it into the different parts, try to simplify bitvector expressions as far as possible, and convert it to internal presentation. Bitvector simplifications are done based on the type declarations inSigned, inUnsigned, and inArray. The problem will also be restructured such that the type declaration of a constant occurs in the first part in which the constant is used (sorted the partitions lexicographically according to their name).

    Attributes
    protected
    Definition Classes
    SoftwareInterpolationFramework
  35. def parseProblem(reader: Reader): (IFormula, Signature)

    Permalink
    Attributes
    protected
    Definition Classes
    SoftwareInterpolationFramework
  36. val preludeSignature: Signature

    Permalink
    Attributes
    protected
    Definition Classes
    SoftwareInterpolationFramework
  37. val program: StructuredProgram

    Permalink
  38. def programRelation(localPre: Renaming, globalPre: Renaming, localPost: Renaming, globalPost: Renaming)(implicit st: SigTracker): IFormula

    Permalink
  39. val read1: ConstantTerm

    Permalink
  40. val read2: ConstantTerm

    Permalink
  41. val readRec: ConstantTerm

    Permalink
  42. def simplifyBitvectorFor(f: IFormula, typeAssumptions: IFormula): IFormula

    Permalink
    Attributes
    protected
    Definition Classes
    SoftwareInterpolationFramework
  43. def sortNamesLex[A](transitionParts: Map[PartName, A]): Seq[PartName]

    Permalink

    Sort the transition relations lexicographically according to their name; NO_NAME is ignored and removed

    Sort the transition relations lexicographically according to their name; NO_NAME is ignored and removed

    Attributes
    protected
    Definition Classes
    SoftwareInterpolationFramework
  44. final def synchronized[T0](arg0: ⇒ T0): T0

    Permalink
    Definition Classes
    AnyRef
  45. def toInputAbsyAndSimplify(c: Conjunction): IFormula

    Permalink
    Attributes
    protected
    Definition Classes
    SoftwareInterpolationFramework
  46. def toInternal(f: IFormula, sig: Signature): (Conjunction, TermOrder)

    Permalink
    Attributes
    protected
    Definition Classes
    SoftwareInterpolationFramework
  47. def toNamedParts(f: IFormula, sig: Signature): (Map[PartName, Conjunction], Signature)

    Permalink
    Attributes
    protected
    Definition Classes
    SoftwareInterpolationFramework
  48. def toString(): String

    Permalink
    Definition Classes
    AnyRef → Any
  49. val trackingProgram: StructuredProgram

    Permalink
  50. lazy val validityCheckProver: IncProver

    Permalink
    Attributes
    protected
    Definition Classes
    SoftwareInterpolationFramework
  51. implicit def voc: FrameworkVocabulary

    Permalink
  52. final def wait(): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  53. final def wait(arg0: Long, arg1: Int): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  54. final def wait(arg0: Long): Unit

    Permalink
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  55. val write1: ConstantTerm

    Permalink
  56. val write2: ConstantTerm

    Permalink
  57. val writeRec: ConstantTerm

    Permalink

Inherited from AnyRef

Inherited from Any

Ungrouped