NonInterferenceChecker2

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
object InterferenceException extends Exception
object OwickiGriesException extends Exception
object SelectStoreCollector extends CollectingVisitor[Unit, Seq[ITerm]]
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[java.lang]
Definition Classes
AnyRef
Annotations
@HotSpotIntrinsicCandidate() @throws( ... )
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: Any): 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[_]

Definition Classes
AnyRef → Any
Annotations
@HotSpotIntrinsicCandidate()
def hashCode(): Int

Definition Classes
AnyRef → Any
Annotations
@HotSpotIntrinsicCandidate()
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()
final def notifyAll(): Unit

Definition Classes
AnyRef
Annotations
@HotSpotIntrinsicCandidate()
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( ... )
final def wait(arg0: Long): Unit

Definition Classes
AnyRef
Annotations
@throws( ... )
final def wait(): Unit

Definition Classes
AnyRef
Annotations
@throws( ... )
val write1: ConstantTerm
val write2: ConstantTerm
val writeRec: ConstantTerm

Deprecated Value Members

def finalize(): Unit

Attributes
protected[java.lang]
Definition Classes
AnyRef
Annotations
@Deprecated @deprecated @throws( classOf[java.lang.Throwable] )
Deprecated
(Since version ) see corresponding Javadoc for more information.

Related Docs: object NonInterferenceChecker2 | package interpolants

class NonInterferenceChecker2 extends SoftwareInterpolationFramework

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

final def ##(): Int

final def ==(arg0: Any): Boolean

object InterferenceException extends Exception

object OwickiGriesException extends Exception

object SelectStoreCollector extends CollectingVisitor[Unit, Seq[ITerm]]

val allGVars: Seq[ConstantTerm]

val allLVars: Seq[ConstantTerm]

final def asInstanceOf[T0]: T0

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

def dumpInterpolationProblem(transitionParts: Map[PartName, Conjunction], sig: Signature): Unit

final def eq(arg0: AnyRef): Boolean

def equals(arg0: Any): Boolean

val frameworkVocabulary: FrameworkVocabulary

val gVarNums: Map[ConstantTerm, Int]

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

final def getClass(): Class[_]

def hashCode(): Int

val init: IFormula

var interpolationProblemBasename: String

var interpolationProblemNum: Int

lazy val interpolationProver: IncProver

final def isInstanceOf[T0]: Boolean

final def ne(arg0: AnyRef): Boolean

final def notify(): Unit

final def notifyAll(): Unit

def parseAndSimplify(input: Reader): (Map[PartName, Conjunction], Signature)

def parseProblem(reader: Reader): (IFormula, Signature)

val preludeSignature: Signature

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

def sortNamesLex[A](transitionParts: Map[PartName, A]): Seq[PartName]

final def synchronized[T0](arg0: ⇒ T0): T0

def toInputAbsyAndSimplify(c: Conjunction): IFormula

def toInternal(f: IFormula, sig: Signature): (Conjunction, TermOrder)

def toNamedParts(f: IFormula, sig: Signature): (Map[PartName, Conjunction], Signature)

def toString(): String

val trackingProgram: StructuredProgram

lazy val validityCheckProver: IncProver

implicit def voc: FrameworkVocabulary

final def wait(arg0: Long, arg1: Int): Unit

final def wait(arg0: Long): Unit

final def wait(): Unit

val write1: ConstantTerm

val write2: ConstantTerm

val writeRec: ConstantTerm

Deprecated Value Members

def finalize(): Unit

Inherited from SoftwareInterpolationFramework

Inherited from AnyRef

Inherited from Any

Ungrouped