edu.mit.csail.sdg.squander.spec.ForgeScene Class Reference
[Specification]
Classes | |
| class | ArrayVars |
| class | MyEnv |
Public Member Functions | |
| ForgeScene (JavaScene javaScene) | |
| void | createLocalsForMethod (JMethod m) |
| LocalVariable | newThisVariable (JType.Unary type) |
| ForgeEnv | getEnv (LocalVariable thisVar) |
| ForgeProgram | program () |
| LocalVariable | thisVar () |
| LocalVariable | returnVar () |
| LocalVariable | throwVar () |
| LocalVariable[] | args () |
| InstanceLiteral | nullLit () |
| InstanceDomain | nullType () |
| Set< InstanceDomain > | domains () |
| GlobalVariable | global (String name) |
| GlobalVariable | global (JField fld) |
| Collection< GlobalVariable > | consts () |
| boolean | isConst (GlobalVariable var) |
| ForgeVariable | findVar (String name) |
| Set< JField > | fields (GlobalVariable var) |
| boolean | isSpecField (GlobalVariable var) |
| boolean | isOneField (GlobalVariable var) |
| Collection<?extends GlobalVariable > | nonAbstractSpecFields () |
| boolean | isPureAbstractSpecField (GlobalVariable var) |
| ForgeDomain | findDomain (JType.Unary clz) |
| ForgeDomain | ensureDomain (JType.Unary clz) |
| JType.Unary | findClassForDomain (ForgeDomain dom) |
| void | ensureInt (int i) |
| Set< Integer > | ints () |
| boolean | isEnsureAllInts () |
| void | ensureAllInts (boolean b) |
| Collection< ForgeType > | numTypes () |
| Set< ForgeType.Unary > | usedTypes () |
| GlobalVariable | ensureGlobal (JField field) |
| GlobalVariable | ensureConst (String name) |
| InstanceLiteral | createLiteral (Object object) |
| int | numLiteralsFor (InstanceDomain id) |
| ForgeType.Unary | typeForCls (JType.Unary cls, boolean includeNull) |
| Object | objForLit (String litName) |
| ForgeLiteral | forgeLitForObj (Object obj) |
| InstanceLiteral | instLitForObj (Object obj) |
| InstanceLiteral | litForName (String name) |
Private Member Functions | |
| void | addUsedType (ForgeType.Unary t) |
| ForgeType | getRangeForField (JField field) |
| ForgeType | convertToForgeType (JType jtype, boolean includeNull) |
| GlobalVariable | createGlobalVar (JField field, String name) |
Private Attributes | |
| final Counter< JType.Unary > | counter = new Counter<JType.Unary>() |
| final Counter< InstanceDomain > | litCnt = new Counter<InstanceDomain>() |
| final JavaScene | javaScene |
| final ForgeProgram | program |
| final InstanceDomain | nullType |
| final InstanceLiteral | nullLit |
| final IdentityHashMap< Object, InstanceLiteral > | obj2lit = new IdentityHashMap<Object, InstanceLiteral>() |
| final HashMap< String, InstanceLiteral > | str2lit = new HashMap<String, InstanceLiteral>() |
| final Map< String, Object > | lit2obj = new HashMap<String, Object>() |
| final Map< JType.Unary, ForgeDomain > | cls2dom = new HashMap<JType.Unary, ForgeDomain>() |
| final Map< String, GlobalVariable > | globals = new HashMap<String, GlobalVariable>() |
| final Map< String, LocalVariable > | locals = new HashMap<String, LocalVariable>() |
| final Map< String, GlobalVariable > | consts = new HashMap<String, GlobalVariable>() |
| final Map< GlobalVariable, Set < JField > > | var2fld = new HashMap<GlobalVariable, Set<JField>>() |
| final Set< Integer > | ints = new HashSet<Integer>(64) |
| boolean | ensureAllInts = false |
| Map< String, ForgeType > | numTypes = new HashMap<String, ForgeType>() |
| Map< String, ForgeType.Unary > | usedTypes = new HashMap<String, ForgeType.Unary>() |
| LocalVariable | throwVar |
| LocalVariable | returnVar |
| LocalVariable | thisVar |
| LocalVariable[] | args = new LocalVariable[0] |
Detailed Description
Definition at line 35 of file ForgeScene.java.
Constructor & Destructor Documentation
| edu.mit.csail.sdg.squander.spec.ForgeScene.ForgeScene | ( | JavaScene | javaScene | ) |
Definition at line 96 of file ForgeScene.java.
References edu.mit.csail.sdg.squander.spec.ForgeScene.addUsedType(), edu.mit.csail.sdg.squander.spec.ForgeScene.cls2dom, edu.mit.csail.sdg.squander.spec.ForgeScene.lit2obj, edu.mit.csail.sdg.squander.spec.ForgeScene.litCnt, edu.mit.csail.sdg.squander.spec.ForgeScene.nullLit(), edu.mit.csail.sdg.squander.spec.ForgeScene.nullType(), and edu.mit.csail.sdg.squander.spec.ForgeScene.program().
Member Function Documentation
| void edu.mit.csail.sdg.squander.spec.ForgeScene.addUsedType | ( | ForgeType.Unary | t | ) | [private] |
Definition at line 354 of file ForgeScene.java.
References edu.mit.csail.sdg.squander.spec.ForgeScene.usedTypes().
Referenced by edu.mit.csail.sdg.squander.spec.ForgeScene.ensureDomain(), edu.mit.csail.sdg.squander.spec.ForgeScene.ForgeScene(), and edu.mit.csail.sdg.squander.spec.ForgeScene.typeForCls().
| LocalVariable [] edu.mit.csail.sdg.squander.spec.ForgeScene.args | ( | ) |
Definition at line 159 of file ForgeScene.java.
Referenced by edu.mit.csail.sdg.squander.spec.ForgeScene.MyEnv.arg(), edu.mit.csail.sdg.squander.spec.ForgeScene.createLocalsForMethod(), and edu.mit.csail.sdg.squander.spec.ForgeScene.getEnv().
| Collection<GlobalVariable> edu.mit.csail.sdg.squander.spec.ForgeScene.consts | ( | ) |
Definition at line 165 of file ForgeScene.java.
Referenced by edu.mit.csail.sdg.squander.spec.ForgeScene.ensureConst(), edu.mit.csail.sdg.squander.spec.ForgeScene.findVar(), and edu.mit.csail.sdg.squander.spec.ForgeScene.isConst().
| ForgeType edu.mit.csail.sdg.squander.spec.ForgeScene.convertToForgeType | ( | JType | jtype, | |
| boolean | includeNull | |||
| ) | [private] |
Definition at line 367 of file ForgeScene.java.
References edu.mit.csail.sdg.squander.spec.JType.arity(), edu.mit.csail.sdg.squander.spec.JType.domain(), edu.mit.csail.sdg.squander.spec.JType.projection(), and edu.mit.csail.sdg.squander.spec.ForgeScene.typeForCls().
Referenced by edu.mit.csail.sdg.squander.spec.ForgeScene.createGlobalVar(), edu.mit.csail.sdg.squander.spec.ForgeScene.ensureConst(), and edu.mit.csail.sdg.squander.spec.ForgeScene.getRangeForField().
| GlobalVariable edu.mit.csail.sdg.squander.spec.ForgeScene.createGlobalVar | ( | JField | field, | |
| String | name | |||
| ) | [private] |
Definition at line 375 of file ForgeScene.java.
References edu.mit.csail.sdg.squander.spec.ForgeScene.convertToForgeType(), edu.mit.csail.sdg.squander.spec.ForgeScene.getRangeForField(), edu.mit.csail.sdg.squander.spec.JField.owningType, and edu.mit.csail.sdg.squander.spec.ForgeScene.program().
Referenced by edu.mit.csail.sdg.squander.spec.ForgeScene.ensureGlobal().
| InstanceLiteral edu.mit.csail.sdg.squander.spec.ForgeScene.createLiteral | ( | Object | object | ) |
Definition at line 278 of file ForgeScene.java.
References edu.mit.csail.sdg.squander.spec.ForgeScene.counter, edu.mit.csail.sdg.squander.spec.ForgeScene.ensureDomain(), edu.mit.csail.sdg.squander.spec.ForgeScene.javaScene, edu.mit.csail.sdg.squander.spec.JavaScene.jtypeForObj(), edu.mit.csail.sdg.squander.spec.ForgeScene.lit2obj, edu.mit.csail.sdg.squander.spec.ForgeScene.litCnt, edu.mit.csail.sdg.squander.spec.ForgeScene.obj2lit, edu.mit.csail.sdg.squander.spec.ForgeScene.program(), and edu.mit.csail.sdg.squander.spec.ForgeScene.str2lit.
Referenced by edu.mit.csail.sdg.squander.engine.ForgeConverter.finish().
| void edu.mit.csail.sdg.squander.spec.ForgeScene.createLocalsForMethod | ( | JMethod | m | ) |
Definition at line 110 of file ForgeScene.java.
References edu.mit.csail.sdg.squander.spec.ForgeScene.args(), edu.mit.csail.sdg.squander.spec.JMethod.declaringClass, edu.mit.csail.sdg.squander.spec.JMethod.isStatic, edu.mit.csail.sdg.squander.spec.ForgeScene.locals, edu.mit.csail.sdg.squander.spec.JMethod.name(), edu.mit.csail.sdg.squander.spec.ForgeScene.newThisVariable(), edu.mit.csail.sdg.squander.spec.JMethod.params, edu.mit.csail.sdg.squander.spec.ForgeScene.program(), edu.mit.csail.sdg.squander.spec.JMethod.returnType, edu.mit.csail.sdg.squander.spec.ForgeScene.returnVar(), edu.mit.csail.sdg.squander.spec.ForgeScene.thisVar(), and edu.mit.csail.sdg.squander.spec.ForgeScene.typeForCls().
Referenced by edu.mit.csail.sdg.squander.engine.ForgeConverter.finish().
| Set<InstanceDomain> edu.mit.csail.sdg.squander.spec.ForgeScene.domains | ( | ) |
Definition at line 162 of file ForgeScene.java.
References edu.mit.csail.sdg.squander.spec.ForgeScene.program().
Referenced by edu.mit.csail.sdg.squander.engine.ForgeConverter.makeForgeBounds().
| void edu.mit.csail.sdg.squander.spec.ForgeScene.ensureAllInts | ( | boolean | b | ) |
Definition at line 246 of file ForgeScene.java.
References edu.mit.csail.sdg.squander.spec.ForgeScene.ensureAllInts.
| GlobalVariable edu.mit.csail.sdg.squander.spec.ForgeScene.ensureConst | ( | String | name | ) |
Definition at line 268 of file ForgeScene.java.
References edu.mit.csail.sdg.squander.spec.ForgeScene.consts(), edu.mit.csail.sdg.squander.spec.ForgeScene.convertToForgeType(), and edu.mit.csail.sdg.squander.spec.ForgeScene.program().
| ForgeDomain edu.mit.csail.sdg.squander.spec.ForgeScene.ensureDomain | ( | JType.Unary | clz | ) |
Definition at line 224 of file ForgeScene.java.
References edu.mit.csail.sdg.squander.spec.ForgeScene.addUsedType(), edu.mit.csail.sdg.squander.spec.ForgeScene.cls2dom, and edu.mit.csail.sdg.squander.spec.ForgeScene.program().
Referenced by edu.mit.csail.sdg.squander.spec.ForgeScene.createLiteral(), and edu.mit.csail.sdg.squander.spec.ForgeScene.typeForCls().
| GlobalVariable edu.mit.csail.sdg.squander.spec.ForgeScene.ensureGlobal | ( | JField | field | ) |
Definition at line 250 of file ForgeScene.java.
References edu.mit.csail.sdg.squander.spec.ForgeScene.createGlobalVar(), edu.mit.csail.sdg.squander.spec.ForgeScene.fields(), edu.mit.csail.sdg.squander.spec.JField.fullName(), edu.mit.csail.sdg.squander.spec.ForgeScene.global(), edu.mit.csail.sdg.squander.spec.ForgeScene.globals, edu.mit.csail.sdg.squander.spec.JField.isSpec(), and edu.mit.csail.sdg.squander.spec.ForgeScene.var2fld.
| void edu.mit.csail.sdg.squander.spec.ForgeScene.ensureInt | ( | int | i | ) |
Definition at line 242 of file ForgeScene.java.
References edu.mit.csail.sdg.squander.spec.ForgeScene.ints().
Referenced by edu.mit.csail.sdg.squander.engine.ForgeConverter.finish().
| Set<JField> edu.mit.csail.sdg.squander.spec.ForgeScene.fields | ( | GlobalVariable | var | ) |
Definition at line 176 of file ForgeScene.java.
References edu.mit.csail.sdg.squander.spec.ForgeScene.var2fld.
Referenced by edu.mit.csail.sdg.squander.spec.Frame.add(), edu.mit.csail.sdg.squander.spec.ForgeScene.ensureGlobal(), edu.mit.csail.sdg.squander.engine.SquanderResult.getJFieldForVar(), edu.mit.csail.sdg.squander.spec.ForgeScene.isOneField(), edu.mit.csail.sdg.squander.spec.ForgeScene.isPureAbstractSpecField(), edu.mit.csail.sdg.squander.spec.ForgeScene.isSpecField(), and edu.mit.csail.sdg.squander.spec.Frame.modifiable().
| JType.Unary edu.mit.csail.sdg.squander.spec.ForgeScene.findClassForDomain | ( | ForgeDomain | dom | ) |
Definition at line 234 of file ForgeScene.java.
References edu.mit.csail.sdg.squander.spec.ForgeScene.cls2dom.
Referenced by edu.mit.csail.sdg.squander.spec.ForgeScene.MyEnv.classForDomain().
| ForgeDomain edu.mit.csail.sdg.squander.spec.ForgeScene.findDomain | ( | JType.Unary | clz | ) |
Definition at line 222 of file ForgeScene.java.
References edu.mit.csail.sdg.squander.spec.ForgeScene.cls2dom.
Referenced by edu.mit.csail.sdg.squander.spec.ForgeScene.typeForCls().
| ForgeVariable edu.mit.csail.sdg.squander.spec.ForgeScene.findVar | ( | String | name | ) |
Definition at line 167 of file ForgeScene.java.
References edu.mit.csail.sdg.squander.spec.ForgeScene.consts(), edu.mit.csail.sdg.squander.spec.ForgeScene.global(), and edu.mit.csail.sdg.squander.spec.ForgeScene.locals.
Referenced by edu.mit.csail.sdg.squander.engine.ForgeConverter.makeForgeBounds().
| ForgeLiteral edu.mit.csail.sdg.squander.spec.ForgeScene.forgeLitForObj | ( | Object | obj | ) |
Definition at line 322 of file ForgeScene.java.
References edu.mit.csail.sdg.squander.spec.ForgeScene.instLitForObj(), and edu.mit.csail.sdg.squander.spec.ForgeScene.program().
Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.conv2tuples(), and edu.mit.csail.sdg.squander.engine.ForgeConverter.printObjSet().
| ForgeEnv edu.mit.csail.sdg.squander.spec.ForgeScene.getEnv | ( | LocalVariable | thisVar | ) |
Definition at line 147 of file ForgeScene.java.
References edu.mit.csail.sdg.squander.spec.ForgeScene.args(), and edu.mit.csail.sdg.squander.spec.ForgeScene.locals.
Referenced by edu.mit.csail.sdg.squander.spec.JavaScene.translateSpecs(), and edu.mit.csail.sdg.squander.spec.ClassSpec.translateSpecs().
| ForgeType edu.mit.csail.sdg.squander.spec.ForgeScene.getRangeForField | ( | JField | field | ) | [private] |
Definition at line 358 of file ForgeScene.java.
References edu.mit.csail.sdg.squander.spec.ForgeScene.convertToForgeType(), edu.mit.csail.sdg.squander.spec.JField.isSpec(), edu.mit.csail.sdg.squander.spec.JType.range(), edu.mit.csail.sdg.squander.spec.JField.type, and edu.mit.csail.sdg.squander.spec.ForgeScene.typeForCls().
Referenced by edu.mit.csail.sdg.squander.spec.ForgeScene.createGlobalVar().
| GlobalVariable edu.mit.csail.sdg.squander.spec.ForgeScene.global | ( | JField | fld | ) |
Definition at line 164 of file ForgeScene.java.
References edu.mit.csail.sdg.squander.spec.JField.fullName(), and edu.mit.csail.sdg.squander.spec.ForgeScene.globals.
| GlobalVariable edu.mit.csail.sdg.squander.spec.ForgeScene.global | ( | String | name | ) |
Definition at line 163 of file ForgeScene.java.
References edu.mit.csail.sdg.squander.spec.ForgeScene.globals.
Referenced by edu.mit.csail.sdg.squander.engine.ForgeConverter.boundSpecFields(), edu.mit.csail.sdg.squander.spec.Spec.concreteConstraint(), edu.mit.csail.sdg.squander.spec.ForgeScene.ensureGlobal(), edu.mit.csail.sdg.squander.spec.Spec.fieldConstraint(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.findMaxArrayLength(), edu.mit.csail.sdg.squander.spec.ForgeScene.findVar(), edu.mit.csail.sdg.squander.engine.SquanderResult.getReturnValue(), and edu.mit.csail.sdg.squander.engine.SquanderResult.getSpecField().
| InstanceLiteral edu.mit.csail.sdg.squander.spec.ForgeScene.instLitForObj | ( | Object | obj | ) |
Definition at line 335 of file ForgeScene.java.
References edu.mit.csail.sdg.squander.spec.ForgeScene.nullLit(), edu.mit.csail.sdg.squander.spec.ForgeScene.obj2lit, and edu.mit.csail.sdg.squander.spec.ForgeScene.str2lit.
Referenced by edu.mit.csail.sdg.squander.spec.ForgeScene.forgeLitForObj(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.getLitNameForObject(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.getModLits(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.getPostLower(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.getPostLower(), and edu.mit.csail.sdg.squander.engine.ForgeConverter.obj2atom().
| Set<Integer> edu.mit.csail.sdg.squander.spec.ForgeScene.ints | ( | ) |
returns only used ints
Definition at line 244 of file ForgeScene.java.
Referenced by edu.mit.csail.sdg.squander.spec.ForgeScene.ensureInt().
| boolean edu.mit.csail.sdg.squander.spec.ForgeScene.isConst | ( | GlobalVariable | var | ) |
Definition at line 166 of file ForgeScene.java.
References edu.mit.csail.sdg.squander.spec.ForgeScene.consts().
Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.createBounds(), and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.createRelations().
| boolean edu.mit.csail.sdg.squander.spec.ForgeScene.isEnsureAllInts | ( | ) |
Definition at line 245 of file ForgeScene.java.
References edu.mit.csail.sdg.squander.spec.ForgeScene.ensureAllInts.
Referenced by edu.mit.csail.sdg.squander.engine.ForgeConverter.allInts(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.createUniverse(), and edu.mit.csail.sdg.squander.engine.ForgeConverter.maxSize().
| boolean edu.mit.csail.sdg.squander.spec.ForgeScene.isOneField | ( | GlobalVariable | var | ) |
Definition at line 188 of file ForgeScene.java.
References edu.mit.csail.sdg.squander.spec.ForgeScene.fields(), edu.mit.csail.sdg.squander.spec.JField.getBound(), and edu.mit.csail.sdg.squander.spec.JField.isSpec().
Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.getExtent().
| boolean edu.mit.csail.sdg.squander.spec.ForgeScene.isPureAbstractSpecField | ( | GlobalVariable | var | ) |
Definition at line 211 of file ForgeScene.java.
References edu.mit.csail.sdg.squander.spec.ForgeScene.fields(), and edu.mit.csail.sdg.squander.spec.ForgeScene.program().
Referenced by edu.mit.csail.sdg.squander.spec.ForgeScene.nonAbstractSpecFields().
| boolean edu.mit.csail.sdg.squander.spec.ForgeScene.isSpecField | ( | GlobalVariable | var | ) |
Definition at line 180 of file ForgeScene.java.
References edu.mit.csail.sdg.squander.spec.ForgeScene.fields().
Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.createBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.createBounds(), edu.mit.csail.sdg.squander.spec.ForgeScene.nonAbstractSpecFields(), and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.wellformed().
| InstanceLiteral edu.mit.csail.sdg.squander.spec.ForgeScene.litForName | ( | String | name | ) |
Definition at line 343 of file ForgeScene.java.
References edu.mit.csail.sdg.squander.spec.ForgeScene.program().
| LocalVariable edu.mit.csail.sdg.squander.spec.ForgeScene.newThisVariable | ( | JType.Unary | type | ) |
Definition at line 141 of file ForgeScene.java.
References edu.mit.csail.sdg.squander.spec.ForgeScene.program(), and edu.mit.csail.sdg.squander.spec.ForgeScene.typeForCls().
Referenced by edu.mit.csail.sdg.squander.spec.ForgeScene.createLocalsForMethod(), and edu.mit.csail.sdg.squander.spec.ClassSpec.translateSpecs().
| Collection<? extends GlobalVariable> edu.mit.csail.sdg.squander.spec.ForgeScene.nonAbstractSpecFields | ( | ) |
Definition at line 202 of file ForgeScene.java.
References edu.mit.csail.sdg.squander.spec.ForgeScene.globals, edu.mit.csail.sdg.squander.spec.ForgeScene.isPureAbstractSpecField(), and edu.mit.csail.sdg.squander.spec.ForgeScene.isSpecField().
Referenced by edu.mit.csail.sdg.squander.spec.Frame.modifiable().
| InstanceLiteral edu.mit.csail.sdg.squander.spec.ForgeScene.nullLit | ( | ) |
Definition at line 160 of file ForgeScene.java.
Referenced by edu.mit.csail.sdg.squander.spec.ForgeScene.ForgeScene(), and edu.mit.csail.sdg.squander.spec.ForgeScene.instLitForObj().
| InstanceDomain edu.mit.csail.sdg.squander.spec.ForgeScene.nullType | ( | ) |
Definition at line 161 of file ForgeScene.java.
Referenced by edu.mit.csail.sdg.squander.spec.ForgeScene.ForgeScene(), and edu.mit.csail.sdg.squander.spec.ForgeScene.typeForCls().
| int edu.mit.csail.sdg.squander.spec.ForgeScene.numLiteralsFor | ( | InstanceDomain | id | ) |
Definition at line 292 of file ForgeScene.java.
References edu.mit.csail.sdg.squander.spec.ForgeScene.litCnt.
Referenced by edu.mit.csail.sdg.squander.engine.ForgeConverter.maxSize().
| Collection<ForgeType> edu.mit.csail.sdg.squander.spec.ForgeScene.numTypes | ( | ) |
Definition at line 247 of file ForgeScene.java.
Referenced by edu.mit.csail.sdg.squander.spec.ForgeScene.MyEnv.ensureNum().
| Object edu.mit.csail.sdg.squander.spec.ForgeScene.objForLit | ( | String | litName | ) |
Definition at line 318 of file ForgeScene.java.
References edu.mit.csail.sdg.squander.spec.ForgeScene.lit2obj.
Referenced by edu.mit.csail.sdg.squander.engine.ForgeConverter.atom2obj(), edu.mit.csail.sdg.squander.engine.ForgeConverter.lit2obj(), and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.KodkodEval.makeConst().
| ForgeProgram edu.mit.csail.sdg.squander.spec.ForgeScene.program | ( | ) |
Definition at line 155 of file ForgeScene.java.
Referenced by edu.mit.csail.sdg.squander.spec.ForgeScene.MyEnv.booleanType(), edu.mit.csail.sdg.squander.spec.ForgeScene.createGlobalVar(), edu.mit.csail.sdg.squander.spec.ForgeScene.createLiteral(), edu.mit.csail.sdg.squander.spec.ForgeScene.createLocalsForMethod(), edu.mit.csail.sdg.squander.spec.ForgeScene.domains(), edu.mit.csail.sdg.squander.spec.ForgeScene.MyEnv.emptyDecls(), edu.mit.csail.sdg.squander.spec.ForgeScene.ensureConst(), edu.mit.csail.sdg.squander.spec.ForgeScene.ensureDomain(), edu.mit.csail.sdg.squander.spec.ForgeScene.MyEnv.falseExpr(), edu.mit.csail.sdg.squander.spec.ForgeScene.forgeLitForObj(), edu.mit.csail.sdg.squander.spec.ForgeScene.ForgeScene(), edu.mit.csail.sdg.squander.spec.ForgeScene.MyEnv.getThrowVar(), edu.mit.csail.sdg.squander.spec.ForgeScene.MyEnv.integerType(), edu.mit.csail.sdg.squander.spec.ForgeScene.MyEnv.intExpr(), edu.mit.csail.sdg.squander.spec.ForgeScene.isPureAbstractSpecField(), edu.mit.csail.sdg.squander.spec.ForgeScene.litForName(), edu.mit.csail.sdg.squander.spec.ForgeScene.MyEnv.newLocalVar(), edu.mit.csail.sdg.squander.spec.ForgeScene.newThisVariable(), edu.mit.csail.sdg.squander.spec.ForgeScene.MyEnv.stringExpr(), edu.mit.csail.sdg.squander.spec.ForgeScene.MyEnv.trueExpr(), and edu.mit.csail.sdg.squander.spec.ForgeScene.typeForCls().
| LocalVariable edu.mit.csail.sdg.squander.spec.ForgeScene.returnVar | ( | ) |
Definition at line 157 of file ForgeScene.java.
Referenced by edu.mit.csail.sdg.squander.spec.ForgeScene.createLocalsForMethod().
| LocalVariable edu.mit.csail.sdg.squander.spec.ForgeScene.thisVar | ( | ) |
Definition at line 156 of file ForgeScene.java.
Referenced by edu.mit.csail.sdg.squander.spec.ForgeScene.createLocalsForMethod().
| LocalVariable edu.mit.csail.sdg.squander.spec.ForgeScene.throwVar | ( | ) |
Definition at line 158 of file ForgeScene.java.
| ForgeType.Unary edu.mit.csail.sdg.squander.spec.ForgeScene.typeForCls | ( | JType.Unary | cls, | |
| boolean | includeNull | |||
| ) |
Definition at line 297 of file ForgeScene.java.
References edu.mit.csail.sdg.squander.spec.ForgeScene.addUsedType(), edu.mit.csail.sdg.squander.spec.ForgeScene.ensureDomain(), edu.mit.csail.sdg.squander.spec.ForgeScene.findDomain(), edu.mit.csail.sdg.squander.spec.ForgeScene.javaScene, edu.mit.csail.sdg.squander.spec.ForgeScene.nullType(), edu.mit.csail.sdg.squander.spec.ForgeScene.program(), and edu.mit.csail.sdg.squander.spec.JavaScene.subTypes().
Referenced by edu.mit.csail.sdg.squander.spec.ForgeScene.convertToForgeType(), edu.mit.csail.sdg.squander.spec.ForgeScene.createLocalsForMethod(), edu.mit.csail.sdg.squander.spec.Spec.fieldConstraint(), edu.mit.csail.sdg.squander.spec.ForgeScene.getRangeForField(), edu.mit.csail.sdg.squander.spec.Spec.invariant(), and edu.mit.csail.sdg.squander.spec.ForgeScene.newThisVariable().
| Set<ForgeType.Unary> edu.mit.csail.sdg.squander.spec.ForgeScene.usedTypes | ( | ) |
Definition at line 248 of file ForgeScene.java.
Referenced by edu.mit.csail.sdg.squander.spec.ForgeScene.addUsedType().
Member Data Documentation
LocalVariable [] edu.mit.csail.sdg.squander.spec.ForgeScene.args = new LocalVariable[0] [private] |
Definition at line 94 of file ForgeScene.java.
Referenced by edu.mit.csail.sdg.squander.engine.ForgeConverter.boundOtherStuff(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.createBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.createBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.createBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.createBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.createRelations(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.createRelations(), edu.mit.csail.sdg.squander.engine.ForgeConverter.proc(), and edu.mit.csail.sdg.squander.spec.Spec.wellformedPre().
final Map<JType.Unary, ForgeDomain> edu.mit.csail.sdg.squander.spec.ForgeScene.cls2dom = new HashMap<JType.Unary, ForgeDomain>() [private] |
Maps Java classes to Forge domains.
Definition at line 69 of file ForgeScene.java.
Referenced by edu.mit.csail.sdg.squander.spec.ForgeScene.ensureDomain(), edu.mit.csail.sdg.squander.spec.ForgeScene.findClassForDomain(), edu.mit.csail.sdg.squander.spec.ForgeScene.findDomain(), and edu.mit.csail.sdg.squander.spec.ForgeScene.ForgeScene().
final Map<String, GlobalVariable> edu.mit.csail.sdg.squander.spec.ForgeScene.consts = new HashMap<String, GlobalVariable>() [private] |
Definition at line 76 of file ForgeScene.java.
Referenced by edu.mit.csail.sdg.squander.engine.ForgeConverter.boundOtherStuff(), and edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.createRelations().
final Counter<JType.Unary> edu.mit.csail.sdg.squander.spec.ForgeScene.counter = new Counter<JType.Unary>() [private] |
Definition at line 49 of file ForgeScene.java.
Referenced by edu.mit.csail.sdg.squander.spec.ForgeScene.createLiteral().
boolean edu.mit.csail.sdg.squander.spec.ForgeScene.ensureAllInts = false [private] |
whether all integers (within a bound) should be enumerated in Kodkod
Definition at line 84 of file ForgeScene.java.
Referenced by edu.mit.csail.sdg.squander.spec.ForgeScene.ensureAllInts(), edu.mit.csail.sdg.squander.engine.ForgeConverter.finish(), and edu.mit.csail.sdg.squander.spec.ForgeScene.isEnsureAllInts().
final Map<String, GlobalVariable> edu.mit.csail.sdg.squander.spec.ForgeScene.globals = new HashMap<String, GlobalVariable>() [private] |
Maps Java fields to Forge global variables.
Definition at line 72 of file ForgeScene.java.
Referenced by edu.mit.csail.sdg.squander.spec.ForgeScene.ensureGlobal(), edu.mit.csail.sdg.squander.spec.ForgeScene.global(), and edu.mit.csail.sdg.squander.spec.ForgeScene.nonAbstractSpecFields().
final Set<Integer> edu.mit.csail.sdg.squander.spec.ForgeScene.ints = new HashSet<Integer>(64) [private] |
List of all integers found on the heap
Definition at line 81 of file ForgeScene.java.
Referenced by edu.mit.csail.sdg.squander.engine.ForgeConverter.allInts(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.createUniverse(), and edu.mit.csail.sdg.squander.engine.ForgeConverter.maxSize().
final JavaScene edu.mit.csail.sdg.squander.spec.ForgeScene.javaScene [private] |
Definition at line 52 of file ForgeScene.java.
Referenced by edu.mit.csail.sdg.squander.spec.ForgeScene.MyEnv.arrayElems(), edu.mit.csail.sdg.squander.spec.ForgeScene.MyEnv.arrayLength(), edu.mit.csail.sdg.squander.spec.ForgeScene.createLiteral(), and edu.mit.csail.sdg.squander.spec.ForgeScene.typeForCls().
final Map<String, Object> edu.mit.csail.sdg.squander.spec.ForgeScene.lit2obj = new HashMap<String, Object>() [private] |
Keys are sometimes ForgeAtom and sometimes InstanceLiteral. We use Strings to abstract these to a common representation.
Definition at line 66 of file ForgeScene.java.
Referenced by edu.mit.csail.sdg.squander.spec.ForgeScene.createLiteral(), edu.mit.csail.sdg.squander.spec.ForgeScene.ForgeScene(), and edu.mit.csail.sdg.squander.spec.ForgeScene.objForLit().
final Counter<InstanceDomain> edu.mit.csail.sdg.squander.spec.ForgeScene.litCnt = new Counter<InstanceDomain>() [private] |
Definition at line 50 of file ForgeScene.java.
Referenced by edu.mit.csail.sdg.squander.spec.ForgeScene.createLiteral(), edu.mit.csail.sdg.squander.spec.ForgeScene.ForgeScene(), edu.mit.csail.sdg.squander.spec.ForgeScene.numLiteralsFor(), and edu.mit.csail.sdg.squander.spec.ForgeScene.MyEnv.stringExpr().
final Map<String, LocalVariable> edu.mit.csail.sdg.squander.spec.ForgeScene.locals = new HashMap<String, LocalVariable>() [private] |
Maps local variable names to local variables (e.g. thisVar, throwVar, returnVar, args)
Definition at line 74 of file ForgeScene.java.
Referenced by edu.mit.csail.sdg.squander.spec.ForgeScene.createLocalsForMethod(), edu.mit.csail.sdg.squander.spec.ForgeScene.findVar(), and edu.mit.csail.sdg.squander.spec.ForgeScene.getEnv().
final InstanceLiteral edu.mit.csail.sdg.squander.spec.ForgeScene.nullLit [private] |
Definition at line 55 of file ForgeScene.java.
Referenced by edu.mit.csail.sdg.squander.engine.ForgeConverter.obj2atom().
final InstanceDomain edu.mit.csail.sdg.squander.spec.ForgeScene.nullType [private] |
Definition at line 54 of file ForgeScene.java.
Map<String, ForgeType> edu.mit.csail.sdg.squander.spec.ForgeScene.numTypes = new HashMap<String, ForgeType>() [private] |
types whose cardinality is mentioned in the spec
Definition at line 87 of file ForgeScene.java.
Referenced by edu.mit.csail.sdg.squander.engine.ForgeConverter.finish().
final IdentityHashMap<Object, InstanceLiteral> edu.mit.csail.sdg.squander.spec.ForgeScene.obj2lit = new IdentityHashMap<Object, InstanceLiteral>() [private] |
Maps memory addresses to Forge InstanceLiterals.
Definition at line 58 of file ForgeScene.java.
Referenced by edu.mit.csail.sdg.squander.spec.ForgeScene.createLiteral(), and edu.mit.csail.sdg.squander.spec.ForgeScene.instLitForObj().
final ForgeProgram edu.mit.csail.sdg.squander.spec.ForgeScene.program [private] |
Definition at line 53 of file ForgeScene.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.Frame.condition(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.exeSpec(), edu.mit.csail.sdg.squander.spec.Spec.fieldConstraint(), edu.mit.csail.sdg.squander.engine.ForgeConverter.findInstLiteralsForType(), edu.mit.csail.sdg.squander.engine.ForgeConverter.findLiteralsForType(), edu.mit.csail.sdg.squander.spec.Spec.funcConstraint(), edu.mit.csail.sdg.squander.engine.SquanderImpl.getModsForPostState(), edu.mit.csail.sdg.squander.engine.SquanderImpl.getPostSpec(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.getPostSpec(), edu.mit.csail.sdg.squander.spec.Spec.invariant(), edu.mit.csail.sdg.squander.engine.ForgeConverter.makeForgeBounds(), edu.mit.csail.sdg.squander.spec.Frame.modCond(), edu.mit.csail.sdg.squander.engine.ForgeConverter.printUniverseStats(), edu.mit.csail.sdg.squander.engine.ForgeConverter.proc(), edu.mit.csail.sdg.squander.engine.SquanderResult.program(), edu.mit.csail.sdg.squander.spec.Spec.wellformedPost(), and edu.mit.csail.sdg.squander.spec.Spec.wellformedPre().
LocalVariable edu.mit.csail.sdg.squander.spec.ForgeScene.returnVar [private] |
Definition at line 92 of file ForgeScene.java.
Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.createBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.createBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.createBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.createBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.createRelations(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.createRelations(), edu.mit.csail.sdg.squander.engine.ForgeConverter.proc(), edu.mit.csail.sdg.squander.engine.SquanderResult.returnVar(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.wellformed(), and edu.mit.csail.sdg.squander.spec.Spec.wellformedPost().
final HashMap<String, InstanceLiteral> edu.mit.csail.sdg.squander.spec.ForgeScene.str2lit = new HashMap<String, InstanceLiteral>() [private] |
Maps string to Forge literals.
Definition at line 60 of file ForgeScene.java.
Referenced by edu.mit.csail.sdg.squander.spec.ForgeScene.createLiteral(), edu.mit.csail.sdg.squander.spec.ForgeScene.instLitForObj(), and edu.mit.csail.sdg.squander.spec.ForgeScene.MyEnv.stringExpr().
LocalVariable edu.mit.csail.sdg.squander.spec.ForgeScene.thisVar [private] |
Definition at line 93 of file ForgeScene.java.
Referenced by edu.mit.csail.sdg.squander.engine.ForgeConverter.boundOtherStuff(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.createBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPart2Impl.createBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.createBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.createBounds(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodImpl.createRelations(), edu.mit.csail.sdg.squander.engine.kk.SquanderKodkod2Impl.createRelations(), edu.mit.csail.sdg.squander.engine.ForgeConverter.proc(), edu.mit.csail.sdg.squander.engine.SquanderResult.self(), edu.mit.csail.sdg.squander.spec.JavaScene.translateSpecs(), and edu.mit.csail.sdg.squander.spec.Spec.wellformedPre().
LocalVariable edu.mit.csail.sdg.squander.spec.ForgeScene.throwVar [private] |
Definition at line 91 of file ForgeScene.java.
Referenced by edu.mit.csail.sdg.squander.spec.Spec.wellformedPost().
Map<String, ForgeType.Unary> edu.mit.csail.sdg.squander.spec.ForgeScene.usedTypes = new HashMap<String, ForgeType.Unary>() [private] |
Definition at line 89 of file ForgeScene.java.
Referenced by edu.mit.csail.sdg.squander.engine.kk.SquanderKodkodPartImpl.partitionDomains().
final Map<GlobalVariable, Set<JField> > edu.mit.csail.sdg.squander.spec.ForgeScene.var2fld = new HashMap<GlobalVariable, Set<JField>>() [private] |
Definition at line 78 of file ForgeScene.java.
Referenced by edu.mit.csail.sdg.squander.spec.ForgeScene.ensureGlobal(), and edu.mit.csail.sdg.squander.spec.ForgeScene.fields().
The documentation for this class was generated from the following file:
- src/edu/mit/csail/sdg/squander/spec/ForgeScene.java
