Uses of Class
jml2b.structure.java.JmlFile

Packages that use JmlFile

jack.plugin.source
jml2b
jml2b.exceptions
jml2b.link
jml2b.pog	Provides the classes necessary to generate proof obligations.
jml2b.pog.lemma
jml2b.pog.printers
jml2b.pog.util
jml2b.structure
jml2b.structure.bytecode
jml2b.structure.java
jml2b.structure.jml	Provides the classes necessary to create and manage jml clauses such that depends, represents, specification cases, modifies and exsures.
jml2b.structure.statement	Provides the classes necessary to create and manage java and jml statements and expressions.
jml2b.util

Uses of JmlFile in jack.plugin.source

Constructors in jack.plugin.source with parameters of type JmlFile

JmlClauseGenerator(IJml2bConfiguration configuration, org.eclipse.swt.widgets.Shell shell, JmlFile f)

ModifiesGenerator(IJml2bConfiguration configuration, org.eclipse.swt.widgets.Shell shell, JmlFile f)

RequiresGenerator(IJml2bConfiguration config, org.eclipse.swt.widgets.Shell shell, JmlFile jf, boolean reqNullPointer, boolean reqArryOutOfBounds)

Uses of JmlFile in jml2b

Methods in jml2b that return JmlFile

static JmlFile[]	Jml2b.loadFiles(IJml2bConfiguration config, java.lang.String[] args) Loads files from args.
static JmlFile[]	Jml2b.loadFiles(IJml2bConfiguration config, java.lang.String[] args, int file_count) Loads the file_count files from args.
static JmlFile[]	Jml2b.loadFileImage(java.lang.String file_name) Restore the JmlFile array as well as the system packages from the given file.
static JmlFile[]	Jml2b.loadAstImage(IJml2bConfiguration config, java.lang.String astFile)

Methods in jml2b with parameters of type JmlFile

static void

Jml2b.saveFileImage(JmlFile[] files, java.lang.String file_name) Saves an image.

Uses of JmlFile in jml2b.exceptions

Methods in jml2b.exceptions with parameters of type JmlFile

static void	ErrorHandler.error(JmlFile f, int line, int column, java.lang.String description) Indicate an error in the specified file, line and column.
static void	ErrorHandler.warning(JmlFile f, int line, int column, java.lang.String description) Indicates an error in the specified file, line and column.

Constructors in jml2b.exceptions with parameters of type JmlFile

ParseException(JmlFile f, jml.LineAST tree, java.lang.String description)
Creates a new ParseException instance.

TokenException(JmlFile f, jml.LineAST tree, java.lang.String method, java.lang.String expected, java.lang.String got)
Creates a new TokenException instance.

TokenException(JmlFile f, jml.LineAST tree, java.lang.String method, java.lang.String expected, int got)
Creates a new TokenException instance.

TokenException(JmlFile f, jml.LineAST tree, java.lang.String method, int expected, int got)
Creates a new TokenException instance.

Uses of JmlFile in jml2b.link

Constructors in jml2b.link with parameters of type JmlFile

LinkContext(JmlFile f)

Uses of JmlFile in jml2b.pog

Methods in jml2b.pog with parameters of type JmlFile

void	IObviousProver.prove(IJml2bConfiguration config, JmlFile file) Prove and save the status of a jpo file.
void	Pog.pog(JmlFile file, IJml2bConfiguration config, java.util.Vector addedDepends, java.util.Vector removedDepends, org.eclipse.core.runtime.IProgressMonitor monitor) Generate the proof obligations associated with a JML file, calculate them and prove them with the obvious prover if requested.
static void	Pog.saveFiles(IJml2bConfiguration config, JmlFile file, org.eclipse.core.runtime.IProgressMonitor monitor, java.util.Vector addedDepends, java.util.Vector removedDepends, IClassResolver printer)
void	Pog.pog(JmlFile[] files, IJml2bConfiguration config) Generates the proof obligations for all the JML files, calculate them and prove them with the obvious prover if requested.

Uses of JmlFile in jml2b.pog.lemma

Methods in jml2b.pog.lemma with parameters of type JmlFile

void	NonObviousGoal.save(IJml2bConfiguration config, JpoOutputStream s, JmlFile jf) Saves the goal in a .jpo file
void	Proofs.saveThl(IJml2bConfiguration config, JpoOutputStream s, JmlFile jf)
void	Proofs.save(IJml2bConfiguration config, JpoOutputStream s, JmlFile jf) Saves the proof in the a .jpo file
void	SimpleLemma.save(IJml2bConfiguration config, JpoOutputStream s, JmlFile jf)
void	VirtualFormula.save(IJml2bConfiguration config, JpoOutputStream s, int index, JmlFile jf) Saves the virtual formula into a .jpo file

Uses of JmlFile in jml2b.pog.printers

Methods in jml2b.pog.printers with parameters of type JmlFile

void	IPrinter.print(IClassResolver printer, JmlFile fi, java.io.File output_directory) Writes an output file corresponding to the entry of a prover.

Uses of JmlFile in jml2b.pog.util

Methods in jml2b.pog.util with parameters of type JmlFile

void	ColoredInfo.save(JpoOutputStream s, int index, JmlFile f) Saves the colored info in a .jpo file if it is declared in a specified JML file

Uses of JmlFile in jml2b.structure

Constructors in jml2b.structure with parameters of type JmlFile

AMethod(JmlFile jf, antlr.collections.AST tree, Modifiers m, Class defining)

Uses of JmlFile in jml2b.structure.bytecode

Methods in jml2b.structure.bytecode with parameters of type JmlFile

antlr.collections.AST	ClassField.parse(JmlFile jmlFile, antlr.collections.AST ast)
antlr.collections.AST	ClassMethod.parse(JmlFile jmlFile, antlr.collections.AST ast)

Uses of JmlFile in jml2b.structure.java

Methods in jml2b.structure.java that return JmlFile

JmlFile

ParsedItem.getJmlFile() Returns the file.

Methods in jml2b.structure.java with parameters of type JmlFile

antlr.collections.AST	Class.parse(JmlFile jmlFile, antlr.collections.AST tree) Initialise the content of the class from the given AST tree.
void	Class.save(IJml2bConfiguration config, JpoOutputStream s, JmlFile jf) .jpo file
antlr.collections.AST	Constructor.parse(JmlFile jmlFile, antlr.collections.AST ast)
abstract antlr.collections.AST	Declaration.parse(JmlFile jmlFile, antlr.collections.AST ast) Parses the content of the declaration.
antlr.collections.AST	Field.parse(JmlFile jmlFile, antlr.collections.AST a) Deprecated. The VarDeclParser class should be used instead of this method.
static Field[]	Field.parseVarDecl(JmlFile jmlFile, antlr.collections.AST vardecl, Modifiers mods)
antlr.collections.AST	Invariant.parse(JmlFile jmlFile, antlr.collections.AST ast)
antlr.collections.AST	Method.parse(JmlFile jmlFile, antlr.collections.AST a)
void	Method.save(IJml2bConfiguration config, JpoOutputStream s, JmlFile jf) .jpo file
antlr.collections.AST	Parameters.parse(JmlFile jmlFile, antlr.collections.AST ast)
static Type	Type.addDims(JmlFile jmlFile, antlr.collections.AST dims_ast, Type t) count the number of dimensions in the given ast.
antlr.collections.AST	VarDeclParser.parse(JmlFile jmlFile, antlr.collections.AST ast)

Constructors in jml2b.structure.java with parameters of type JmlFile

AClass(JmlFile jf, antlr.collections.AST tree)

Class(JmlFile jf, antlr.collections.AST tree, Package class_package, Modifiers mods, boolean external)
Creates a new class in package class_package, with the given modifiers.

Constraint(JmlFile jf, antlr.collections.AST tree, Modifiers m, Class defining)

Declaration(JmlFile jf, antlr.collections.AST tree, Modifiers mods, Class defining)
Creates a new declaration from the given AST and modifiers.

Invariant(JmlFile jf, antlr.collections.AST tree, Modifiers m, Class defining)

Method(JmlFile jf, antlr.collections.AST tree, Modifiers m, Class defining)

NamedNode(JmlFile jf, antlr.collections.AST tree)

ParsedItem(JmlFile jf)
Constructs an item from a JML file.

ParsedItem(JmlFile jf, antlr.collections.AST tree)
Constructs an item from a JML file and an AST node.

Type(JmlFile jf, antlr.collections.AST tree)
Creates a new type from the given AST.

Uses of JmlFile in jml2b.structure.jml

Methods in jml2b.structure.jml with parameters of type JmlFile

antlr.collections.AST	Depends.parse(JmlFile jmlFile, antlr.collections.AST ast)
static ModifiesClause	ModifiesClause.create(JmlFile jf, antlr.collections.AST a) Create a concrete modifies clause depending of the AST content
static Represents	Represents.create(JmlFile jf, antlr.collections.AST tree, Modifiers m, Class defining) Creates an empty represent clause from a loaded file.
antlr.collections.AST	Represents.parse(JmlFile jmlFile, antlr.collections.AST ast)
static void	SpecCase.parseLabel(java.util.Vector labels, antlr.collections.AST a, JmlFile jmlFile) Parses the label clause of a specification case.
antlr.collections.AST	SpecCase.parseSpecBlock(JmlFile file, antlr.collections.AST tree) Parses the content of a lightweight spec case.
int	SpecCase.parseExsures(JmlFile jmlFile, antlr.collections.AST a, int first_line) Parse the content of an exsures clause, returning the new value for first_line.
int	SpecCase.parseEnsures(JmlFile jmlFile, antlr.collections.AST a, int first_line) Parses the content of the ensures clause, and returns the new value for first_line.
int	SpecCase.parseModifies(JmlFile jmlFile, antlr.collections.AST a, int first_line) Parses the modifies clause, and returns the updated value of first_line.

Constructors in jml2b.structure.jml with parameters of type JmlFile

Depends(JmlFile jf, antlr.collections.AST tree, Modifiers m, Class defining)
Constructs an empty depends clause that will be fill at parsing.

Represents(JmlFile jf, antlr.collections.AST tree, Modifiers m, Class defining)
Constructs an empty represent clause from a loaded file.

Uses of JmlFile in jml2b.structure.statement

Methods in jml2b.structure.statement with parameters of type JmlFile

static Expression	Expression.createE(JmlFile jf, antlr.collections.AST tree) Creates an expression from an AST node.
void	StLoops.parseModifies(JmlFile jmlFile, antlr.collections.AST a) Parses a modifies clause.
static Statement	Statement.createS(JmlFile jf, antlr.collections.AST tree) Creates a statement from an AST.

Constructors in jml2b.structure.statement with parameters of type JmlFile

QuantifiedVar(JmlFile jf, Type type, antlr.collections.AST ast)

Uses of JmlFile in jml2b.util

Methods in jml2b.util that return JmlFile

JmlFile

JmlSourceEntryFile.loadFile(boolean external) /** Load the given Java/JML file and return a new JmlFile structure