jml2b.structure.java
Class ParsedItem

java.lang.Object
  jml2b.util.Profiler
      jml2b.structure.java.ParsedItem

All Implemented Interfaces:

java.io.Serializable

Direct Known Subclasses:

GuardedModifies, Modifies, ModifiesClause, NamedNode, QuantifiedVar, SpecArray, SpecCase, Statement, Type

public class ParsedItem

extends Profiler

implements java.io.Serializable

This class provides features to store informations that allow to locate a parsed items. Those informations are the file where the item is located, with the line, the column and its length.

Author:

L. Burdy

See Also:

Serialized Form

Constructor Summary

ParsedItem()
Constructs a default item.

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.

ParsedItem(ParsedItem b)
Constructs an item from another.

Method Summary

void	change(ParsedItem pi)
void	change(java.util.Vector pi)
int	getColumn() Returns the column.
JmlFile	getJmlFile() Returns the file.
int	getLine() Returns the line.
void	save(JpoOutputStream s) Saves the item in a .jpo file
void	setBox(ParsedItem b) Deines an item from another.

Methods inherited from class jml2b.util.Profiler

runGC

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Constructor Detail

ParsedItem

public ParsedItem()

Constructs a default item.

ParsedItem

public ParsedItem(JmlFile jf)

Constructs an item from a JML file.

Parameters:

jf - The file

ParsedItem

public ParsedItem(JmlFile jf,
                  antlr.collections.AST tree)

Constructs an item from a JML file and an AST node.

Parameters:

jf - The file

tree - The AST node from which the line, the column and the length are extracted

ParsedItem

public ParsedItem(ParsedItem b)

Constructs an item from another.

Parameters:

b - The item where informations are collected

Method Detail

setBox

public final void setBox(ParsedItem b)

Deines an item from another.

Parameters:

b - The item where informations are collected

save

public final void save(JpoOutputStream s)
                throws java.io.IOException

Saves the item in a .jpo file

Parameters:

s - output stream for the jpo file

Throws:

java.io.IOException

getLine

public final int getLine()

Returns the line.

Returns:

line

getColumn

public final int getColumn()

Returns the column.

Returns:

column

getJmlFile

public final JmlFile getJmlFile()

Returns the file.

Returns:

jmlFile

change

public final void change(ParsedItem pi)

change

public final void change(java.util.Vector pi)