Uses of Class
org.jmlspecs.checker.JmlConstraint

Packages that use JmlConstraint

org.jmlspecs.checker	Contains the source code for a parser and typechecker for JML annotations and java code.
org.jmlspecs.jmldoc.jmldoc_142
org.jmlspecs.jmlrac	Generates Java classes from JML specifications that check assertions at runtime.

Uses of JmlConstraint in org.jmlspecs.checker

Fields in org.jmlspecs.checker declared as JmlConstraint

protected JmlConstraint[]	JmlTypeDeclaration.constraints
protected JmlConstraint[]	JmlTypeDeclaration.combinedConstraints

Methods in org.jmlspecs.checker that return JmlConstraint

JmlConstraint[]	CParseClassContext.constraints()
JmlConstraint[]	JmlTypeDeclaration.constraints()
JmlConstraint[]	JmlTypeDeclaration.combinedConstraints()
private JmlConstraint[]	TestJmlParser.constraintsFrom(JmlCompilationUnit unit)

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

void	JmlAbstractVisitor.visitJmlConstraint(JmlConstraint self)
abstract void	JmlVisitor.visitJmlConstraint(JmlConstraint self)
void	CParseClassContext.addConstraint(JmlConstraint inv)
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 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.
void	JmlVisitorNI.visitJmlConstraint(JmlConstraint self)

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

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.

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.

Uses of JmlConstraint in org.jmlspecs.jmldoc.jmldoc_142

Methods in org.jmlspecs.jmldoc.jmldoc_142 with parameters of type JmlConstraint

void	SpecWriter.visitJmlConstraint(JmlConstraint self)

Uses of JmlConstraint in org.jmlspecs.jmlrac

Methods in org.jmlspecs.jmlrac with parameters of type JmlConstraint

void	RacPrettyPrinter.visitJmlConstraint(JmlConstraint self) Prints a JML constraint clause.
RacNode	TransConstraint.translate(JmlConstraint[] constraints) Translates the given history constraints, constraints, and returns the translation result.
private RacNode	TransConstraint.constraintMethod(JmlConstraint[] constraints, boolean forStatic) Returns a static or an instance constraint check method for the given history constraints, constraints.
private RacNode	TransConstraint.constraintMethod(JmlConstraint constraint, int cnt) Returns a constraint check method for the given hisotry constraint, constraint.
private static boolean	TransConstraint.isCheckable(JmlConstraint cons) Returns true if the given constraint clause is checkable.