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

Collaboration diagram for edu.mit.csail.sdg.squander.spec.JavaScene:
Collaboration graph
[legend]

List of all members.

Public Member Functions

boolean isFinished ()
void addObj2spec (Object object, ClassSpec cs)
ClassSpec ensureClass (Class<?> cls)
ClassSpec ensureClass (JType.Unary type)
void finish ()
void setMethod (JMethod method)
void setArgs (Object[] methodArgs)
JMethod method ()
MethodSpec methodSpec ()
Collection< ClassSpec > classSpecs ()
Collection< Class<?> > classes ()
List< JType.Unary > jtypes (Class<?> cls)
ClassSpec classSpecForObj (Object o)
JType.Unary jtypeForObj (Object o)
ClassSpec classSpec (Unary jtype)
ClassSpec findSpec (Class cls, boolean ensureSingle)
void setCaller (Object caller)
Object caller ()
Object[] methodArgs ()
Collection< JField > specFields ()
Collection< ClassSpec > subTypes (JType.Unary jtype)
Collection< ClassSpec > subTypes (Class<?> cls)
void translateSpecs (ForgeScene forgeScene)

Private Member Functions

Collection< ClassSpec > subTypes (ClassSpec clsSpec)
ClassSpec createClassSpec (JType.Unary jtype)

Private Attributes

Map< JType.Unary, ClassSpec > classes = new HashMap<JType.Unary, ClassSpec>()
Map< Object, ClassSpec > obj2spec = new IdentityHashMap<Object, ClassSpec>()
JMethod method
Object caller
Object[] methodArgs = new Object[0]
boolean finished = false

Detailed Description

Definition at line 25 of file JavaScene.java.

Member Function Documentation

void edu.mit.csail.sdg.squander.spec.JavaScene.addObj2spec ( Object  object,
ClassSpec  cs 
)

Definition at line 38 of file JavaScene.java.

Referenced by edu.mit.csail.sdg.squander.engine.Heap2Bounds.newObject().

Object edu.mit.csail.sdg.squander.spec.JavaScene.caller (  ) 

Definition at line 154 of file JavaScene.java.

Collection<Class<?> > edu.mit.csail.sdg.squander.spec.JavaScene.classes (  ) 

Definition at line 122 of file JavaScene.java.

ClassSpec edu.mit.csail.sdg.squander.spec.JavaScene.classSpec ( Unary  jtype  ) 

Definition at line 140 of file JavaScene.java.

ClassSpec edu.mit.csail.sdg.squander.spec.JavaScene.classSpecForObj ( Object  o  ) 

Definition at line 138 of file JavaScene.java.

Referenced by edu.mit.csail.sdg.squander.serializer.special.SetSer.absFunc(), edu.mit.csail.sdg.squander.serializer.special.MapSer.absFunc(), edu.mit.csail.sdg.squander.serializer.special.ListSer.absFunc(), edu.mit.csail.sdg.squander.serializer.special.DefaultObjSer.absFunc(), and edu.mit.csail.sdg.squander.serializer.special.ArraySer.absFunc().

Collection<ClassSpec> edu.mit.csail.sdg.squander.spec.JavaScene.classSpecs (  ) 

Definition at line 112 of file JavaScene.java.

Referenced by edu.mit.csail.sdg.squander.spec.Spec.abstractConstraint(), edu.mit.csail.sdg.squander.spec.Spec.concreteConstraint(), edu.mit.csail.sdg.squander.spec.Spec.funcConstraint(), and edu.mit.csail.sdg.squander.spec.Spec.invariant().

ClassSpec edu.mit.csail.sdg.squander.spec.JavaScene.createClassSpec ( JType.Unary  jtype  )  [private]

Definition at line 206 of file JavaScene.java.

References edu.mit.csail.sdg.squander.spec.ClassSpec.addInvariant(), edu.mit.csail.sdg.squander.spec.ClassSpec.addSpecFieldSource(), and edu.mit.csail.sdg.squander.spec.ISpecProvider.extractClassSpec().

ClassSpec edu.mit.csail.sdg.squander.spec.JavaScene.ensureClass ( JType.Unary  type  ) 

Definition at line 44 of file JavaScene.java.

References edu.mit.csail.sdg.squander.spec.ClassSpec.addSuper(), and edu.mit.csail.sdg.squander.spec.ClassSpec.typecheck().

ClassSpec edu.mit.csail.sdg.squander.spec.JavaScene.ensureClass ( Class<?>  cls  ) 

Definition at line 40 of file JavaScene.java.

Referenced by edu.mit.csail.sdg.squander.spec.NameSpace.findField(), edu.mit.csail.sdg.squander.spec.TypeChecker.getFldOwner(), edu.mit.csail.sdg.squander.engine.ForgeConverter.initJavaScene(), edu.mit.csail.sdg.squander.engine.Heap2Bounds.newObject(), edu.mit.csail.sdg.squander.spec.TypeChecker.visitAmbiguous(), edu.mit.csail.sdg.squander.spec.TypeChecker.visitName(), and edu.mit.csail.sdg.squander.spec.TypeChecker.visitRefType().

ClassSpec edu.mit.csail.sdg.squander.spec.JavaScene.findSpec ( Class  cls,
boolean  ensureSingle 
)

Definition at line 141 of file JavaScene.java.

Referenced by edu.mit.csail.sdg.squander.spec.ForgeScene.MyEnv.arrayElems(), and edu.mit.csail.sdg.squander.spec.ForgeScene.MyEnv.arrayLength().

void edu.mit.csail.sdg.squander.spec.JavaScene.finish (  ) 

Definition at line 63 of file JavaScene.java.

Referenced by edu.mit.csail.sdg.squander.engine.ForgeConverter.setCallContext().

boolean edu.mit.csail.sdg.squander.spec.JavaScene.isFinished (  ) 

Definition at line 36 of file JavaScene.java.

Referenced by edu.mit.csail.sdg.squander.spec.ClassSpec.addInvariant(), edu.mit.csail.sdg.squander.spec.ClassSpec.addSpecField(), edu.mit.csail.sdg.squander.spec.ClassSpec.addSpecFieldSource(), and edu.mit.csail.sdg.squander.spec.ClassSpec.ensureField().

JType.Unary edu.mit.csail.sdg.squander.spec.JavaScene.jtypeForObj ( Object  o  ) 

Definition at line 139 of file JavaScene.java.

Referenced by edu.mit.csail.sdg.squander.spec.ForgeScene.createLiteral().

List<JType.Unary> edu.mit.csail.sdg.squander.spec.JavaScene.jtypes ( Class<?>  cls  ) 

Definition at line 129 of file JavaScene.java.

JMethod edu.mit.csail.sdg.squander.spec.JavaScene.method (  ) 

Definition at line 110 of file JavaScene.java.

Object [] edu.mit.csail.sdg.squander.spec.JavaScene.methodArgs (  ) 

Definition at line 155 of file JavaScene.java.

MethodSpec edu.mit.csail.sdg.squander.spec.JavaScene.methodSpec (  ) 

Definition at line 111 of file JavaScene.java.

References edu.mit.csail.sdg.squander.spec.JMethod.spec.

Referenced by edu.mit.csail.sdg.squander.engine.SquanderImpl.exeSpec(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.exeSpec(), edu.mit.csail.sdg.squander.engine.ForgeConverter.finish(), edu.mit.csail.sdg.squander.engine.ForgeConverter.getSpec(), and edu.mit.csail.sdg.squander.engine.ForgeConverter.proc().

void edu.mit.csail.sdg.squander.spec.JavaScene.setArgs ( Object[]  methodArgs  ) 

Definition at line 103 of file JavaScene.java.

Referenced by edu.mit.csail.sdg.squander.engine.ForgeConverter.setCallContext().

void edu.mit.csail.sdg.squander.spec.JavaScene.setCaller ( Object  caller  ) 

Definition at line 153 of file JavaScene.java.

Referenced by edu.mit.csail.sdg.squander.engine.ForgeConverter.setCallContext().

void edu.mit.csail.sdg.squander.spec.JavaScene.setMethod ( JMethod  method  ) 

Definition at line 98 of file JavaScene.java.

References edu.mit.csail.sdg.squander.spec.JMethod.spec, and edu.mit.csail.sdg.squander.spec.MethodSpec.typecheck().

Referenced by edu.mit.csail.sdg.squander.engine.ForgeConverter.setCallContext().

Collection<JField> edu.mit.csail.sdg.squander.spec.JavaScene.specFields (  ) 

Definition at line 157 of file JavaScene.java.

Referenced by edu.mit.csail.sdg.squander.engine.ForgeConverter.boundSpecFields().

Collection<ClassSpec> edu.mit.csail.sdg.squander.spec.JavaScene.subTypes ( ClassSpec  clsSpec  )  [private]

Definition at line 175 of file JavaScene.java.

References edu.mit.csail.sdg.squander.spec.ClassSpec.clz(), edu.mit.csail.sdg.squander.spec.ClassSpec.jtype, edu.mit.csail.sdg.squander.spec.ClassSpec.setSubs(), and edu.mit.csail.sdg.squander.spec.ClassSpec.subs.

Collection<ClassSpec> edu.mit.csail.sdg.squander.spec.JavaScene.subTypes ( Class<?>  cls  ) 

Definition at line 171 of file JavaScene.java.

Collection<ClassSpec> edu.mit.csail.sdg.squander.spec.JavaScene.subTypes ( JType.Unary  jtype  ) 

Definition at line 167 of file JavaScene.java.

Referenced by edu.mit.csail.sdg.squander.spec.ForgeScene.typeForCls().

void edu.mit.csail.sdg.squander.spec.JavaScene.translateSpecs ( ForgeScene  forgeScene  ) 

Definition at line 193 of file JavaScene.java.

References edu.mit.csail.sdg.squander.spec.ForgeScene.getEnv(), edu.mit.csail.sdg.squander.spec.JMethod.spec, edu.mit.csail.sdg.squander.spec.ForgeScene.thisVar, and edu.mit.csail.sdg.squander.spec.MethodSpec.translateSpecs().

Referenced by edu.mit.csail.sdg.squander.engine.ForgeConverter.finish().

Member Data Documentation

Object edu.mit.csail.sdg.squander.spec.JavaScene.caller [private]

Definition at line 31 of file JavaScene.java.

Referenced by edu.mit.csail.sdg.squander.engine.ForgeConverter.boundOtherStuff().

Map<JType.Unary, ClassSpec> edu.mit.csail.sdg.squander.spec.JavaScene.classes = new HashMap<JType.Unary, ClassSpec>() [private]

Definition at line 27 of file JavaScene.java.

boolean edu.mit.csail.sdg.squander.spec.JavaScene.finished = false [private]

Definition at line 34 of file JavaScene.java.

JMethod edu.mit.csail.sdg.squander.spec.JavaScene.method [private]

Definition at line 30 of file JavaScene.java.

Referenced by edu.mit.csail.sdg.squander.engine.ForgeConverter.finish(), edu.mit.csail.sdg.squander.engine.SquanderResult.getReturnValue(), and edu.mit.csail.sdg.squander.engine.ForgeConverter.proc().

Object [] edu.mit.csail.sdg.squander.spec.JavaScene.methodArgs = new Object[0] [private]

Definition at line 32 of file JavaScene.java.

Referenced by edu.mit.csail.sdg.squander.engine.ForgeConverter.boundOtherStuff().

Map<Object, ClassSpec> edu.mit.csail.sdg.squander.spec.JavaScene.obj2spec = new IdentityHashMap<Object, ClassSpec>() [private]

Definition at line 28 of file JavaScene.java.

The documentation for this class was generated from the following file:
Generated by  doxygen 1.6.2-20100208