---

VirtualMachine Class Reference

Inheritance diagram for VirtualMachine:[legend]Collaboration diagram for VirtualMachine:[legend]List of all members.

Public Methods
	VirtualMachine (String classname)
boolean	Backtrack ()
Path	buildPath ()
boolean	CheckInvariant (iProperty p)
FilenameLinePair	ErrorBackward ()
FilenameLinePair	ErrorForward ()
FilenameLinePair	ErrorInit ()
int	ErrorPathLength ()
int	Forward ()
ErrorTrailInterface	getErrorTrail ()
Path	getErrorTrail_from_file ()
Path	getErrorTrail_to_file ()
Path	getErrorTrail1 ()
iKernelState	getKernelState ()
int	getSafeMoves ()
iSystemState	getSystemState ()
int	nextThreadToExecute ()
int	previousThreadToExecute ()
void	printStackTrace ()
void	pushInitialSystemState ()
void	pushSystemState ()
void	reinit (String classname)
void	ShowErrorTrail ()
void	ShowErrorTrail (Path ePath)
int	simForward ()
void	SimulateErrorTrail (Path ePath)
	VirtualMachine ()
boolean	Backtrack ()
boolean	BuchiBacktrack ()
boolean	BuchiEvaluate (Method method)
boolean	BuchiEvaluate (Method method, Object[] arg)
int	BuchiForward ()
BuchiSet	BuchiGet ()
void	BuchiInitSch ()
void	BuchiObservable (String observable)
void	BuchiSetState (int buchi_state)
Path	buildPath ()
FilenameLinePair	ErrorBackward ()
FilenameLinePair	ErrorForward ()
FilenameLinePair	ErrorInit ()
int	ErrorPathLength ()
boolean	executePath (Path p)
boolean	executePath (Path p, Object state)
int	Forward ()
Reference	getClassReference (String name)
String	getErrorMessage ()
ErrorTrailInterface	getErrorTrail ()
Path	getErrorTrail_from_file ()
Path	getErrorTrail_to_file ()
Path	getErrorTrail1 ()
Path	getPath (byte[] p)
Reference	getReference (String name)
Object	getState ()
iSystemState	getSystemState ()
void	init (String[] arguments)
boolean	isDeadlocked ()
boolean	isTerminated ()
int	nextThreadToExecute ()
void	popState ()
void	popSystem ()
int	previousThreadToExecute ()
void	printStackTrace ()
void	pushState ()
void	pushSystem ()
void	reinit ()
void	removeState ()
void	setState (Object state)
void	ShowErrorTrail ()
void	ShowErrorTrail (Path path)
iScheduler	xForward (iScheduler sch)
Static Public Methods
void	activateGC ()
String	getStatus ()
SystemState	getSS ()
Static Public Attributes
HashPool	fieldsPool = new HashPool()
HashPool	framePool = new HashPool()
HashPool	objectInfoPool = new HashPool()
HashPool	threadPool = new HashPool()
JVMOptions	options
HashSet	observablePositions = new HashSet()
HashSet	observableLabels = new HashSet()
HashSet	observableInvokes = new HashSet()
HashSet	observableReturns = new HashSet()
Static Private Methods
void	setSS (SystemState ss)
Private Attributes
SystemState	system_state
KernelState	kernel_state
StateStack	stack = new StateStack()
boolean	first_max_stack_reached = true
String	mainClass
JVMPath	errorPath
int	pos_in_errorPath
Counter	matching_states
SystemState	ss
Stack	stateStoringStack
Stack	stateBacktrackStack
Stack	backtrackStack
boolean	maxDepthReached
String	classname
String[]	args
int	posInErrorPath
boolean	executingPath
LinkedList	path
boolean	initialState
Static Private Attributes
boolean	gc_needed = false
boolean	initial_state = true
SystemState	xss
String[]	partitionPath
BufferedReader	br

---

Detailed Description

This class represents the virtual machine. The virtual machine is able to move backward and forward one step at a time.

Definition at line 18 of file lib/jpf/gov/nasa/arc/ase/jpf/jvm/VirtualMachine.java.

---

Constructor & Destructor Documentation

VirtualMachine::VirtualMachine (    )  [inline]

Creates a new Virtual Machine. Definition at line 187 of file src/gov/nasa/arc/ase/jpf/jvm/VirtualMachine.java.

---

Member Function Documentation

boolean VirtualMachine::Backtrack (    )  [inline]

Moves one step backward. Definition at line 192 of file src/gov/nasa/arc/ase/jpf/jvm/VirtualMachine.java.

FilenameLinePair VirtualMachine::ErrorBackward (    )  [inline]

Moves backward in the error path. Definition at line 341 of file src/gov/nasa/arc/ase/jpf/jvm/VirtualMachine.java.

FilenameLinePair VirtualMachine::ErrorForward (    )  [inline]

Moves forward in the simulation. Definition at line 353 of file src/gov/nasa/arc/ase/jpf/jvm/VirtualMachine.java.

FilenameLinePair VirtualMachine::ErrorInit (    )  [inline]

Initializes error simulation. Definition at line 373 of file src/gov/nasa/arc/ase/jpf/jvm/VirtualMachine.java.

int VirtualMachine::ErrorPathLength (    )  [inline]

Length of the erro path. Definition at line 387 of file src/gov/nasa/arc/ase/jpf/jvm/VirtualMachine.java.

int VirtualMachine::Forward (    )  [inline]

Moves one step forward. Definition at line 435 of file src/gov/nasa/arc/ase/jpf/jvm/VirtualMachine.java.

void VirtualMachine::ShowErrorTrail (  Path   path )  [inline]

Prints the content of an error trail. Definition at line 1051 of file src/gov/nasa/arc/ase/jpf/jvm/VirtualMachine.java.

void VirtualMachine::ShowErrorTrail (    )  [inline]

Prints and saves the error trace. Definition at line 1037 of file src/gov/nasa/arc/ase/jpf/jvm/VirtualMachine.java.

Path VirtualMachine::buildPath (    )  [inline]

Creates a path to the current state. Definition at line 328 of file src/gov/nasa/arc/ase/jpf/jvm/VirtualMachine.java.

ErrorTrailInterface VirtualMachine::getErrorTrail (    )  [inline]

Create a new error trace. Definition at line 532 of file src/gov/nasa/arc/ase/jpf/jvm/VirtualMachine.java.

Path VirtualMachine::getErrorTrail1 (    )  [inline]

Returns an error trail. Definition at line 637 of file src/gov/nasa/arc/ase/jpf/jvm/VirtualMachine.java.

Path VirtualMachine::getErrorTrail_from_file (    )  [inline]

Read the error trail and returns a path that can be simulated. Definition at line 561 of file src/gov/nasa/arc/ase/jpf/jvm/VirtualMachine.java.

SystemState VirtualMachine::getSS (    )  [inline, static]

Gets the thread local system state. Definition at line 678 of file src/gov/nasa/arc/ase/jpf/jvm/VirtualMachine.java.

iSystemState VirtualMachine::getSystemState (    )  [inline]

Gets the system state. Definition at line 691 of file src/gov/nasa/arc/ase/jpf/jvm/VirtualMachine.java.

void VirtualMachine::init (  String   arguments[] )  [inline]

Initialize the virtual machine. Creates the main thread, passes the arguments to the main function and store the initial state. Parameters: arguments   the argument strings Definition at line 700 of file src/gov/nasa/arc/ase/jpf/jvm/VirtualMachine.java.

int VirtualMachine::nextThreadToExecute (    )  [inline]

Returns the identifier of the next thread to be executed. Definition at line 775 of file src/gov/nasa/arc/ase/jpf/jvm/VirtualMachine.java.

void VirtualMachine::popState (    )  [inline]

Restore the state and backtracking information. Definition at line 835 of file src/gov/nasa/arc/ase/jpf/jvm/VirtualMachine.java.

int VirtualMachine::previousThreadToExecute (    )  [inline]

Returns the identified of the thread that just executed. Definition at line 847 of file src/gov/nasa/arc/ase/jpf/jvm/VirtualMachine.java.

void VirtualMachine::printStackTrace (    )  [inline]

Prints the current stack trace. Definition at line 860 of file src/gov/nasa/arc/ase/jpf/jvm/VirtualMachine.java.

void VirtualMachine::pushState (    )  [inline]

Saves the state of the system. Definition at line 866 of file src/gov/nasa/arc/ase/jpf/jvm/VirtualMachine.java.

void VirtualMachine::pushSystem (    )  [inline]

Saves the backtracking information. Definition at line 873 of file src/gov/nasa/arc/ase/jpf/jvm/VirtualMachine.java.

void VirtualMachine::reinit (    )  [inline]

Reinitializes the virtual machine. Definition at line 881 of file src/gov/nasa/arc/ase/jpf/jvm/VirtualMachine.java.

void VirtualMachine::setSS (  SystemState   ss )  [inline, static, private]

Sets the thread local system state. Definition at line 1019 of file src/gov/nasa/arc/ase/jpf/jvm/VirtualMachine.java.

void VirtualMachine::setState (  Object   state )  [inline]

Restores the machine to a state from the heuristic queue. Definition at line 1029 of file src/gov/nasa/arc/ase/jpf/jvm/VirtualMachine.java.

---

Member Data Documentation

String [] VirtualMachine::args [private]

The arguments to the main class. Definition at line 97 of file src/gov/nasa/arc/ase/jpf/jvm/VirtualMachine.java.

Stack VirtualMachine::backtrackStack [private]

Backtrack stack. Definition at line 82 of file src/gov/nasa/arc/ase/jpf/jvm/VirtualMachine.java.

BufferedReader VirtualMachine::br [static, private]

Initial value: new BufferedReader( new InputStreamReader(System.in)) Definition at line 181 of file src/gov/nasa/arc/ase/jpf/jvm/VirtualMachine.java.

String VirtualMachine::classname [private]

The name of the main class. Definition at line 92 of file src/gov/nasa/arc/ase/jpf/jvm/VirtualMachine.java.

JVMPath VirtualMachine::errorPath [private]

The path to the error. Definition at line 102 of file src/gov/nasa/arc/ase/jpf/jvm/VirtualMachine.java.

boolean VirtualMachine::executingPath [private]

Set to true during path execution. Definition at line 112 of file src/gov/nasa/arc/ase/jpf/jvm/VirtualMachine.java.

boolean VirtualMachine::initialState [private]

Set to true at the initial state. Used to simulate a transition into the initial state itself. Definition at line 125 of file src/gov/nasa/arc/ase/jpf/jvm/VirtualMachine.java.

boolean VirtualMachine::maxDepthReached [private]

Used to print the max stack depth reached message only once. Definition at line 87 of file src/gov/nasa/arc/ase/jpf/jvm/VirtualMachine.java.

HashSet VirtualMachine::observableInvokes = new HashSet() [static]

Contains the list of invoke instructions which are observable. Definition at line 140 of file src/gov/nasa/arc/ase/jpf/jvm/VirtualMachine.java.

HashSet VirtualMachine::observableLabels = new HashSet() [static]

Contains the list of the labels which are observable. Definition at line 135 of file src/gov/nasa/arc/ase/jpf/jvm/VirtualMachine.java.

HashSet VirtualMachine::observablePositions = new HashSet() [static]

Contains the list of the positions which are observable. Definition at line 130 of file src/gov/nasa/arc/ase/jpf/jvm/VirtualMachine.java.

HashSet VirtualMachine::observableReturns = new HashSet() [static]

Contains the list of methods whose return instruction are observable. Definition at line 145 of file src/gov/nasa/arc/ase/jpf/jvm/VirtualMachine.java.

JVMOptions VirtualMachine::options [static]

A way to access the options specific to the JVM without using a cast. Definition at line 154 of file src/gov/nasa/arc/ase/jpf/jvm/VirtualMachine.java.

String [] VirtualMachine::partitionPath [static, private]

Initial value: { null, "gov.nasa.arc.ase.jpf.partition", "gov.nasa.arc.ase.jpf.jvm.partition", } Set of packages where to look for partition classes. The first entry is null and it is set as the package the main class is defined in at run time. Definition at line 175 of file src/gov/nasa/arc/ase/jpf/jvm/VirtualMachine.java.

LinkedList VirtualMachine::path [private]

Path to the current position. Definition at line 117 of file src/gov/nasa/arc/ase/jpf/jvm/VirtualMachine.java.

int VirtualMachine::posInErrorPath [private]

The current position in the error path. Definition at line 107 of file src/gov/nasa/arc/ase/jpf/jvm/VirtualMachine.java.

SystemState VirtualMachine::ss [private]

The state of the system. Definition at line 67 of file src/gov/nasa/arc/ase/jpf/jvm/VirtualMachine.java.

Stack VirtualMachine::stateBacktrackStack [private]

State backtrack information stack. Definition at line 77 of file src/gov/nasa/arc/ase/jpf/jvm/VirtualMachine.java.

Stack VirtualMachine::stateStoringStack [private]

State storing information stack. Definition at line 72 of file src/gov/nasa/arc/ase/jpf/jvm/VirtualMachine.java.

SystemState VirtualMachine::xss [static, private]

Thread local version of the system state. Definition at line 160 of file src/gov/nasa/arc/ase/jpf/jvm/VirtualMachine.java.

---

The documentation for this class was generated from the following files:

• lib/jpf/gov/nasa/arc/ase/jpf/jvm/VirtualMachine.java
• src/gov/nasa/arc/ase/jpf/jvm/VirtualMachine.java

---