Uses of Class
org.jmlspecs.checker.JmlSpecVarDecl

Packages that use JmlSpecVarDecl

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 JmlSpecVarDecl in org.jmlspecs.checker

Subclasses of JmlSpecVarDecl in org.jmlspecs.checker

class	JmlForAllVarDecl An AST node class for the JML forall variable declarations.
class	JmlLetVarDecl An AST node class for the JML let (old) variable declarations.

Fields in org.jmlspecs.checker declared as JmlSpecVarDecl

protected JmlSpecVarDecl[]	JmlGeneralSpecCase.specVarDecls
private JmlSpecVarDecl[]	JmlExample.specVarDecls

Methods in org.jmlspecs.checker that return JmlSpecVarDecl

JmlSpecVarDecl[]	JmlGeneralSpecCase.specVarDecls()
JmlSpecVarDecl[]	JmlExample.specVarDecls()
JmlSpecVarDecl[]	JmlParser.jmlSpecVarDecls()
protected JmlSpecVarDecl[]	TestJmlParser.Helper.getSpecVarDecls(String sourceCode)

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

void	JmlAbstractVisitor.visitJmlSpecVarDecl(JmlSpecVarDecl self)
abstract void	JmlVisitor.visitJmlSpecVarDecl(JmlSpecVarDecl self)
void	JmlVisitorNI.visitJmlSpecVarDecl(JmlSpecVarDecl self)
private JmlLetVarDecl[]	TestJmlParser.letVarDeclsFrom(JmlSpecVarDecl[] oldDecls)

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

JmlGeneralSpecCase(TokenReference where, JmlSpecVarDecl[] specVarDecls, JmlRequiresClause[] specHeader, JmlSpecBody specBody)
Creates a new JmlGeneralSpecCase instance.

JmlAbruptSpecCase(TokenReference sourceRef, JmlSpecVarDecl[] specVarDecls, JmlRequiresClause[] specHeader, JmlAbruptSpecBody abruptSpecBody)

JmlExample(TokenReference where, long privacy, JmlSpecVarDecl[] specVarDecls, JmlRequiresClause[] specHeader, JmlSpecBodyClause[] specBody)
Constructs a new instance with given arguments.

JmlExample(TokenReference where, JmlSpecVarDecl[] specVarDecls, JmlRequiresClause[] specHeader, JmlSpecBodyClause[] specBody)
Constructs a new instance with given arguments.

JmlExceptionalExample(TokenReference where, long privacy, JmlSpecVarDecl[] specVarDecls, JmlRequiresClause[] specHeader, JmlSpecBodyClause[] specClauses)
Constructs a new instance with given arguments.

JmlExceptionalSpecCase(TokenReference sourceRef, JmlSpecVarDecl[] specVarDecls, JmlRequiresClause[] specHeader, JmlExceptionalSpecBody exceptionalSpecBody)

JmlGenericSpecCase(TokenReference sourceRef, JmlSpecVarDecl[] specVarDecls, JmlRequiresClause[] specHeader, JmlGenericSpecBody genericSpecBody)

JmlNormalExample(TokenReference where, long privacy, JmlSpecVarDecl[] specVarDecls, JmlRequiresClause[] specHeader, JmlSpecBodyClause[] specClauses)
Constructs a new instance with given arguments.

JmlNormalSpecCase(TokenReference sourceRef, JmlSpecVarDecl[] specVarDecls, JmlRequiresClause[] specHeader, JmlNormalSpecBody normalSpecBody)

Uses of JmlSpecVarDecl in org.jmlspecs.jmldoc.jmldoc_142

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

void	SpecWriter.visitJmlSpecVarDecl(JmlSpecVarDecl self)

Uses of JmlSpecVarDecl in org.jmlspecs.jmlrac

Methods in org.jmlspecs.jmlrac that return JmlSpecVarDecl

abstract JmlSpecVarDecl[]	TransMethod.SpecCase.specVarDecls() Returns the specification variable declarations of this spec case.
JmlSpecVarDecl[]	TransMethod.GeneralSpecCase.specVarDecls() Returns the specification variable declarations of this spec case.

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

private JmlGenericSpecCase	DesugarSpec.add(JmlGenericSpecCase specCase, JmlSpecVarDecl[] specVarDecls, JmlRequiresClause[] specHeader) Adds the given spec var decls, specVarDecls, and spec header, specHeader, to the spec case, specCase.
void	RacPrettyPrinter.visitJmlSpecVarDecl(JmlSpecVarDecl self)
protected List	TransMethod.translateSpecVarDecls(JmlSpecVarDecl[] varDecls, VarGenerator varGen) Translates specification variable declarations.
protected List	TransMethod.translateLetVarDecl(JmlSpecVarDecl varDecl, VarGenerator varGen) Translates the given old variable declarations.
protected List	TransMethod.translateForAllVarDecl(JmlSpecVarDecl varDecl, VarGenerator varGen) Translates the given forall variable declarations.