Uses of Class
org.jmlspecs.checker.JmlVarAssertion

Packages that use JmlVarAssertion

org.jmlspecs.checker

Contains the source code for a parser and typechecker for JML annotations and java code.

Uses of JmlVarAssertion in org.jmlspecs.checker

Subclasses of JmlVarAssertion in org.jmlspecs.checker

class	JmlInitiallyVarAssertion This class represents a jml-var-assertion of the form initially predicate.
class	JmlMonitorsForVarAssertion JmlMonitorsForVarAssertion.java
class	JmlReadableIfVarAssertion This class represents a jml-var-assertion of the form readable id if predicate.
class	JmlWritableIfVarAssertion This class represents a jml-var-assertion of the form writable id if predicate.

Fields in org.jmlspecs.checker declared as JmlVarAssertion

protected JmlVarAssertion[]	JmlTypeDeclaration.varAssertions
protected JmlVarAssertion[]	JmlTypeDeclaration.combinedVarAssertions
private JmlVarAssertion[]	JmlFieldDeclaration.varAssertions
private JmlVarAssertion[]	JmlFieldDeclaration.combinedVarAssertions

Methods in org.jmlspecs.checker that return JmlVarAssertion

JmlVarAssertion[]	CParseClassContext.varAssertions()
JmlVarAssertion[]	JmlMemberDeclaration.getCombinedVarAssertions() Returns null unless overridden by a subclass.
JmlVarAssertion[]	JmlTypeDeclaration.varAssertions()
JmlVarAssertion[]	JmlTypeDeclaration.combinedVarAssertions()
JmlVarAssertion[]	JmlFieldDeclaration.varAssertions() Returns the jml-var-assertion associated with this.
JmlVarAssertion[]	JmlFieldDeclaration.getCombinedVarAssertions() Returns the variable assertions of this member declaration combined with the assertions of those it refines.
private JmlVarAssertion[]	TestJmlParser.varAssertionFrom(JmlCompilationUnit unit)

Methods in org.jmlspecs.checker with parameters of type JmlVarAssertion

void	CParseClassContext.addVarAssertion(JmlVarAssertion varAssert)
static JmlClassDeclaration	JmlClassDeclaration.makeInstance(TokenReference where, long modifiers, String ident, CTypeVariable[] typevariables, CClassType superType, boolean isWeakSubtype, CClassType[] interfaces, boolean[] interfaceWeaklyFlags, ArrayList methods, ArrayList inners, JPhylum[] fieldsAndInits, JmlInvariant[] invariants, JmlConstraint[] constraints, JmlRepresentsDecl[] representsDecls, JmlAxiom[] axioms, JmlVarAssertion[] varAssertions, JavadocComment javadoc, JavaStyleComment[] comment, boolean isRefinedType) Constructs a class declaration in the parsing tree.
static JmlFieldDeclaration	JmlFieldDeclaration.makeInstance(TokenReference where, JVariableDefinition var, JavadocComment javadoc, JavaStyleComment[] comment, JmlVarAssertion[] varAssertions, JmlDataGroupAccumulator dataGroups)
static JmlInterfaceDeclaration	JmlInterfaceDeclaration.makeInstance(TokenReference where, long modifiers, String ident, CTypeVariable[] typevariables, CClassType[] interfaces, boolean[] interfaceWeaklyFlags, ArrayList methods, ArrayList inners, JPhylum[] fieldsAndInits, JmlInvariant[] invariants, JmlConstraint[] constraints, JmlRepresentsDecl[] representsDecls, JmlAxiom[] axioms, JmlVarAssertion[] varAssertions, JavadocComment javadoc, JavaStyleComment[] comment, boolean isRefinedType) Constructs an interface declaration in the parsing tree.

Constructors in org.jmlspecs.checker with parameters of type JmlVarAssertion

JmlTypeDeclaration(TokenReference where, boolean[] interfaceWeaklyFlags, JmlInvariant[] invariants, JmlConstraint[] constraints, JmlRepresentsDecl[] representsDecls, JmlAxiom[] axioms, JmlVarAssertion[] varAssertions, JTypeDeclaration delegee)

JmlClassDeclaration(TokenReference where, boolean isWeakSubtype, boolean[] interfaceWeaklyFlags, JmlInvariant[] invariants, JmlConstraint[] constraints, JmlRepresentsDecl[] representsDecls, JmlAxiom[] axioms, JmlVarAssertion[] varAssertions, JClassDeclarationWrapper delegee)
Constructs a new JML class declaration; clients should use factory method makeInstance instead.

JmlFieldDeclaration(TokenReference where, JmlVarAssertion[] varAssertions, JmlDataGroupAccumulator dataGroups, JFieldDeclaration delegee)

JmlInterfaceDeclaration(TokenReference where, boolean[] interfaceWeaklyFlags, JmlInvariant[] invariants, JmlConstraint[] constraints, JmlRepresentsDecl[] representsDecls, JmlAxiom[] axioms, JmlVarAssertion[] varAssertions, JInterfaceDeclarationWrapper delegee)
Constructs a new JML interface declaration; clients should use factory method makeInstance instead.