00001 package edu.ksu.cis.bandera.specification;
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023
00024
00025
00026
00027
00028
00029
00030
00031
00032
00033
00034
00035 import ca.mcgill.sable.soot.*;
00036 import ca.mcgill.sable.soot.jimple.*;
00037 import ca.mcgill.sable.soot.grimp.*;
00038 import edu.ksu.cis.bandera.jext.*;
00039 import edu.ksu.cis.bandera.jjjc.*;
00040 import edu.ksu.cis.bandera.specification.datastructure.*;
00041 public class QuantifiedVariableFixer extends AbstractBanderaValueSwitch {
00042 private static Grimp grimp = Grimp.v();
00043 private static QuantifiedVariableFixer qvf = new QuantifiedVariableFixer();
00044 private QuantifiedVariable qv;
00045
00046
00047
00048
00049 public void caseComplementExpr(ComplementExpr expr) {
00050 expr.getOp().apply(this);
00051 setResult(new ComplementExpr((Value) getResult()));
00052 }
00053 public void caseEqExpr(EqExpr v) {
00054 setResult(grimp.newEqExpr(grimp.newStaticFieldRef(CompilationManager.getFieldForQuantifier("quantification$" + qv.getName())), grimp.newStaticFieldRef(CompilationManager.getFieldForQuantifier(((Local) v.getOp2()).getName()))));
00055 }
00056 public void caseInstanceOfExpr(InstanceOfExpr v) {
00057 setResult(grimp.newInstanceOfExpr(grimp.newStaticFieldRef(CompilationManager.getFieldForQuantifier("quantification$" + qv.getName())), v.getCheckType()));
00058 }
00059
00060
00061
00062
00063 public void caseLogicalAndExpr(LogicalAndExpr expr) {
00064 expr.getOp1().apply(this);
00065 Value lValue = (Value) getResult();
00066 expr.getOp2().apply(this);
00067 Value rValue = (Value) getResult();
00068 setResult(new LogicalAndExpr(lValue, rValue));
00069 }
00070
00071
00072
00073
00074 public void caseLogicalOrExpr(LogicalOrExpr expr) {
00075 expr.getOp1().apply(this);
00076 Value lValue = (Value) getResult();
00077 expr.getOp2().apply(this);
00078 Value rValue = (Value) getResult();
00079 setResult(new LogicalOrExpr(lValue, rValue));
00080 }
00081
00082
00083
00084
00085 public void defaultCase(Object v) {
00086 throw new RuntimeException("Unexpected value: " + v);
00087 }
00088
00089
00090
00091
00092
00093 public static Value fix(QuantifiedVariable qv) {
00094 qvf.qv = qv;
00095 qv.getConstraint().apply(qvf);
00096 qvf.qv = null;
00097 Value result = (Value) qvf.getResult();
00098 qvf.setResult(null);
00099 return result;
00100 }
00101 }