fmrisc.ProgramExplorer.Tasks

Class MethodTasks

java.lang.Object

fmrisc.ProgramExplorer.Tasks.MethodTasks

public final class MethodTasks
extends java.lang.Object

The delayed generation of method-related tasks.

Constructor Summary

Constructors

Constructor and Description
MethodTasks()

Method Summary

Methods

Modifier and Type	Method and Description
static void	clearTasks() Clear the registered tasks.
static boolean	exist() Determine whether there are tasks.
static void	generateTasks(java.io.PrintWriter out) Generate those tasks for which the information has been previously registered.
static void	register(ParamSymbol method, StateType stateType, Name[] stateVars, Name[] stateExcs, java.util.Vector<TheorySymbol> theories, Declaration[][] decls, ErrorStream out) Register the construction of tasks for a given method.

Methods inherited from class java.lang.Object

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

Constructor Detail

MethodTasks

public MethodTasks()

Method Detail

register

public static void register(ParamSymbol method,
            StateType stateType,
            Name[] stateVars,
            Name[] stateExcs,
            java.util.Vector<TheorySymbol> theories,
            Declaration[][] decls,
            ErrorStream out)

Register the construction of tasks for a given method.

Parameters:

method - the symbol of a method.

stateType - the type of the current state (null, if none)

stateVars - the names of the modifiable variables (null, if none)

stateExcs - the names of the throwable exceptions (null, if none)

theories - the theories on which the following depend in dependence order.

decls - a sequence of declaration lists.

out - the stream to which to write error messages.

clearTasks

public static void clearTasks()

Clear the registered tasks.

exist

public static boolean exist()

Determine whether there are tasks.

Returns:

true iff there are tasks.

generateTasks

public static void generateTasks(java.io.PrintWriter out)

Generate those tasks for which the information has been previously registered.

Parameters:

out - the stream to which messages are written.