jml2b.structure.java
Class JmlFile

java.lang.Object
  jml2b.structure.java.JmlFile

All Implemented Interfaces:

IJmlFile, java.io.Serializable

public class JmlFile

extends java.lang.Object

implements java.io.Serializable, IJmlFile

Class keeping information on Java/JML files. It basically contains a set of classes.

Author:

L. Burdy, A. Requet

See Also:

Serialized Form

Field Summary

JmlFileEntry	fileName FileName of the corresponding file (if any)
static long	jmlParserTime
static int	JPO_FILE_FORMAT_VERSION .jpo file
static long	loadedFilesCount

Constructor Summary

JmlFile()

JmlFile(java.io.File file_name, antlr.collections.AST a)

JmlFile(JmlFileEntry file_name, antlr.collections.AST a, boolean external)

JmlFile(java.lang.String fileName, java.util.Vector classes)

Method Summary

static Package	addPackages(antlr.collections.AST ast, Package pkg) parse a package AST clause, adding packages as needed.
java.lang.String	emit(IJml2bConfiguration config)
java.util.Enumeration	getClasses()
IJml2bConfiguration	getConfig()
java.lang.Object	getData(java.lang.Object key) Retrieve data previously stored using storeData.
java.util.Vector	getDepends()
antlr.collections.AST	getFileAST()
JmlFileEntry	getFileName() Return the filename corresponding to this file.
java.lang.String	getFileNameAbsolutePath()
java.lang.String	getFlatName() Returns the "flat name" for this JmlFile.
Package	getImportedClassPackage(java.lang.String class_name) return the package corresponding to the given imported class.
java.util.Enumeration	getImportedPackages()
static long	getJmlParserTime()
java.lang.String[]	getLangNames()
static long	getLoadedFilesCount()
int	getNbPo()
int	getNbPoProved()
int	getNbPoProved(java.lang.String prover)
Package	getPackage()
boolean	isExternal() Return true if the file correspond to an external file.
boolean	isImportedClass(java.lang.String class_name) Return true if the given class_name correspond to an imported class.
static boolean	isJmlFile(java.lang.String s)
void	link(IJml2bConfiguration config)
int	linkStatements(IJml2bConfiguration config) Links the statement parts of the file if needed.
void	mergeWith(JmlFile jf)
int	parse(IJml2bConfiguration config) Parse the file fills the package and import structures.
void	purgeObvious()
void	removeData(java.lang.Object key) Remove the data stored with the specified key.
static void	resetStats()
void	save(IJml2bConfiguration config, JpoOutputStream s) .jpo file
void	setDepends(java.util.Vector depends) Sets the depends.
void	storeData(java.lang.Object key, java.lang.Object data) Store the data using key so that the information can be retrieved using getUserData.
void	typeCheck(IJml2bConfiguration config) Links the statement parts of the file if needed.

Methods inherited from class java.lang.Object

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

Field Detail

fileName

public JmlFileEntry fileName

FileName of the corresponding file (if any)

jmlParserTime

public static long jmlParserTime

loadedFilesCount

public static long loadedFilesCount

JPO_FILE_FORMAT_VERSION

public static final int JPO_FILE_FORMAT_VERSION

.jpo file

See Also:

Constant Field Values

Constructor Detail

JmlFile

public JmlFile()

JmlFile

public JmlFile(java.io.File file_name,
               antlr.collections.AST a)

JmlFile

public JmlFile(JmlFileEntry file_name,
               antlr.collections.AST a,
               boolean external)

JmlFile

public JmlFile(java.lang.String fileName,
               java.util.Vector classes)

Method Detail

storeData

public void storeData(java.lang.Object key,
                      java.lang.Object data)

Store the data using key so that the information can be retrieved using getUserData.

Parameters:

key - the key to use for retrieving the data

data - the data that has to be stored.

getData

public java.lang.Object getData(java.lang.Object key)

Retrieve data previously stored using storeData.

removeData

public void removeData(java.lang.Object key)

Remove the data stored with the specified key.

Parameters:

key - the key corresponding to the information that should be removed.

getFlatName

public java.lang.String getFlatName()

Returns the "flat name" for this JmlFile.

The flat name is a name that can be used as a B machine name, and reduce the probability of name conflicts between different classes (such as classes with the same name in different packages).

It is currently equal to the name of the package this file belongs to, with dots replaced by underscores, and the name of the file without its extension. In case where the file belongs to the default package, the flat name correspond to the name of the file, without its extension.

getFileName

public JmlFileEntry getFileName()

Return the filename corresponding to this file.

getFileNameAbsolutePath

public java.lang.String getFileNameAbsolutePath()

isExternal

public boolean isExternal()

Return true if the file correspond to an external file.

isImportedClass

public boolean isImportedClass(java.lang.String class_name)

Return true if the given class_name correspond to an imported class.

getImportedClassPackage

public Package getImportedClassPackage(java.lang.String class_name)

return the package corresponding to the given imported class. (i.e. a class imported as import package.class_name;) return null if the class is not imported

parse

public int parse(IJml2bConfiguration config)

Parse the file

• fills the package and import structures.
• creates the class structures corresponding to the classes defined in this package

Returns:

the number of errors encountered.

link

public void link(IJml2bConfiguration config)
          throws Jml2bException

Throws:

Jml2bException

linkStatements

public int linkStatements(IJml2bConfiguration config)
                   throws Jml2bException

Links the statement parts of the file if needed.

Throws:

Jml2bException

typeCheck

public void typeCheck(IJml2bConfiguration config)
               throws Jml2bException

Links the statement parts of the file if needed.

Throws:

Jml2bException

getPackage

public Package getPackage()

getClasses

public java.util.Enumeration getClasses()

getImportedPackages

public java.util.Enumeration getImportedPackages()

isJmlFile

public static boolean isJmlFile(java.lang.String s)

addPackages

public static Package addPackages(antlr.collections.AST ast,
                                  Package pkg)

parse a package AST clause, adding packages as needed. return the corresponding package

getNbPo

public int getNbPo()

getNbPoProved

public int getNbPoProved(java.lang.String prover)

getNbPoProved

public int getNbPoProved()

getLoadedFilesCount

public static long getLoadedFilesCount()

getJmlParserTime

public static long getJmlParserTime()

resetStats

public static void resetStats()

mergeWith

public void mergeWith(JmlFile jf)

getDepends

public java.util.Vector getDepends()

Returns:

Vector

setDepends

public void setDepends(java.util.Vector depends)

Sets the depends.

Parameters:

depends - The depends to set

emit

public java.lang.String emit(IJml2bConfiguration config)

getLangNames

public java.lang.String[] getLangNames()

Specified by:

getLangNames in interface IJmlFile

getConfig

public IJml2bConfiguration getConfig()

Returns:

purgeObvious

public void purgeObvious()

getFileAST

public antlr.collections.AST getFileAST()

Returns:

save

public void save(IJml2bConfiguration config,
                 JpoOutputStream s)
          throws java.io.IOException

.jpo file

Throws:

java.io.IOException