Uses of Class
org.jmlspecs.jml4.esc.vc.lang.VC

Packages that use VC

org.jmlspecs.jml4.esc.gc.lang
org.jmlspecs.jml4.esc.gc.lang.expr
org.jmlspecs.jml4.esc.provercoordinator.prover
org.jmlspecs.jml4.esc.provercoordinator.prover.cvc3
org.jmlspecs.jml4.esc.provercoordinator.prover.isabelle
org.jmlspecs.jml4.esc.provercoordinator.prover.simplify
org.jmlspecs.jml4.esc.vc
org.jmlspecs.jml4.esc.vc.lang

Uses of VC in org.jmlspecs.jml4.esc.gc.lang

Methods in org.jmlspecs.jml4.esc.gc.lang that return VC

VC	CfgVarDecl.accept(WlpVisitor visitor, VC N)
VC	CfgStatementBlock.accept(WlpVisitor visitor, VC N)
abstract VC	CfgStatement.accept(WlpVisitor visitor, VC N)
VC	CfgSequence.accept(WlpVisitor visitor, VC N)
VC	CfgGoto.accept(WlpVisitor visitor, VC N)
VC	CfgBlock.accept(WlpVisitor visitor, VC N)
VC	CfgAssume.accept(WlpVisitor visitor, VC N)
VC	CfgAssert.accept(WlpVisitor visitor, VC N)

Methods in org.jmlspecs.jml4.esc.gc.lang with parameters of type VC

VC	CfgVarDecl.accept(WlpVisitor visitor, VC N)
VC	CfgStatementBlock.accept(WlpVisitor visitor, VC N)
abstract VC	CfgStatement.accept(WlpVisitor visitor, VC N)
VC	CfgSequence.accept(WlpVisitor visitor, VC N)
VC	CfgGoto.accept(WlpVisitor visitor, VC N)
VC	CfgBlock.accept(WlpVisitor visitor, VC N)
VC	CfgAssume.accept(WlpVisitor visitor, VC N)
VC	CfgAssert.accept(WlpVisitor visitor, VC N)

Uses of VC in org.jmlspecs.jml4.esc.gc.lang.expr

Methods in org.jmlspecs.jml4.esc.gc.lang.expr that return VC

VC	CfgVariable.accept(WlpVisitor visitor)
VC	CfgThisReference.accept(WlpVisitor visitor)
VC	CfgSuperReference.accept(WlpVisitor visitor)
VC	CfgQuantifiedExpression.accept(WlpVisitor visitor)
VC	CfgNotExpression.accept(WlpVisitor visitor)
VC	CfgIntegerConstant.accept(WlpVisitor visitor)
VC	CfgFieldStore.accept(WlpVisitor visitor)
VC	CfgFieldReference.accept(WlpVisitor visitor)
abstract VC	CfgExpression.accept(WlpVisitor visitor)
VC	CfgConditionalExpression.accept(WlpVisitor visitor)
VC	CfgBooleanConstant.accept(WlpVisitor visitor)
VC	CfgBinaryExpression.accept(WlpVisitor visitor)
VC	CfgArrayReference.accept(WlpVisitor visitor)
VC	CfgArrayAllocationExpression.accept(WlpVisitor visitor)

Uses of VC in org.jmlspecs.jml4.esc.provercoordinator.prover

Methods in org.jmlspecs.jml4.esc.provercoordinator.prover with parameters of type VC

void	CachedVcs.add(VC vc)
boolean	CachedVcs.contains(VC vc)
java.lang.String	ProverVisitor.getVarDecls(VC[] vcs, java.util.Map incarnations)
abstract Result[]	ProverAdapter.prove(VC vc, java.util.Map incarnations)

Uses of VC in org.jmlspecs.jml4.esc.provercoordinator.prover.cvc3

Methods in org.jmlspecs.jml4.esc.provercoordinator.prover.cvc3 with parameters of type VC

java.lang.String	Cvc3Visitor.getTheory(VC vc, java.util.Map incarnations)
Result[]	Cvc3Adapter.prove(VC vc, java.util.Map incarnations)

Uses of VC in org.jmlspecs.jml4.esc.provercoordinator.prover.isabelle

Methods in org.jmlspecs.jml4.esc.provercoordinator.prover.isabelle with parameters of type VC

java.lang.String	IsabelleVisitor.getTheory(VC vc, java.util.Map incarnations)
Result[]	IsabelleAdapter.prove(VC vc, java.util.Map incarnations)

Uses of VC in org.jmlspecs.jml4.esc.provercoordinator.prover.simplify

Methods in org.jmlspecs.jml4.esc.provercoordinator.prover.simplify with parameters of type VC

Result[]	SimplifyAdapter.formatResponse(java.lang.String fromProver, VC vc, java.lang.String simplifyString)
java.lang.String	SimplifyVisitor.getTheory(VC vc, java.util.Map incarnations)
Result[]	SimplifyAdapter.prove(VC vc, java.util.Map incarnations)

Uses of VC in org.jmlspecs.jml4.esc.vc

Methods in org.jmlspecs.jml4.esc.vc that return VC

VC	WlpVisitor.visit(CfgArrayAllocationExpression arrayAlloc)
VC	WlpVisitor.visit(CfgArrayReference arrayRef)
VC	WlpVisitor.visit(CfgAssert cfgAssert, VC N)
VC	WlpVisitor.visit(CfgAssume cfgAssume, VC N)
VC	WlpVisitor.visit(CfgBinaryExpression binExpr)
VC	WlpVisitor.visit(CfgBlock cfgBlock, VC N)
VC	WlpVisitor.visit(CfgBooleanConstant bool)
VC	WlpVisitor.visit(CfgConditionalExpression condExpr)
VC	WlpVisitor.visit(CfgFieldReference fieldRef)
VC	WlpVisitor.visit(CfgFieldStore fieldStore)
VC	WlpVisitor.visit(CfgGoto cfgGoto, VC N)
VC	WlpVisitor.visit(CfgIntegerConstant intConst)
VC	WlpVisitor.visit(CfgNotExpression notRef)
VC	WlpVisitor.visit(CfgQuantifiedExpression expr)
VC	WlpVisitor.visit(CfgSequence cfgSequence, VC N)
VC	WlpVisitor.visit(CfgStatementBlock cfgStatementBlock, VC N)
VC	WlpVisitor.visit(CfgSuperReference superRef)
VC	WlpVisitor.visit(CfgThisReference thisRef)
VC	WlpVisitor.visit(CfgVarDecl cfgVarDecl)
VC	WlpVisitor.visit(CfgVariable var)

Methods in org.jmlspecs.jml4.esc.vc with parameters of type VC

VC	WlpVisitor.visit(CfgAssert cfgAssert, VC N)
VC	WlpVisitor.visit(CfgAssume cfgAssume, VC N)
VC	WlpVisitor.visit(CfgBlock cfgBlock, VC N)
VC	WlpVisitor.visit(CfgGoto cfgGoto, VC N)
VC	WlpVisitor.visit(CfgSequence cfgSequence, VC N)
VC	WlpVisitor.visit(CfgStatementBlock cfgStatementBlock, VC N)

Uses of VC in org.jmlspecs.jml4.esc.vc.lang

Subclasses of VC in org.jmlspecs.jml4.esc.vc.lang

class	VcAnd
class	VcAndNary
class	VcArithExpression
class	VcArrayAllocationExpression
class	VcArrayReference
class	VcBinaryExpression
class	VcBooleanConstant
class	VcConditionalExpression
class	VcFieldReference
class	VcFieldStore
class	VcIntegerConstant
class	VcLogicalExpression
class	VcNot
class	VcOr
class	VcQuantifiedExpression
class	VcRelativeExpression
class	VcSuperReference
class	VcThisReference
class	VcVarDecl
class	VcVariable

Fields in org.jmlspecs.jml4.esc.vc.lang declared as VC

VC	VcQuantifiedExpression.body
VC	VcConditionalExpression.condition
VC[]	VcAndNary.conjuncts
VC[]	VcArrayAllocationExpression.dims
static VC[]	VC.EMPTY
VC	VcBinaryExpression.left
VC	VcArrayReference.position
VC	VcQuantifiedExpression.range
VC	VcFieldReference.receiver
VC	VcArrayReference.receiver
VC	VcBinaryExpression.right
VC	VcFieldStore.value
VC	VcConditionalExpression.valueIfFalse
VC	VcConditionalExpression.valueIfTrue
VC	VcNot.vc
VC[]	VcProgram.vcs

Methods in org.jmlspecs.jml4.esc.vc.lang that return VC

VC[]	VcProgram.getAsImplications_old()
VC[]	VcProgram.getAsImplications()
VC[]	VcProgram.getAsSingleVC_old()
VC[]	VcProgram.getAsSingleVC()
VC	VcLogicalExpression.negateLastImplication()
VC	VC.negateLastImplication()

Constructors in org.jmlspecs.jml4.esc.vc.lang with parameters of type VC

VcAnd(VC left, VC right, int sourceStart, int sourceEnd)

VcAnd(VC left, VC right, KindOfAssertion kindOfAssertion, int kindOfLabel, int sourceStart, int sourceEnd, int labelStart)

VcAndNary(VC[] conjuncts, int sourceStart, int sourceEnd)

VcArithExpression(VcOperator operator, VC left, VC right, TypeBinding type, int sourceStart, int sourceEnd)

VcArithExpression(VcOperator operator, VC left, VC right, TypeBinding type, KindOfAssertion kindOfAssertion, int kindOfLabel, int sourceStart, int sourceEnd, int labelStart)

VcArrayAllocationExpression(int[] ids, VC[] dims, TypeBinding type, int sourceStart, int sourceEnd)

VcArrayAllocationExpression(int[] ids, VC[] dims, TypeBinding type, KindOfAssertion kindOfAssertion, int kindOfLabel, int sourceStart, int sourceEnd, int labelStart)

VcArrayReference(VC receiver, VC position, int incarnation, TypeBinding type, int sourceStart, int sourceEnd)

VcArrayReference(VC receiver, VC position, int incarnation, TypeBinding type, KindOfAssertion kindOfAssertion, int kindOfLabel, int sourceStart, int sourceEnd, int labelStart)

VcBinaryExpression(VC left, VC right, TypeBinding type, int sourceStart, int sourceEnd)

VcBinaryExpression(VC left, VC right, TypeBinding type, KindOfAssertion kindOfAssertion, int kindOfLabel, int sourceStart, int sourceEnd, int labelStart)

VcConditionalExpression(VC condition, VC valueIfTrue, VC valueIfFalse, TypeBinding type, int sourceStart, int sourceEnd)

VcConditionalExpression(VC condition, VC valueIfTrue, VC valueIfFalse, TypeBinding type, KindOfAssertion kindOfAssertion, int kindOfLabel, int sourceStart, int sourceEnd, int labelStart)

VcFieldReference(VC receiver, java.lang.String field, int incarnation, TypeBinding type, int sourceStart, int sourceEnd)

VcFieldReference(VC receiver, java.lang.String field, int incarnation, TypeBinding type, KindOfAssertion kindOfAssertion, int kindOfLabel, int sourceStart, int sourceEnd, int labelStart)

VcFieldStore(VcFieldReference field, int oldIncarnation, int newIncarnation, VC value)

VcFieldStore(VcFieldReference field, int oldIncarnation, int newIncarnation, VC value, KindOfAssertion kindOfAssertion, int kindOfLabel, int labelStart)

VcLogicalExpression(VcOperator operator, VC left, VC right, int sourceStart, int sourceEnd)

VcLogicalExpression(VcOperator operator, VC left, VC right, KindOfAssertion kindOfAssertion, int kindOfLabel, int sourceStart, int sourceEnd, int labelStart)

VcNot(VC vc, int sourceStart, int sourceEnd)

VcNot(VC vc, KindOfAssertion kindOfAssertion, int kindOfLabel, int sourceStart, int sourceEnd, int labelStart)

VcOr(VC left, VC right, int sourceStart, int sourceEnd)

VcOr(VC left, VC right, KindOfAssertion kindOfAssertion, int kindOfLabel, int sourceStart, int sourceEnd, int labelStart)

VcProgram(VC[] vcs, java.lang.String startId, java.util.Map incarnations, java.lang.String methodIndicator)

VcQuantifiedExpression(VcQuantifier quantifier, VcVarDecl[] boundVarDecls, VC body)

VcQuantifiedExpression(VcQuantifier quantifier, VC range, VC body, TypeBinding type, int sourceStart, int sourceEnd)

VcQuantifiedExpression(VcQuantifier quantifier, VC range, VC body, TypeBinding type, KindOfAssertion kindOfAssertion, int kindOfLabel, int sourceStart, int sourceEnd, int labelStart)

VcRelativeExpression(VcOperator operator, VC left, VC right, int sourceStart, int sourceEnd)

VcRelativeExpression(VcOperator operator, VC left, VC right, KindOfAssertion kindOfAssertion, int kindOfLabel, int sourceStart, int sourceEnd, int labelStart)