Uses of Class
jml2b.structure.java.ParsedItem

Packages that use ParsedItem

jml2b.exceptions
jml2b.formula	Provides the classes necessary to create and manage formulas.
jml2b.languages.java
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.

Uses of ParsedItem in jml2b.exceptions

Constructors in jml2b.exceptions with parameters of type ParsedItem

LinkException(java.lang.String message, ParsedItem b)

PogException(java.lang.String msg, ParsedItem b)
Constructs an exception and add an error into the error handler.

TypeCheckException(java.lang.String message, ParsedItem b)

Uses of ParsedItem in jml2b.formula

Methods in jml2b.formula with parameters of type ParsedItem

void	TerminalForm.setBox(ParsedItem box) Sets the box.

Uses of ParsedItem in jml2b.languages.java

Subclasses of ParsedItem in jml2b.languages.java

class

JavaType

Uses of ParsedItem in jml2b.pog.util

Subclasses of ParsedItem in jml2b.pog.util

class

TemporaryField This class provides services to create and use temporary fields that are usefull during the proof obligation calculation.

Constructors in jml2b.pog.util with parameters of type ParsedItem

ColoredInfo(ParsedItem b)
Constructs a green colored info

ColoredInfo(ParsedItem b, byte c)
Constructs a red colored info or a blue without additional informations.

ColoredInfo(ParsedItem b, byte c, java.lang.String s)
Constructs a blue colored info with informations.

TemporaryField(ParsedItem pi, Modifiers m, Type t, java.lang.String n, Expression a)
Constructs a temporary field from a field with a new name.

TemporaryField(ParsedItem pi, Type t, java.lang.String n)
Constructs a tempory field with a given name and a given type.

Uses of ParsedItem in jml2b.structure

Subclasses of ParsedItem in jml2b.structure

class	AField
class	AMethod

Methods in jml2b.structure with parameters of type ParsedItem

abstract java.util.Vector

AMethod.getClonedSpecCases(ParsedItem pi)

Constructors in jml2b.structure with parameters of type ParsedItem

AField(ParsedItem pi, Modifiers mods)

AMethod(ParsedItem pi, Modifiers m, Class defining)

Uses of ParsedItem in jml2b.structure.bytecode

Subclasses of ParsedItem in jml2b.structure.bytecode

class	ClassDefaultConstructor
class	ClassField
class	ClassFile
class	ClassMethod

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

java.util.Vector

ClassMethod.getClonedSpecCases(ParsedItem pi)

Uses of ParsedItem in jml2b.structure.java

Subclasses of ParsedItem in jml2b.structure.java

class	AClass
class	Class Internal representation of classes.
class	Constraint
class	Constructor Specialisation of the Method class suitable for representing constructors.
class	Declaration Base class for representing declarations.
class	Field Class representing fields.
class	Invariant class representing invariants.
class	Method
class	NamedNode
class	Package class representing packages.
class	Type Class representing types.

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

void	Field.setParsedItem(ParsedItem pi)
LinkInfo	Identifier.linkFieldIdent(IJml2bConfiguration config, LinkContext ctx, ParsedItem ident_box)
java.util.Vector	Method.getClonedSpecCases(ParsedItem pi)
void	ParsedItem.setBox(ParsedItem b) Deines an item from another.
void	ParsedItem.change(ParsedItem pi)
void	Type.setParsedItem(ParsedItem pi)

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

Declaration(ParsedItem pi, Modifiers mods)
Creates a new instance with the given modifiers from the given parsed item.

Declaration(ParsedItem pi, Modifiers mods, Class defining)
Creates a new declaration instance.

Field(ParsedItem pi, Modifiers m, Type t, java.lang.String n, Expression a)

Field(ParsedItem pi, Type t, java.lang.String n)

Method(ParsedItem pi, Modifiers m, Class defining)

NamedNode(ParsedItem pi)

ParsedItem(ParsedItem b)
Constructs an item from another.

Uses of ParsedItem in jml2b.structure.jml

Subclasses of ParsedItem in jml2b.structure.jml

class	Depends This class implements a depends clause.
class	GuardedModifies This class implements a guarded modifies clause.
class	Modifies This class represents a modified variable.
class	ModifiesClause This class describes the content of a modifies clause.
class	ModifiesDot This class implements a modifies corresponding to a member field.
class	ModifiesEverything This class implements a \everything
class	ModifiesIdent This class corresponds to a modified field.
class	ModifiesLbrack This class implements a modifies corresponding to array elements, that is a[b], a[b..c] or a[*] where a, b and c are expressions.
class	ModifiesList This class describes the modifies clause as a list of Modifies elements.
class	ModifiesNothing This class implements a \nothing modifies clause.
class	Represents This abstract class describes a represents clause.
class	SpecArray This class defines the possible indexes set of an array in the modifies clause.
class	SpecArrayDotDot This class represents an indexes interval
class	SpecArrayExpr This class represents an index of an array
class	SpecArrayStar This class describes all the indexes of an array that are declared to be potentially modified.
class	SpecCase This class implements a specification case, that is a labelled record of requires, modifies, ensures and exsures.

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

void	Exsures.setParsedItem(ParsedItem pi)
void	GuardedModifies.setParsedItem(ParsedItem pi)
abstract void	ModifiesClause.setParsedItem(ParsedItem pi)
void	ModifiesEverything.setParsedItem(ParsedItem pi)
void	ModifiesList.setParsedItem(ParsedItem pi)
void	ModifiesNothing.setParsedItem(ParsedItem pi)
void	SpecCase.setParsedItem(ParsedItem pi)

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

ModifiesDot(ParsedItem pi, Type t, Formula f, ModifiesIdent m)
Constructs a modified identifier from a formula and a modified field.

ModifiesIdent(ParsedItem pi, Type t, Identifier ident)
Constructs a modified identifier from an identifier.

Uses of ParsedItem in jml2b.structure.statement

Subclasses of ParsedItem in jml2b.structure.statement

class	ArrayInitializer This class implements an array initializer statement, that is, for instance, { {"car", "house" }, {"dog", "cat", "monkey"} }.
class	BinaryExp This class implements binary expressions.
class	Expression This class defines a Java expression.
class	IsSubtypeOfExp This class implements subtype JML expression, it corresponds to code like a <: b
class	MethodCallExp This class implements a method call expression
class	QuantifiedExp This class implements a quantified expression, that is \forall type var; body or \exists type var; body.
class	QuantifiedVar This class implements a list of quantified fields.
class	QuestionExp This class implements a question expression, that is a ? b :c
class	StAssert
class	Statement This class defines a Java statement.
class	StBlock This class implements a block statement
class	StControlFlowBreak This class implements a control flow break statement, that is a throw, a continue, a break or a return.
class	StDoWhile
class	StFor
class	StIf
class	StImplementsLabel This class implements an implements label statement.
class	StLabel
class	StLoops This abstract class implements a loop statement.
class	StSequence This class implements a sequence of two statements.
class	StSkip This class implements a skip statement.
class	StSpecBlock This class implements a specified block.
class	StSwitch This class implements a switch statement
class	StTry This class implements a try catch finally statement or a try catch or a try finally statement.
class	StVarDecl This class implements a set of local field declaration statement
class	TerminalExp This class implements a terminal expression.
class	TTypeExp This class implements expressions corresponding to types.
class	UnaryExp This class implements unary expressions.
class	WithTypeExp This class implements expression with type, that is object and array creation, casting and instanceof.

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

void	ArrayInitializer.setParsedItem(ParsedItem pi)
void	BinaryExp.setParsedItem(ParsedItem pi)
abstract void	Expression.setParsedItem(ParsedItem pi)
void	IsSubtypeOfExp.setParsedItem(ParsedItem pi)
void	MethodCallExp.setParsedItem(ParsedItem pi)
void	QuantifiedExp.setParsedItem(ParsedItem pi)
void	QuantifiedVar.setParsedItem(ParsedItem pi)
void	QuestionExp.setParsedItem(ParsedItem pi)
void	TTypeExp.setParsedItem(ParsedItem pi)
void	TerminalExp.setParsedItem(ParsedItem pi)
void	UnaryExp.setParsedItem(ParsedItem pi)
void	WithTypeExp.setParsedItem(ParsedItem pi)

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

QuantifiedVar(ParsedItem pi, Field f, QuantifiedVar n)
Constructs a quantified fields list form another one.

StSequence(ParsedItem pi, Statement left, Statement right)
Constructs a sequence from another one.