org.multijava.mjc
Class CVariableState

java.lang.Object
  org.multijava.mjc.CVariableState

All Implemented Interfaces:

Cloneable

public class CVariableState

extends Object

implements Cloneable

The class stores information about the definitely assigned state of a variable or field. See JLS2, chapter 16.

Version:

$Revision: 1.16 $

Author:

Curtis Clifton

Field Summary
private  boolean	isDefinitelyAssigned           Indicates that the variable represented by this definitely has been initialized.
private  boolean	maybeAssigned           Indicates that the variable represented by this may have been initialized.
private  VariableDescriptor	variableDesc           A descriptor for the field or variable (i.e., slot) tracked by this state.

 

Constructor Summary

CVariableState()           Create a variable state corresponding to a newly allocated variable.

 

Method Summary
Object	clone()
CVariableState	duplicate()           Returns a duplicate of this.
boolean	equals(Object other)
int	hashCode()
String	ident()           Returns the (unqualified) identifier of the slot tracked by this.
void	initialize()           Mutates the state of this to indicate that the corresponding variable has been initialized in the local control flow.
boolean	isDefinitelyAssigned()           Returns true if the variable represented by this is definitely initialized (i.e., is definitely assigned according to JLS2, 16).
boolean	isDefinitelyUnassigned()           Returns true if the variable represented by this is definitely not initialized (i.e., is definitely unassigned according to JLS2, 16).
boolean	isFinal()           Returns true if the slot tracked by this is declared final.
CVariableState	mergeWith(CVariableState other)           Mutates the state of this to indicate the result of merging with the given variable state.
void	setDescriptor(VariableDescriptor varDesc)           Sets the descriptor of the slot whose state is tracked by this.
String	toString()
void	tryFinallyMergeWith(CVariableState tryVariableState)           Sets the definite assignment state of this using the special merge logic appropriate for combining the definite assignment information from a finally block (as represented by this) with the definite assignment information from a try-block.

 

Methods inherited from class java.lang.Object

finalize, getClass, notify, notifyAll, wait, wait, wait

 

Field Detail

maybeAssigned

private boolean maybeAssigned

Indicates that the variable represented by this may have been initialized.

isDefinitelyAssigned

private boolean isDefinitelyAssigned

Indicates that the variable represented by this definitely has been initialized.

variableDesc

private VariableDescriptor variableDesc

A descriptor for the field or variable (i.e., slot) tracked by this state. Descriptor is only initialized if the slot may be initialized.

CVariableState

public CVariableState()

Create a variable state corresponding to a newly allocated variable.

clone

public Object clone()

Overrides:

clone in class Object

toString

public String toString()

Overrides:

toString in class Object

duplicate

public CVariableState duplicate()

Returns a duplicate of this. Utility method allows clients to avoid typecast when cloning this.

 ensures \fresh(\result) && \result.equals(this);
 

isDefinitelyAssigned

public boolean isDefinitelyAssigned()

Returns true if the variable represented by this is definitely initialized (i.e., is definitely assigned according to JLS2, 16).

isDefinitelyUnassigned

public boolean isDefinitelyUnassigned()

Returns true if the variable represented by this is definitely not initialized (i.e., is definitely unassigned according to JLS2, 16).

initialize

public void initialize()

Mutates the state of this to indicate that the corresponding variable has been initialized in the local control flow.

mergeWith

public CVariableState mergeWith(CVariableState other)

Mutates the state of this to indicate the result of merging with the given variable state.

 {|
   requires other == null;
   modifiable objectState;
   ensures (* result is equivalent to the case where other != null &&
              other.isDefinitelyUnassigned() *);
   ensures \result == this;
 |}
 also
 {|
   requires other != null;
   modifiable objectState;
   ensures (* mergeWith is symmetric *);
 
   ensures \old(this.isDefinitelyAssigned()) &&
 		other.isDefinitelyAssigned()
   		==> \result.isDefinitelyAssigned();
 
   ensures \old(this.isDefinitelyAssigned()) &&
 		!other.isDefinitelyAssigned()
   	 	==> !\result.isDefinitelyUnassigned() &&
 				!\result.isDefinitelyAssigned();
 
   ensures \old(this.isDefinitelyUnassigned()) &&
 		other.isDefinitelyUnassigned()
 			==> \result.isDefinitelyUnassigned();
 
   ensures \old(!this.isDefinitelyAssigned() &&
 			!this.isDefinitelyUnassigned()) &&
 		!other.isDefinitelyAssigned()
   	 	==> !\result.isDefinitelyUnassigned() &&
 				!\result.isDefinitelyAssigned();
   ensures \result == this;
 |}
 

tryFinallyMergeWith

public void tryFinallyMergeWith(CVariableState tryVariableState)

Sets the definite assignment state of this using the special merge logic appropriate for combining the definite assignment information from a finally block (as represented by this) with the definite assignment information from a try-block.

Parameters:

tryVariableState - definite assignment state from a try block

equals

public boolean equals(Object other)

Overrides:

equals in class Object

hashCode

public int hashCode()

Overrides:

hashCode in class Object

setDescriptor

public void setDescriptor(VariableDescriptor varDesc)

Sets the descriptor of the slot whose state is tracked by this.

isFinal

public boolean isFinal()

Returns true if the slot tracked by this is declared final. Result is only valid if maybeAssigned.

ident

public String ident()

Returns the (unqualified) identifier of the slot tracked by this. Result is only valid if maybeAssigned.