Uses of Interface
fmrisc.ProgramExplorer.InOut.SourcePosition

Packages that use SourcePosition

Package	Description
fmrisc.ProgramExplorer.InOut
fmrisc.ProgramExplorer.Parser
fmrisc.ProgramExplorer.Semantics
fmrisc.ProgramExplorer.SWT
fmrisc.ProgramExplorer.Syntax
fmrisc.ProgramExplorer.Syntax.Logic
fmrisc.ProgramExplorer.Syntax.Program
fmrisc.ProgramExplorer.Syntax.Spec
fmrisc.ProgramExplorer.Tasks

Uses of SourcePosition in fmrisc.ProgramExplorer.InOut

Classes in fmrisc.ProgramExplorer.InOut that implement SourcePosition

Modifier and Type	Class and Description
class	SourceAnnotationPosition An annotation position in a source file with a position inside the annotation.
class	SourcePositionClass A position in a source file.
class	StringSourcePosition A position within a text represented by a string.

Methods in fmrisc.ProgramExplorer.InOut that return SourcePosition

Modifier and Type	Method and Description
SourcePosition	ErrorStream.getPosition() Get current source position.
SourcePosition	SourceAnnotation.getPosition() Get the source position of the annotation.
SourcePosition[]	Source.getPositions() Get positions for this source.
SourcePosition	Source.newPosition(int line, int column) Construct position in this source.
SourcePosition	SourceAnnotation.newPosition(int line, int column) Construct position in this source.

Methods in fmrisc.ProgramExplorer.InOut with parameters of type SourcePosition

Modifier and Type	Method and Description
void	ErrorStream.newError(SourcePosition pos, java.lang.String message) Generate a new error.
void	Source.register(SourcePosition pos) Register position for this source.
void	ErrorStream.setPosition(SourcePosition pos) Set current source position.

Constructors in fmrisc.ProgramExplorer.InOut with parameters of type SourcePosition

Constructor and Description
SourceAnnotation(SourcePosition pos, java.lang.String text) Construct a source annotation.

Uses of SourcePosition in fmrisc.ProgramExplorer.Parser

Methods in fmrisc.ProgramExplorer.Parser that return SourcePosition

Modifier and Type	Method and Description
SourcePosition	MiniJavaParser.getPosition()
SourcePosition	SpecLangParser.getPosition()
SourcePosition	SpecLangParser.getPosition(org.antlr.runtime.Token token)

Methods in fmrisc.ProgramExplorer.Parser with parameters of type SourcePosition

Modifier and Type	Method and Description
void	MiniJavaParser.annotateClass(ClassDeclaration tree, org.antlr.runtime.Token token, SourcePosition pos)
void	MiniJavaParser.annotateLoop(LoopStatement tree, org.antlr.runtime.Token token, SourcePosition pos)
void	MiniJavaParser.annotateMethod(ParamDeclaration tree, org.antlr.runtime.Token token, SourcePosition pos)
void	MiniJavaParser.annotateStatement(Statement tree, org.antlr.runtime.Token token, SourcePosition pos)
void	MiniJavaParser.annotateUnit(ClassDeclaration tree, org.antlr.runtime.Token token, SourcePosition pos)

Constructors in fmrisc.ProgramExplorer.Parser with parameters of type SourcePosition

Constructor and Description
SpecLangLexer(org.antlr.runtime.CharStream input, ErrorStream error, SourcePosition pos)
SpecLangParser(org.antlr.runtime.TokenStream input, ErrorStream error, SourcePosition pos, java.lang.String text)

Uses of SourcePosition in fmrisc.ProgramExplorer.Semantics

Methods in fmrisc.ProgramExplorer.Semantics with parameters of type SourcePosition

Modifier and Type	Method and Description
void	TCCGenerator.prove(java.lang.String name, SourcePosition position, Formula formula, StateType resultType, Name[] stateVars, Name[] stateExcs) Create a new task to prove the given formula.

Uses of SourcePosition in fmrisc.ProgramExplorer.SWT

Methods in fmrisc.ProgramExplorer.SWT with parameters of type SourcePosition

Modifier and Type	Method and Description
void	TopWindow.addAnnotation(SourcePosition pos, java.lang.String text) Add annotation with given text at specified source position.
void	TopWindow.addMarker(SourcePosition pos, boolean marker) Add marker at specified source position.
void	TopWindow.displaySource(SourcePosition pos, boolean marker) Display source at denoted position.

Uses of SourcePosition in fmrisc.ProgramExplorer.Syntax

Methods in fmrisc.ProgramExplorer.Syntax that return SourcePosition

Modifier and Type	Method and Description
SourcePosition	ASTSourceBase.getPosition() Get the position of this node in the source code (may be null).
SourcePosition	ASTSource.getPosition() Get the position of this statement in the source code.

Methods in fmrisc.ProgramExplorer.Syntax with parameters of type SourcePosition

Modifier and Type	Method and Description
void	Identifier.setPosition(SourcePosition position) Set the position of this identifier in the source code.
void	ASTSourceBase.setPosition(SourcePosition position) Set the position of this node in the source code.
void	ASTSource.setPosition(SourcePosition position) Set the position of this statement in the source code.

Uses of SourcePosition in fmrisc.ProgramExplorer.Syntax.Logic

Methods in fmrisc.ProgramExplorer.Syntax.Logic that return SourcePosition

Modifier and Type	Method and Description
SourcePosition	TypedIdentifier.getPosition() Get the position of this node in the source code (may be null).
SourcePosition	ExpressionBase.getPosition() Get the position of this node in the source code (may be null).
SourcePosition	DeclarationBase.getPosition() Get the position of this node in the source code (may be null).

Methods in fmrisc.ProgramExplorer.Syntax.Logic with parameters of type SourcePosition

Modifier and Type	Method and Description
void	TypedIdentifier.setPosition(SourcePosition position) Set the position of this node in the source code.
void	ExpressionBase.setPosition(SourcePosition position) Set the position of this node in the source code.
void	DeclarationBase.setPosition(SourcePosition position) Set the position of this node in the source code.

Uses of SourcePosition in fmrisc.ProgramExplorer.Syntax.Program

Methods in fmrisc.ProgramExplorer.Syntax.Program that return SourcePosition

Modifier and Type	Method and Description
SourcePosition	ProgramAnnotationBase.getPosition() Get the position of this node in the source code (may be null).

Methods in fmrisc.ProgramExplorer.Syntax.Program with parameters of type SourcePosition

Modifier and Type	Method and Description
void	ProgramAnnotationBase.setPosition(SourcePosition position) Set the position of this node in the source code.
void	ForLoopStatement.setPosition(SourcePosition position) Set the position of this node in the source code.

Uses of SourcePosition in fmrisc.ProgramExplorer.Syntax.Spec

Methods in fmrisc.ProgramExplorer.Syntax.Spec with parameters of type SourcePosition

Modifier and Type	Method and Description
static UnitSpec	UnitSpec.construct(java.lang.String text, ErrorStream error, SourcePosition pos) Construct unit specification from denoted text.
static ClassSpec	ClassSpec.construct(java.lang.String text, ErrorStream error, SourcePosition pos) Construct class specification from denoted text.
static StatementSpec	StatementSpec.construct(java.lang.String text, ErrorStream error, SourcePosition pos) Construct method specification from denoted text.
static LoopSpec	LoopSpec.construct(java.lang.String text, ErrorStream error, SourcePosition pos) Construct loop specification from denoted text.
static MethodSpec	MethodSpec.construct(java.lang.String text, ErrorStream error, SourcePosition pos) Construct method specification from denoted text.

Uses of SourcePosition in fmrisc.ProgramExplorer.Tasks

Methods in fmrisc.ProgramExplorer.Tasks that return SourcePosition

Modifier and Type	Method and Description
SourcePosition	TaskBase.getPosition() Get source code position linked to this task (null, if none)
SourcePosition	Task.getPosition() Get source code position linked to this task (null, if none)

Constructors in fmrisc.ProgramExplorer.Tasks with parameters of type SourcePosition

Constructor and Description
FailedTask(java.lang.String tag, java.lang.String name, java.lang.String message, SourcePosition pos, java.io.File parent) Construct a failed task.
InvariantTask(ParamSymbol method, Statement stat, Formula goal, Formula invariant, SourcePosition pos, Formula cond, Formula body, java.io.File parent, StateType stateType, java.util.Set<VariableSymbol> variables, java.util.Set<ClassSymbol> exceptions, java.util.Vector<TheorySymbol> theories, Declaration[][] decls, ErrorStream out) Construct an invariant verification task.
TypeCheckingTask(TheorySymbol tsymbol, java.lang.String name, SourcePosition position, java.io.File dir, StateType resultType, Name[] stateVars, Name[] stateExcs, java.util.Vector<TheorySymbol> theories, Declaration[][] decls, Formula goal, ErrorStream out) Create task of proving a type-checking condition.