class NonInterferenceChecker2 extends SoftwareInterpolationFramework
Linear Supertypes
Ordering
- Alphabetic
- By Inheritance
Inherited
- NonInterferenceChecker2
- SoftwareInterpolationFramework
- AnyRef
- Any
- Hide All
- Show All
Visibility
- Public
- Protected
Instance Constructors
- new NonInterferenceChecker2(progCtor: (FrameworkVocabulary) => (IFormula, StructuredProgram), id: ConstantTerm, lVars: Seq[ConstantTerm], gVars: Seq[ConstantTerm])
Type Members
- class ModelChecker extends AnyRef
- case class NIAssertion(globalState: Renaming, localState1: Renaming, localState2: Renaming)(implicit st: SigTracker) extends Product with Serializable
- case class NICheck(inv1: IFormula, inv2: IFormula)(implicit st: SigTracker) extends Product with Serializable
- case class NIInterpolation(inv1: IFormula, inv2: IFormula, path1: Int, path2: Int)(implicit st: SigTracker) extends Product with Serializable
- case class OwickiGriesCheck(inv1: IFormula, inv2: IFormula)(implicit st: SigTracker) extends Product with Serializable
Value Members
- final def !=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- final def ##: Int
- Definition Classes
- AnyRef → Any
- final def ==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- val allGVars: Seq[ConstantTerm]
- val allLVars: Seq[ConstantTerm]
- final def asInstanceOf[T0]: T0
- Definition Classes
- Any
- def assignReadWriteTrackers(prog: StructuredProgram): StructuredProgram
- def assignTrackers(accesses: Seq[ITerm], Op: IFunction, tRec: ConstantTerm, t1: ConstantTerm, t2: ConstantTerm): StructuredProgram
- val basicSig: Signature
- def checkReadWriteTrackers(prog: StructuredProgram): StructuredProgram
- def checkTrackers(accesses: Seq[ITerm], Op: IFunction, tRec: ConstantTerm, t1: ConstantTerm, t2: ConstantTerm): StructuredProgram
- val checkingProgram: StructuredProgram
- def clone(): AnyRef
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.CloneNotSupportedException]) @HotSpotIntrinsicCandidate() @native()
- def dumpInterpolationProblem(transitionParts: Map[PartName, Conjunction], sig: Signature): Unit
- Attributes
- protected
- Definition Classes
- SoftwareInterpolationFramework
- final def eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- def equals(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef → Any
- val frameworkVocabulary: FrameworkVocabulary
- Attributes
- protected
- Definition Classes
- SoftwareInterpolationFramework
- val gVarNums: Map[ConstantTerm, Int]
- def genInterpolants(formulas: Seq[Conjunction], commonFormula: Conjunction, order: TermOrder): Either[Conjunction, Iterator[Conjunction]]
- Attributes
- protected
- Definition Classes
- SoftwareInterpolationFramework
- final def getClass(): Class[_ <: AnyRef]
- Definition Classes
- AnyRef → Any
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- def hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- val init: IFormula
- var interpolationProblemBasename: String
- Attributes
- protected
- Definition Classes
- SoftwareInterpolationFramework
- var interpolationProblemNum: Int
- Attributes
- protected
- Definition Classes
- SoftwareInterpolationFramework
- lazy val interpolationProver: IncProver
- Attributes
- protected
- Definition Classes
- SoftwareInterpolationFramework
- final def isInstanceOf[T0]: Boolean
- Definition Classes
- Any
- final def ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
- final def notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- final def notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @HotSpotIntrinsicCandidate() @native()
- def parseAndSimplify(input: Reader): (Map[PartName, Conjunction], Signature)
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
- def parseProblem(reader: Reader): (IFormula, Signature)
- Attributes
- protected
- Definition Classes
- SoftwareInterpolationFramework
- val preludeSignature: Signature
- Attributes
- protected
- Definition Classes
- SoftwareInterpolationFramework
- val program: StructuredProgram
- def programRelation(localPre: Renaming, globalPre: Renaming, localPost: Renaming, globalPost: Renaming)(implicit st: SigTracker): IFormula
- val read1: ConstantTerm
- val read2: ConstantTerm
- val readRec: ConstantTerm
- def simplifyBitvectorFor(f: IFormula, typeAssumptions: IFormula): IFormula
- Attributes
- protected
- Definition Classes
- SoftwareInterpolationFramework
- def sortNamesLex[A](transitionParts: Map[PartName, A]): Seq[PartName]
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
- final def synchronized[T0](arg0: => T0): T0
- Definition Classes
- AnyRef
- def toInputAbsyAndSimplify(c: Conjunction): IFormula
- Attributes
- protected
- Definition Classes
- SoftwareInterpolationFramework
- def toInternal(f: IFormula, sig: Signature): (Conjunction, TermOrder)
- Attributes
- protected
- Definition Classes
- SoftwareInterpolationFramework
- def toNamedParts(f: IFormula, sig: Signature): (Map[PartName, Conjunction], Signature)
- Attributes
- protected
- Definition Classes
- SoftwareInterpolationFramework
- def toString(): String
- Definition Classes
- AnyRef → Any
- val trackingProgram: StructuredProgram
- lazy val validityCheckProver: IncProver
- Attributes
- protected
- Definition Classes
- SoftwareInterpolationFramework
- implicit def voc: FrameworkVocabulary
- final def wait(arg0: Long, arg1: Int): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException])
- final def wait(arg0: Long): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException]) @native()
- final def wait(): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.InterruptedException])
- val write1: ConstantTerm
- val write2: ConstantTerm
- val writeRec: ConstantTerm
- object InterferenceException extends Exception
- object OwickiGriesException extends Exception
- object SelectStoreCollector extends CollectingVisitor[Unit, Seq[ITerm]]
Deprecated Value Members
- def finalize(): Unit
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws(classOf[java.lang.Throwable]) @Deprecated
- Deprecated
(Since version 9)