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

Inherited by edu.mit.csail.sdg.squander.spec.Tr.FrameConstructor, edu.mit.csail.sdg.squander.spec.Tr.SpecFieldBoundTranslator, and edu.mit.csail.sdg.squander.spec.Tr.SpecFieldTranslator.

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

[legend]

List of all members.

Classes
class	FrameConstructor
class	SpecFieldBoundTranslator
class	SpecFieldTranslator
Static Public Attributes
static Map< LocalDecls, List < String > >	absolutelyTerribleHack = new IdentityHashMap<LocalDecls, List<String>>()
Protected Member Functions
ForgeExpression	visitBinary (ForgeEnv env, Node tree, int op, Node leftTree, Node rightTree)
ForgeExpression	visitConditional (ForgeEnv env, Node condTree, Node leftTree, Node rightTree)
ForgeExpression	visitDecimal (ForgeEnv env, int i)
ForgeExpression	visitString (ForgeEnv env, String text)
ForgeExpression	visitTrue (ForgeEnv env)
ForgeExpression	visitFalse (ForgeEnv env)
ForgeExpression	visitNull (ForgeEnv env)
ForgeExpression	visitReturn (ForgeEnv env)
ForgeExpression	visitThrow (ForgeEnv env)
ForgeExpression	visitThis (ForgeEnv env)
ForgeExpression	visitSuper (ForgeEnv env)
ForgeExpression	visitArgument (ForgeEnv env, int i)
ForgeExpression	visitOld (ForgeEnv env, Node sub)
ForgeExpression	visitQuantification (ForgeEnv env, int op, List< String > names, List< String > mults, List< Node > sets, Node expr)
ForgeExpression	visitUnary (ForgeEnv env, Node tree, int op, Node expr)
ForgeExpression	visitName (ForgeEnv env, Node ident)
ForgeExpression	visitAmbiguous (ForgeEnv env, List< Node > idents)
ForgeExpression	visitBracket (ForgeEnv env, ForgeExpression primary, Node tree)
ForgeExpression	visitJoin (ForgeEnv env, ForgeExpression primary, Node tree)
ForgeExpression	visitJoinReflexive (ForgeEnv env, ForgeExpression primary, Node tree)
ForgeExpression	visitMethodCall (ForgeEnv env, ForgeExpression receiver, String id, Node arguments)
ForgeExpression	visitFieldDeclaration (ForgeEnv env, Node ident, int op, Node set, Node frame, Node constraint)
ForgeExpression	visitCastExpression (ForgeEnv env, Node type, Node sub)
ForgeExpression	visitFieldRelation (ForgeEnv env, Node type, Node ident)
ForgeExpression	visitArrayType (ForgeEnv env, Node base)
ForgeExpression	visitBooleanType (ForgeEnv env)
ForgeExpression	visitIntegralType (ForgeEnv env)
ForgeExpression	visitRefType (ForgeEnv env, Node source, List< Node > idents)
ForgeExpression	visitFrame (ForgeEnv env, List< ForgeExpression > locations, List< Node > fields, List< ForgeExpression > selectors, List< ForgeExpression > lowers, List< ForgeExpression > uppers)
Package Functions
	Tr ()
Private Member Functions
int[]	reverse (int i)

---

Detailed Description

Definition at line 72 of file Tr.java.

---

Constructor & Destructor Documentation

edu.mit.csail.sdg.squander.spec.Tr.Tr

(

)

[package]

Definition at line 76 of file Tr.java.

---

Member Function Documentation

int [] edu.mit.csail.sdg.squander.spec.Tr.reverse

(

int

i

)

[private]

Definition at line 362 of file Tr.java.

Referenced by edu.mit.csail.sdg.squander.spec.Tr.visitUnary().

ForgeExpression edu.mit.csail.sdg.squander.spec.Tr.visitAmbiguous	(	ForgeEnv	env,
		List< Node >	idents
	)			[protected]

Definition at line 403 of file Tr.java.

References edu.mit.csail.sdg.squander.spec.Tr.visitName().

ForgeExpression edu.mit.csail.sdg.squander.spec.Tr.visitArgument	(	ForgeEnv	env,
		int	i
	)			[protected]

Definition at line 225 of file Tr.java.

References edu.mit.csail.sdg.squander.spec.ForgeEnv.arg().

ForgeExpression edu.mit.csail.sdg.squander.spec.Tr.visitArrayType	(	ForgeEnv	env,
		Node	base
	)			[protected]

Definition at line 472 of file Tr.java.

References edu.mit.csail.sdg.squander.spec.ForgeEnv.ensureDomain().

ForgeExpression edu.mit.csail.sdg.squander.spec.Tr.visitBinary	(	ForgeEnv	env,
		Node	tree,
		int	op,
		Node	leftTree,
		Node	rightTree
	)			[protected]

Definition at line 79 of file Tr.java.

References edu.mit.csail.sdg.squander.spec.ForgeEnv.ensureAllInts().

ForgeExpression edu.mit.csail.sdg.squander.spec.Tr.visitBooleanType

(

ForgeEnv

env

)

[protected]

Definition at line 479 of file Tr.java.

References edu.mit.csail.sdg.squander.spec.ForgeEnv.booleanType().

ForgeExpression edu.mit.csail.sdg.squander.spec.Tr.visitBracket	(	ForgeEnv	env,
		ForgeExpression	primary,
		Node	tree
	)			[protected]

Definition at line 416 of file Tr.java.

References edu.mit.csail.sdg.squander.spec.ForgeEnv.arrayElems(), and edu.mit.csail.sdg.squander.spec.ForgeEnv.classForDomain().

ForgeExpression edu.mit.csail.sdg.squander.spec.Tr.visitCastExpression	(	ForgeEnv	env,
		Node	type,
		Node	sub
	)			[protected]

Definition at line 460 of file Tr.java.

ForgeExpression edu.mit.csail.sdg.squander.spec.Tr.visitConditional	(	ForgeEnv	env,
		Node	condTree,
		Node	leftTree,
		Node	rightTree
	)			[protected]

Definition at line 172 of file Tr.java.

ForgeExpression edu.mit.csail.sdg.squander.spec.Tr.visitDecimal	(	ForgeEnv	env,
		int	i
	)			[protected]

Definition at line 180 of file Tr.java.

References edu.mit.csail.sdg.squander.spec.ForgeEnv.intExpr().

ForgeExpression edu.mit.csail.sdg.squander.spec.Tr.visitFalse

(

ForgeEnv

env

)

[protected]

Definition at line 195 of file Tr.java.

References edu.mit.csail.sdg.squander.spec.ForgeEnv.falseExpr().

ForgeExpression edu.mit.csail.sdg.squander.spec.Tr.visitFieldDeclaration	(	ForgeEnv	env,
		Node	ident,
		int	op,
		Node	set,
		Node	frame,
		Node	constraint
	)			[protected]

Returns field declaration set expression for type information

Definition at line 454 of file Tr.java.

References edu.mit.csail.sdg.squander.spec.ForgeEnv.integerType().

ForgeExpression edu.mit.csail.sdg.squander.spec.Tr.visitFieldRelation	(	ForgeEnv	env,
		Node	type,
		Node	ident
	)			[protected]

Definition at line 465 of file Tr.java.

References edu.mit.csail.sdg.squander.spec.ForgeEnv.ensureGlobal(), and edu.mit.csail.sdg.squander.spec.ForgeEnv.globalVar().

ForgeExpression edu.mit.csail.sdg.squander.spec.Tr.visitFrame	(	ForgeEnv	env,
		List< ForgeExpression >	locations,
		List< Node >	fields,
		List< ForgeExpression >	selectors,
		List< ForgeExpression >	lowers,
		List< ForgeExpression >	uppers
	)			[protected]

Definition at line 496 of file Tr.java.

References edu.mit.csail.sdg.squander.spec.ForgeEnv.trueExpr().

ForgeExpression edu.mit.csail.sdg.squander.spec.Tr.visitIntegralType

(

ForgeEnv

env

)

[protected]

Definition at line 484 of file Tr.java.

References edu.mit.csail.sdg.squander.spec.ForgeEnv.integerType().

ForgeExpression edu.mit.csail.sdg.squander.spec.Tr.visitJoin	(	ForgeEnv	env,
		ForgeExpression	primary,
		Node	tree
	)			[protected]

Definition at line 438 of file Tr.java.

ForgeExpression edu.mit.csail.sdg.squander.spec.Tr.visitJoinReflexive	(	ForgeEnv	env,
		ForgeExpression	primary,
		Node	tree
	)			[protected]

Definition at line 443 of file Tr.java.

ForgeExpression edu.mit.csail.sdg.squander.spec.Tr.visitMethodCall	(	ForgeEnv	env,
		ForgeExpression	receiver,
		String	id,
		Node	arguments
	)			[protected]

Definition at line 448 of file Tr.java.

ForgeExpression edu.mit.csail.sdg.squander.spec.Tr.visitName	(	ForgeEnv	env,
		Node	ident
	)			[protected]

Definition at line 370 of file Tr.java.

References edu.mit.csail.sdg.squander.spec.ForgeEnv.ensureConst(), edu.mit.csail.sdg.squander.spec.ForgeEnv.ensureGlobal(), edu.mit.csail.sdg.squander.spec.ForgeEnv.findLocal(), edu.mit.csail.sdg.squander.spec.ForgeEnv.globalVar(), and edu.mit.csail.sdg.squander.spec.ForgeEnv.typeForCls().

Referenced by edu.mit.csail.sdg.squander.spec.Tr.visitAmbiguous().

ForgeExpression edu.mit.csail.sdg.squander.spec.Tr.visitNull

(

ForgeEnv

env

)

[protected]

Definition at line 200 of file Tr.java.

References edu.mit.csail.sdg.squander.spec.ForgeEnv.nullType().

ForgeExpression edu.mit.csail.sdg.squander.spec.Tr.visitOld	(	ForgeEnv	env,
		Node	sub
	)			[protected]

Definition at line 230 of file Tr.java.

References edu.mit.csail.sdg.squander.spec.ForgeEnv.setPreStateMode().

ForgeExpression edu.mit.csail.sdg.squander.spec.Tr.visitQuantification	(	ForgeEnv	env,
		int	op,
		List< String >	names,
		List< String >	mults,
		List< Node >	sets,
		Node	expr
	)			[protected]

Definition at line 235 of file Tr.java.

References edu.mit.csail.sdg.squander.spec.Tr.absolutelyTerribleHack, edu.mit.csail.sdg.squander.spec.ForgeEnv.addLocal(), edu.mit.csail.sdg.squander.spec.ForgeEnv.emptyDecls(), edu.mit.csail.sdg.squander.spec.ForgeEnv.intExpr(), edu.mit.csail.sdg.squander.spec.ForgeEnv.newLocalVar(), and edu.mit.csail.sdg.squander.spec.ForgeEnv.trueExpr().

ForgeExpression edu.mit.csail.sdg.squander.spec.Tr.visitRefType	(	ForgeEnv	env,
		Node	source,
		List< Node >	idents
	)			[protected]

Definition at line 489 of file Tr.java.

References edu.mit.csail.sdg.squander.spec.ForgeEnv.ensureDomain().

ForgeExpression edu.mit.csail.sdg.squander.spec.Tr.visitReturn

(

ForgeEnv

env

)

[protected]

Definition at line 205 of file Tr.java.

References edu.mit.csail.sdg.squander.spec.ForgeEnv.returnVar().

ForgeExpression edu.mit.csail.sdg.squander.spec.Tr.visitString	(	ForgeEnv	env,
		String	text
	)			[protected]

Definition at line 185 of file Tr.java.

References edu.mit.csail.sdg.squander.spec.ForgeEnv.stringExpr().

ForgeExpression edu.mit.csail.sdg.squander.spec.Tr.visitSuper

(

ForgeEnv

env

)

[protected]

Definition at line 220 of file Tr.java.

ForgeExpression edu.mit.csail.sdg.squander.spec.Tr.visitThis

(

ForgeEnv

env

)

[protected]

Definition at line 215 of file Tr.java.

References edu.mit.csail.sdg.squander.spec.ForgeEnv.thisVar().

ForgeExpression edu.mit.csail.sdg.squander.spec.Tr.visitThrow

(

ForgeEnv

env

)

[protected]

Definition at line 210 of file Tr.java.

References edu.mit.csail.sdg.squander.spec.ForgeEnv.throwVar().

ForgeExpression edu.mit.csail.sdg.squander.spec.Tr.visitTrue

(

ForgeEnv

env

)

[protected]

Definition at line 190 of file Tr.java.

References edu.mit.csail.sdg.squander.spec.ForgeEnv.trueExpr().

ForgeExpression edu.mit.csail.sdg.squander.spec.Tr.visitUnary	(	ForgeEnv	env,
		Node	tree,
		int	op,
		Node	expr
	)			[protected]

Definition at line 323 of file Tr.java.

References edu.mit.csail.sdg.squander.spec.ForgeEnv.ensureInt(), edu.mit.csail.sdg.squander.spec.ForgeEnv.ensureNum(), and edu.mit.csail.sdg.squander.spec.Tr.reverse().

---

Member Data Documentation

Map<LocalDecls, List<String> > edu.mit.csail.sdg.squander.spec.Tr.absolutelyTerribleHack = new IdentityHashMap<LocalDecls, List<String>>() [static]

Definition at line 74 of file Tr.java.

Referenced by edu.mit.csail.sdg.squander.spec.Tr.visitQuantification().

---

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

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