edu.mit.csail.sdg.squander.spec.Frame Class Reference
[Specification]

Collaboration diagram for edu.mit.csail.sdg.squander.spec.Frame:

[legend]

List of all members.

Public Member Functions
	Frame (ForgeScene scene)
Set< GlobalVariable >	locations ()
ForgeExpression	instSelector (GlobalVariable g)
ForgeExpression	lowerBound (GlobalVariable g)
ForgeExpression	upperBound (GlobalVariable g)
void	add (GlobalVariable var, ForgeExpression location, ForgeExpression sel, ForgeExpression lower, ForgeExpression upper)
ForgeExpression	condition ()
ForgeExpression	modCond ()
ForgeExpression	modCond (GlobalVariable var)
ForgeExpression	lowerCond (GlobalVariable var)
ForgeExpression	upperCond (GlobalVariable var)
Set< GlobalVariable >	modifiable ()
String	toString ()
Private Member Functions
ForgeExpression	modCond (GlobalVariable var, ForgeExpression instSel, LocalVariable l)
Private Attributes
final ForgeScene	forgeScene
final Map< GlobalVariable, ForgeExpression >	locations
final Map< GlobalVariable, ForgeExpression >	selectors
final Map< GlobalVariable, ForgeExpression >	lowerBounds
final Map< GlobalVariable, ForgeExpression >	upperBounds
Set< GlobalVariable >	mods = null

---

Detailed Description

Frame condition. The roots of location may be local variables. The context of these variables is not specified in this class.

frame : set GlobalVariable -> ForgeExpression { (all var : GlobalVariable | one var.frame) }

Definition at line 27 of file Frame.java.

---

Constructor & Destructor Documentation

edu.mit.csail.sdg.squander.spec.Frame.Frame

(

ForgeScene

scene

)

Definition at line 36 of file Frame.java.

References edu.mit.csail.sdg.squander.spec.Frame.forgeScene, edu.mit.csail.sdg.squander.spec.Frame.locations(), edu.mit.csail.sdg.squander.spec.Frame.lowerBounds, edu.mit.csail.sdg.squander.spec.Frame.selectors, and edu.mit.csail.sdg.squander.spec.Frame.upperBounds.

---

Member Function Documentation

void edu.mit.csail.sdg.squander.spec.Frame.add	(	GlobalVariable	var,
		ForgeExpression	location,
		ForgeExpression	sel,
		ForgeExpression	lower,
		ForgeExpression	upper
	)

frame = no var.(frame) ? (frame) ++ var -> heap : (frame) ++ var -> (var.(frame) + heap)

If var stands for a spec field, the frame of the field is automatically added.

Parameters:

upper

Definition at line 60 of file Frame.java.

References edu.mit.csail.sdg.squander.spec.ForgeScene.fields(), edu.mit.csail.sdg.squander.spec.Frame.forgeScene, edu.mit.csail.sdg.squander.spec.Frame.locations(), edu.mit.csail.sdg.squander.spec.Frame.lowerBounds, edu.mit.csail.sdg.squander.spec.Frame.selectors, and edu.mit.csail.sdg.squander.spec.Frame.upperBounds.

ForgeExpression edu.mit.csail.sdg.squander.spec.Frame.condition

(

)

Requires that no additional relations are added to the scene afterwards.

Returns:

(all var : scene.globals() | no var.frame => (all quant | quant.var = quant.(var)) && (all var : scene.globals() | some var.frame => (all quant | quant.var != quant.(var) => quant in var.frame))

Definition at line 126 of file Frame.java.

References edu.mit.csail.sdg.squander.spec.Frame.forgeScene, edu.mit.csail.sdg.squander.spec.Frame.modCond(), edu.mit.csail.sdg.squander.spec.Frame.modifiable(), edu.mit.csail.sdg.squander.spec.ForgeScene.program, and edu.mit.csail.sdg.squander.spec.Frame.selectors.

Referenced by edu.mit.csail.sdg.squander.spec.Frame.toString().

ForgeExpression edu.mit.csail.sdg.squander.spec.Frame.instSelector

(

GlobalVariable

g

)

Definition at line 48 of file Frame.java.

References edu.mit.csail.sdg.squander.spec.Frame.selectors.

Set<GlobalVariable> edu.mit.csail.sdg.squander.spec.Frame.locations

(

)

Definition at line 44 of file Frame.java.

Referenced by edu.mit.csail.sdg.squander.spec.Frame.add(), edu.mit.csail.sdg.squander.spec.Frame.Frame(), and edu.mit.csail.sdg.squander.spec.Frame.modifiable().

ForgeExpression edu.mit.csail.sdg.squander.spec.Frame.lowerBound

(

GlobalVariable

g

)

Definition at line 49 of file Frame.java.

References edu.mit.csail.sdg.squander.spec.Frame.lowerBounds.

ForgeExpression edu.mit.csail.sdg.squander.spec.Frame.lowerCond

(

GlobalVariable

var

)

Definition at line 161 of file Frame.java.

References edu.mit.csail.sdg.squander.spec.Frame.lowerBounds, and edu.mit.csail.sdg.squander.spec.Frame.selectors.

ForgeExpression edu.mit.csail.sdg.squander.spec.Frame.modCond	(	GlobalVariable	var,
		ForgeExpression	instSel,
		LocalVariable	l
	)			[private]

Definition at line 179 of file Frame.java.

ForgeExpression edu.mit.csail.sdg.squander.spec.Frame.modCond

(

GlobalVariable

var

)

Definition at line 152 of file Frame.java.

References edu.mit.csail.sdg.squander.spec.Frame.forgeScene, edu.mit.csail.sdg.squander.spec.Frame.modCond(), edu.mit.csail.sdg.squander.spec.ForgeScene.program, and edu.mit.csail.sdg.squander.spec.Frame.selectors.

ForgeExpression edu.mit.csail.sdg.squander.spec.Frame.modCond

(

)

Definition at line 143 of file Frame.java.

References edu.mit.csail.sdg.squander.spec.Frame.forgeScene, and edu.mit.csail.sdg.squander.spec.ForgeScene.program.

Referenced by edu.mit.csail.sdg.squander.spec.Frame.condition(), and edu.mit.csail.sdg.squander.spec.Frame.modCond().

Set<GlobalVariable> edu.mit.csail.sdg.squander.spec.Frame.modifiable

(

)

Global variables for which old heap locations may be modified.

Returns:

{var : scene.globals() | some var.frame}

Definition at line 188 of file Frame.java.

References edu.mit.csail.sdg.squander.spec.ForgeScene.fields(), edu.mit.csail.sdg.squander.spec.Frame.forgeScene, edu.mit.csail.sdg.squander.spec.FrameInference.globals, edu.mit.csail.sdg.squander.spec.Frame.locations(), edu.mit.csail.sdg.squander.spec.Frame.mods, and edu.mit.csail.sdg.squander.spec.ForgeScene.nonAbstractSpecFields().

Referenced by edu.mit.csail.sdg.squander.spec.Frame.condition(), and edu.mit.csail.sdg.squander.spec.Frame.toString().

String edu.mit.csail.sdg.squander.spec.Frame.toString

(

)

Definition at line 234 of file Frame.java.

References edu.mit.csail.sdg.squander.spec.Frame.condition(), and edu.mit.csail.sdg.squander.spec.Frame.modifiable().

ForgeExpression edu.mit.csail.sdg.squander.spec.Frame.upperBound

(

GlobalVariable

g

)

Definition at line 50 of file Frame.java.

References edu.mit.csail.sdg.squander.spec.Frame.upperBounds.

ForgeExpression edu.mit.csail.sdg.squander.spec.Frame.upperCond

(

GlobalVariable

var

)

Definition at line 169 of file Frame.java.

References edu.mit.csail.sdg.squander.spec.Frame.selectors, and edu.mit.csail.sdg.squander.spec.Frame.upperBounds.

---

Member Data Documentation

final ForgeScene edu.mit.csail.sdg.squander.spec.Frame.forgeScene [private]

Definition at line 28 of file Frame.java.

Referenced by edu.mit.csail.sdg.squander.spec.Frame.add(), edu.mit.csail.sdg.squander.spec.Frame.condition(), edu.mit.csail.sdg.squander.spec.Frame.Frame(), edu.mit.csail.sdg.squander.spec.Frame.modCond(), and edu.mit.csail.sdg.squander.spec.Frame.modifiable().

final Map<GlobalVariable, ForgeExpression> edu.mit.csail.sdg.squander.spec.Frame.locations [private]

Definition at line 29 of file Frame.java.

Referenced by edu.mit.csail.sdg.squander.spec.Frame.add(), and edu.mit.csail.sdg.squander.spec.ClassSpec.translateSpecs().

final Map<GlobalVariable, ForgeExpression> edu.mit.csail.sdg.squander.spec.Frame.lowerBounds [private]

Definition at line 31 of file Frame.java.

Referenced by edu.mit.csail.sdg.squander.spec.Frame.add(), edu.mit.csail.sdg.squander.spec.Frame.Frame(), edu.mit.csail.sdg.squander.spec.Frame.lowerBound(), and edu.mit.csail.sdg.squander.spec.Frame.lowerCond().

Set<GlobalVariable> edu.mit.csail.sdg.squander.spec.Frame.mods = null [private]

Definition at line 34 of file Frame.java.

Referenced by edu.mit.csail.sdg.squander.spec.Frame.modifiable().

final Map<GlobalVariable, ForgeExpression> edu.mit.csail.sdg.squander.spec.Frame.selectors [private]

Definition at line 30 of file Frame.java.

Referenced by edu.mit.csail.sdg.squander.spec.Frame.add(), edu.mit.csail.sdg.squander.spec.Frame.condition(), edu.mit.csail.sdg.squander.spec.Frame.Frame(), edu.mit.csail.sdg.squander.spec.Frame.instSelector(), edu.mit.csail.sdg.squander.spec.Frame.lowerCond(), edu.mit.csail.sdg.squander.spec.Frame.modCond(), and edu.mit.csail.sdg.squander.spec.Frame.upperCond().

final Map<GlobalVariable, ForgeExpression> edu.mit.csail.sdg.squander.spec.Frame.upperBounds [private]

Definition at line 32 of file Frame.java.

Referenced by edu.mit.csail.sdg.squander.spec.Frame.add(), edu.mit.csail.sdg.squander.spec.Frame.Frame(), edu.mit.csail.sdg.squander.spec.Frame.upperBound(), and edu.mit.csail.sdg.squander.spec.Frame.upperCond().

---

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

• src/edu/mit/csail/sdg/squander/spec/Frame.java