00001
00005 package edu.mit.csail.sdg.squander.spec;
00006
00007 import static edu.mit.csail.sdg.squander.parser.JFSLParser.DECL_NONE;
00008 import static edu.mit.csail.sdg.squander.parser.JFSLParser.DECL_SEQ;
00009 import static edu.mit.csail.sdg.squander.parser.JFSLParser.FRAME_ALL;
00010 import static edu.mit.csail.sdg.squander.parser.JFSLParser.OP_AND;
00011 import static edu.mit.csail.sdg.squander.parser.JFSLParser.OP_BIT_AND_OR_INTERSECTION;
00012 import static edu.mit.csail.sdg.squander.parser.JFSLParser.OP_BIT_NOT_OR_TRANSPOSE;
00013 import static edu.mit.csail.sdg.squander.parser.JFSLParser.OP_BIT_OR;
00014 import static edu.mit.csail.sdg.squander.parser.JFSLParser.OP_BIT_XOR;
00015 import static edu.mit.csail.sdg.squander.parser.JFSLParser.OP_CLOSURE;
00016 import static edu.mit.csail.sdg.squander.parser.JFSLParser.OP_DIFFERENCE;
00017 import static edu.mit.csail.sdg.squander.parser.JFSLParser.OP_DIVIDE;
00018 import static edu.mit.csail.sdg.squander.parser.JFSLParser.OP_EQ;
00019 import static edu.mit.csail.sdg.squander.parser.JFSLParser.OP_EQUIV;
00020 import static edu.mit.csail.sdg.squander.parser.JFSLParser.OP_GEQ;
00021 import static edu.mit.csail.sdg.squander.parser.JFSLParser.OP_GT;
00022 import static edu.mit.csail.sdg.squander.parser.JFSLParser.OP_IMPLIES;
00023 import static edu.mit.csail.sdg.squander.parser.JFSLParser.OP_INTERSECTION;
00024 import static edu.mit.csail.sdg.squander.parser.JFSLParser.OP_LEQ;
00025 import static edu.mit.csail.sdg.squander.parser.JFSLParser.OP_LT;
00026 import static edu.mit.csail.sdg.squander.parser.JFSLParser.OP_MINUS;
00027 import static edu.mit.csail.sdg.squander.parser.JFSLParser.OP_MINUS_OR_DIFFERENCE;
00028 import static edu.mit.csail.sdg.squander.parser.JFSLParser.OP_MOD;
00029 import static edu.mit.csail.sdg.squander.parser.JFSLParser.OP_NEQ;
00030 import static edu.mit.csail.sdg.squander.parser.JFSLParser.OP_NEQUIV;
00031 import static edu.mit.csail.sdg.squander.parser.JFSLParser.OP_NOT;
00032 import static edu.mit.csail.sdg.squander.parser.JFSLParser.OP_NSET_SUBSET;
00033 import static edu.mit.csail.sdg.squander.parser.JFSLParser.OP_OR;
00034 import static edu.mit.csail.sdg.squander.parser.JFSLParser.OP_PLUS;
00035 import static edu.mit.csail.sdg.squander.parser.JFSLParser.OP_PLUS_OR_UNION;
00036 import static edu.mit.csail.sdg.squander.parser.JFSLParser.OP_RELATIONAL_COMPOSE;
00037 import static edu.mit.csail.sdg.squander.parser.JFSLParser.OP_RELATIONAL_OVERRIDE;
00038 import static edu.mit.csail.sdg.squander.parser.JFSLParser.OP_SET_ALL;
00039 import static edu.mit.csail.sdg.squander.parser.JFSLParser.OP_SET_COMPREHENSION;
00040 import static edu.mit.csail.sdg.squander.parser.JFSLParser.OP_SET_EXISTS;
00041 import static edu.mit.csail.sdg.squander.parser.JFSLParser.OP_SET_LONE;
00042 import static edu.mit.csail.sdg.squander.parser.JFSLParser.OP_SET_NO;
00043 import static edu.mit.csail.sdg.squander.parser.JFSLParser.OP_SET_NUM;
00044 import static edu.mit.csail.sdg.squander.parser.JFSLParser.OP_SET_ONE;
00045 import static edu.mit.csail.sdg.squander.parser.JFSLParser.OP_SET_SOME;
00046 import static edu.mit.csail.sdg.squander.parser.JFSLParser.OP_SET_SUBSET;
00047 import static edu.mit.csail.sdg.squander.parser.JFSLParser.OP_SET_SUM;
00048 import static edu.mit.csail.sdg.squander.parser.JFSLParser.OP_SHL;
00049 import static edu.mit.csail.sdg.squander.parser.JFSLParser.OP_SHR;
00050 import static edu.mit.csail.sdg.squander.parser.JFSLParser.OP_TIMES;
00051 import static edu.mit.csail.sdg.squander.parser.JFSLParser.OP_TRANSPOSE;
00052 import static edu.mit.csail.sdg.squander.parser.JFSLParser.OP_UNION;
00053 import static edu.mit.csail.sdg.squander.parser.JFSLParser.OP_USHR;
00054
00055
00056 import java.util.ArrayList;
00057 import java.util.IdentityHashMap;
00058 import java.util.List;
00059 import java.util.Map;
00060
00061 import edu.mit.csail.sdg.squander.parser.JFSLParser.Decision;
00062 import edu.mit.csail.sdg.squander.parser.JFSLParser.Node;
00063 import forge.program.ForgeDomain;
00064 import forge.program.ForgeExpression;
00065 import forge.program.ForgeType;
00066 import forge.program.GlobalVariable;
00067 import forge.program.IntegerLiteral;
00068 import forge.program.LocalDecls;
00069 import forge.program.LocalVariable;
00070 import forge.program.ForgeType.Tuple;
00071
00072 public class Tr extends Visitor<ForgeExpression, ForgeEnv> {
00073
00074 public static Map<LocalDecls, List<String>> absolutelyTerribleHack = new IdentityHashMap<LocalDecls, List<String>>();
00075
00076 Tr() { }
00077
00078 @Override
00079 protected ForgeExpression visitBinary(ForgeEnv env, Node tree, int op, Node leftTree, Node rightTree) {
00080 final ForgeExpression result;
00081 @SuppressWarnings("unused")
00082 boolean singleton = true;
00083
00084 final ForgeExpression left = visit(env, leftTree);
00085 final ForgeExpression right = visit(env, rightTree);
00086
00087
00088 switch (op) {
00089 case OP_SHL: result = left.shiftLeft(right); env.ensureAllInts(); break;
00090 case OP_SHR: result = left.shiftRight(right); env.ensureAllInts(); break;
00091 case OP_USHR: result = left.unsignedShiftRight(right); env.ensureAllInts(); break;
00092 case OP_PLUS: result = left.plus(right); env.ensureAllInts(); break;
00093 case OP_MINUS: result = left.minus(right); env.ensureAllInts(); break;
00094 case OP_TIMES: result = left.times(right); env.ensureAllInts(); break;
00095 case OP_DIVIDE: result = left.divide(right); env.ensureAllInts(); break;
00096 case OP_MOD: result = left.modulo(right); env.ensureAllInts(); break;
00097 case OP_BIT_XOR: result = left.bitXor(right); env.ensureAllInts(); break;
00098 case OP_BIT_OR: result = left.bitOr(right); env.ensureAllInts(); break;
00099
00100 case OP_LT: result = left.lt(right); break;
00101 case OP_GT: result = left.gt(right); break;
00102 case OP_LEQ: result = left.lte(right); break;
00103 case OP_GEQ: result = left.gte(right); break;
00104
00105 case OP_OR: result = left.or(right); break;
00106 case OP_AND: result = left.and(right); break;
00107 case OP_EQUIV: result = left.iff(right); break;
00108 case OP_NEQUIV: result = (left.iff(right)).not(); break;
00109 case OP_IMPLIES: result = left.implies(right); break;
00110
00111 case OP_EQ: result = left.eq(right); break;
00112 case OP_NEQ: result = (left.eq(right)).not(); break;
00113 case OP_SET_SUBSET: result = left.in(right); break;
00114 case OP_NSET_SUBSET: result = (left.in(right)).not(); break;
00115
00116 case OP_RELATIONAL_OVERRIDE:
00117 result = left.override(right);
00118 singleton = false;
00119 break;
00120 case OP_RELATIONAL_COMPOSE:
00121 result = left.product(right);
00122 singleton = false;
00123 break;
00124
00125 case OP_INTERSECTION:
00126 result = left.intersection(right);
00127 singleton = false;
00128 break;
00129 case OP_UNION:
00130 result = left.union(right);
00131 singleton = false;
00132 break;
00133 case OP_DIFFERENCE:
00134 result = left.difference(right);
00135 singleton = false;
00136 break;
00137
00138 case OP_PLUS_OR_UNION:
00139 if (tree.flag()) {
00140 env.ensureAllInts();
00141 result = left.plus(right);
00142 } else {
00143 result = left.union(right);
00144 singleton = false;
00145 }
00146 break;
00147 case OP_MINUS_OR_DIFFERENCE:
00148 if (tree.flag())
00149 result = left.minus(right);
00150 else {
00151 result = left.difference(right);
00152 singleton = false;
00153 }
00154 break;
00155 case OP_BIT_AND_OR_INTERSECTION:
00156 if (tree.flag())
00157 result = left.bitAnd(right);
00158 else {
00159 result = left.intersection(right);
00160 singleton = false;
00161 }
00162 break;
00163 default:
00164 assert false;
00165 result = null;
00166 }
00167
00168 return result;
00169 }
00170
00171 @Override
00172 protected ForgeExpression visitConditional(ForgeEnv env, Node condTree, Node leftTree, Node rightTree) {
00173 ForgeExpression cond = visit(env, condTree);
00174 ForgeExpression left = visit(env, leftTree);
00175 ForgeExpression right = visit(env, rightTree);
00176 return cond.thenElse(left, right);
00177 }
00178
00179 @Override
00180 protected ForgeExpression visitDecimal(ForgeEnv env, int i) {
00181 return env.intExpr(i);
00182 }
00183
00184 @Override
00185 protected ForgeExpression visitString(ForgeEnv env, String text) {
00186 return env.stringExpr(text);
00187 }
00188
00189 @Override
00190 protected ForgeExpression visitTrue(ForgeEnv env) {
00191 return env.trueExpr();
00192 }
00193
00194 @Override
00195 protected ForgeExpression visitFalse(ForgeEnv env) {
00196 return env.falseExpr();
00197 }
00198
00199 @Override
00200 protected ForgeExpression visitNull(ForgeEnv env) {
00201 return env.nullType();
00202 }
00203
00204 @Override
00205 protected ForgeExpression visitReturn(ForgeEnv env) {
00206 return env.returnVar();
00207 }
00208
00209 @Override
00210 protected ForgeExpression visitThrow(ForgeEnv env) {
00211 return env.throwVar();
00212 }
00213
00214 @Override
00215 protected ForgeExpression visitThis(ForgeEnv env) {
00216 return env.thisVar();
00217 }
00218
00219 @Override
00220 protected ForgeExpression visitSuper(ForgeEnv env) {
00221 return null;
00222 }
00223
00224 @Override
00225 protected ForgeExpression visitArgument(ForgeEnv env, int i) {
00226 return env.arg(i);
00227 }
00228
00229 @Override
00230 protected ForgeExpression visitOld(ForgeEnv env, Node sub) {
00231 return visit(env.setPreStateMode(), sub);
00232 }
00233
00234 @Override
00235 protected ForgeExpression visitQuantification(ForgeEnv env, int op, List<String> names, List<String> mults, List<Node> sets, Node expr) {
00236
00237 LocalDecls decl = env.emptyDecls();
00238 List<LocalVariable> vars = new ArrayList<LocalVariable>();
00239 List<ForgeExpression> domains = new ArrayList<ForgeExpression>();
00240 for (int i = 0; i < names.size(); i++) {
00241 ForgeExpression set = visit(env, sets.get(i));
00242 LocalVariable var = env.newLocalVar(names.get(i), set.type());
00243 env = env.addLocal(var);
00244
00245 vars.add(var);
00246 domains.add(set);
00247 decl = decl.and(var);
00248 }
00249
00250 absolutelyTerribleHack.put(decl, mults);
00251
00252
00253 ForgeExpression sub = visit(env, expr);
00254
00255
00256 ForgeExpression condition = env.trueExpr();
00257 boolean implies = false;
00258 for (int i = 0; i < names.size(); i++) {
00259 ForgeExpression dom = domains.get(i);
00260 condition = condition.and(vars.get(i).in(dom));
00261 if (!(dom instanceof ForgeDomain))
00262 implies = true;
00263 }
00264
00265 final ForgeExpression result;
00266
00267
00268 switch (op) {
00269 case OP_SET_ALL:
00270 if (implies)
00271 result = condition.implies(sub).forAll(decl);
00272 else
00273 result = sub.forAll(decl);
00274 break;
00275 case OP_SET_SOME:
00276 case OP_SET_EXISTS:
00277 if (implies)
00278 result = condition.and(sub).forSome(decl);
00279 else
00280 result = sub.forSome(decl);
00281 break;
00282 case OP_SET_COMPREHENSION:
00283 if (implies)
00284 result = condition.and(sub).comprehension(decl);
00285 else
00286 result = sub.comprehension(decl);
00287 break;
00288 case OP_SET_ONE:
00289 if (implies)
00290 result = condition.and(sub).comprehension(decl).one();
00291 else
00292 result = sub.comprehension(decl).one();
00293 break;
00294 case OP_SET_LONE:
00295 if (implies)
00296 result = condition.and(sub).comprehension(decl).lone();
00297 else
00298 result = sub.comprehension(decl).lone();
00299 break;
00300 case OP_SET_NO:
00301 if (implies)
00302 result = condition.and(sub).comprehension(decl).no();
00303 else
00304 result = sub.comprehension(decl).no();
00305 break;
00306 case OP_SET_NUM:
00307 if (implies)
00308 result = condition.and(sub).comprehension(decl).size();
00309 else
00310 result = sub.comprehension(decl).size();
00311 break;
00312 case OP_SET_SUM:
00313 result = condition.thenElse(sub, env.intExpr(0)).summation(decl);
00314 break;
00315 default:
00316 result = null;
00317 }
00318
00319 return result;
00320 }
00321
00322 @Override
00323 protected ForgeExpression visitUnary(ForgeEnv env, Node tree, int op, Node expr) {
00324 final ForgeExpression sub = visit(env, expr);
00325
00326 final ForgeExpression result;
00327 @SuppressWarnings("unused")
00328 boolean singleton = true;
00329
00330 switch (op) {
00331 case OP_PLUS: result = sub; break;
00332 case OP_MINUS:
00333 result = sub.neg();
00334 if (sub instanceof IntegerLiteral)
00335 env.ensureInt(-((IntegerLiteral) sub).value());
00336 break;
00337 case OP_NOT: result = sub.not(); break;
00338
00339 case OP_SET_SOME: result = sub.some(); break;
00340 case OP_SET_NO: result = sub.no(); break;
00341 case OP_SET_SUM: result = sub.sum(); break;
00342 case OP_SET_ONE: result = sub.one(); break;
00343 case OP_SET_LONE: result = sub.lone(); break;
00344 case OP_SET_NUM: result = sub.size(); env.ensureNum(sub.type()); break;
00345
00346 case OP_CLOSURE: result = sub.closure(); break;
00347 case OP_TRANSPOSE: result = sub.projection(reverse(sub.arity())); break;
00348 case OP_BIT_NOT_OR_TRANSPOSE:
00349 if (tree.flag())
00350 result = sub.bitNot();
00351 else
00352 result = sub.projection(reverse(sub.arity()));
00353 break;
00354 default:
00355 assert false;
00356 result = null;
00357 }
00358
00359 return result;
00360 }
00361
00362 private int[] reverse(int i) {
00363 int[] columns = new int[i];
00364 for (int j = 0; j < i; j++)
00365 columns[j] = i - 1 - j;
00366 return columns;
00367 }
00368
00369 @Override
00370 protected ForgeExpression visitName(ForgeEnv env, Node ident) {
00371 if (ident == null) {
00372 throw new NullPointerException("ident is null " + env);
00373 }
00374 if (ident.decision() == null) {
00375 throw new NullPointerException("ident.decision() == null for " + ident.toStringTree());
00376 }
00377 String name = asText(ident);
00378 switch (ident.decision()) {
00379 case LOCAL:
00380 LocalVariable local = env.findLocal(name);
00381 assert local != null : "Local variable " + name + " not found";
00382 return local;
00383 case GLOBAL:
00384 GlobalVariable global = env.ensureGlobal(ident.field);
00385 assert global != null : "Global variable " + name + " not found";
00386 return env.globalVar(global);
00387 case TYPE:
00388 assert ident.jtype != null;
00389 assert ident.jtype.arity() == 1;
00390 ForgeType.Unary domain = env.typeForCls(ident.jtype.domain(), false);
00391 assert domain != null : "domain " + name + " not found";
00392 return domain;
00393 case CONST:
00394 GlobalVariable globalConst = env.ensureConst(name);
00395 assert globalConst != null : "Global constant " + name + " not found";
00396 return globalConst;
00397 default:
00398 return null;
00399 }
00400 }
00401
00402 @Override
00403 protected ForgeExpression visitAmbiguous(ForgeEnv env, List<Node> idents) {
00404 ForgeExpression primary = visitName(env, idents.get(0));
00405
00406 for (int i = 1; i < idents.size(); i++)
00407 if (idents.get(i).decision() != Decision.FRAGMENT) {
00408 ForgeExpression selector = visitAmbiguous(env, idents.subList(i, idents.size()));
00409 return primary.join(selector);
00410 }
00411
00412 return primary;
00413 }
00414
00415 @Override
00416 protected ForgeExpression visitBracket(ForgeEnv env, ForgeExpression primary, Node tree) {
00417 ForgeExpression expr = visit(env, child(tree));
00418
00419 if (tree.flag()) {
00420 ForgeExpression elems = null;
00421 for (Tuple t : primary.type().tupleTypes()) {
00422 JType.Unary cls = env.classForDomain(t.domain());
00423 if (cls != null) {
00424 ForgeExpression el = env.arrayElems(cls);
00425 if (elems == null)
00426 elems = el;
00427 else
00428 elems = elems.union(el);
00429 }
00430 }
00431 assert elems != null : "elems relation not found for " + primary.type();
00432 return expr.join(primary.join(elems));
00433 } else
00434 return expr.join(primary);
00435 }
00436
00437 @Override
00438 protected ForgeExpression visitJoin(ForgeEnv env, ForgeExpression primary, Node tree) {
00439 return primary.join(visit(env, child(tree)));
00440 }
00441
00442 @Override
00443 protected ForgeExpression visitJoinReflexive(ForgeEnv env, ForgeExpression primary, Node tree) {
00444 return primary.union(primary.join(visit(env, child(tree)).closure()));
00445 }
00446
00447 @Override
00448 protected ForgeExpression visitMethodCall(ForgeEnv env, ForgeExpression receiver, String id, Node arguments) {
00449 throw new RuntimeException("method calls not supported");
00450 }
00451
00453 @Override
00454 protected ForgeExpression visitFieldDeclaration(ForgeEnv env, Node ident, int op, Node set, Node frame, Node constraint) {
00455 final ForgeExpression domain = visit(env, set);
00456 return (op == DECL_SEQ ? env.integerType().product(domain) : domain);
00457 }
00458
00459 @Override
00460 protected ForgeExpression visitCastExpression(ForgeEnv env, Node type, Node sub) {
00461 return visit(env, sub).intersection(visit(env, type));
00462 }
00463
00464 @Override
00465 protected ForgeExpression visitFieldRelation(ForgeEnv env, Node type, Node ident) {
00466 GlobalVariable global = env.ensureGlobal(ident.field);
00467 assert global != null : "global variable " + asText(ident) + " not found";
00468 return env.globalVar(global);
00469 }
00470
00471 @Override
00472 protected ForgeExpression visitArrayType(ForgeEnv env, Node base) {
00473 ForgeType.Unary type = env.ensureDomain(base.jtype.domain().mkArray());
00474 assert type != null : "type " + asText(base) + " not found";
00475 return type;
00476 }
00477
00478 @Override
00479 protected ForgeExpression visitBooleanType(ForgeEnv env) {
00480 return env.booleanType();
00481 }
00482
00483 @Override
00484 protected ForgeExpression visitIntegralType(ForgeEnv env) {
00485 return env.integerType();
00486 }
00487
00488 @Override
00489 protected ForgeExpression visitRefType(ForgeEnv env, Node source, List<Node> idents) {
00490 ForgeType.Unary type = env.ensureDomain(source.jtype.domain());
00491 assert type != null : "type " + asText(source) + " not found";
00492 return type;
00493 }
00494
00495 @Override
00496 protected ForgeExpression visitFrame(ForgeEnv env, List<ForgeExpression> locations,
00497 List<Node> fields, List<ForgeExpression> selectors, List<ForgeExpression> lowers,
00498 List<ForgeExpression> uppers) {
00499
00500 return env.trueExpr();
00501 }
00502
00503
00504
00505
00506
00510 public static class SpecFieldTranslator extends Tr {
00511
00512 public SpecFieldTranslator() { }
00513
00514 @Override
00515 protected ForgeExpression visitFieldDeclaration(ForgeEnv env, Node ident, int op, Node set, Node frame, Node constraint) {
00516 return constraint != null ? visit(env, constraint) : env.trueExpr();
00517 }
00518 }
00519
00520
00521
00522
00523
00527 public static class SpecFieldBoundTranslator extends Tr {
00528
00529 private final JField field;
00530
00531 public SpecFieldBoundTranslator(JField field) {
00532 this.field = field;
00533 }
00534
00535 @Override
00536 protected ForgeExpression visitFieldDeclaration(ForgeEnv env, Node ident, int op, Node set, Node frame, Node constraint) {
00537 LocalVariable x = env.thisVar();
00538 GlobalVariable var = env.ensureGlobal(field);
00539 ForgeExpression upper = visit(env, set);
00540 ForgeExpression upperDeclared = x.join(var).in(op == DECL_SEQ ? env.integerType().product(upper) : upper);
00541 ForgeExpression domain = upper.equals(upper.type()) ? env.trueExpr() : upperDeclared;
00542
00543
00544 ForgeExpression multiplicity;
00545 switch (op) {
00546 case OP_SET_ONE:
00547 multiplicity = x.join(var).one();
00548 break;
00549 case OP_SET_SOME:
00550 multiplicity = x.join(var).some();
00551 break;
00552 case OP_SET_LONE:
00553 multiplicity = x.join(var).lone();
00554 break;
00555 case DECL_SEQ:
00556
00557 LocalVariable i = env.newLocalVar("i", env.integerType());
00558 ForgeExpression positive = i.lt(env.intExpr(0)).thenElse(i.join(x.join(var)).no(), i.join(x.join(var)).lone()).forAll(i);
00559
00560
00561 LocalVariable j = env.newLocalVar("j", env.integerType());
00562 LocalVariable k = env.newLocalVar("k", env.integerType());
00563 ForgeExpression continuous = (j.lt(k).and(j.gte(env.intExpr(0))).and(j.join(x.join(var)).no())).implies(k.join(x.join(var)).no()).forAll(j).forAll(k);
00564 multiplicity = positive.and(continuous);
00565 break;
00566 case DECL_NONE:
00567 multiplicity = var.arity() == 2 ? x.join(var).one() : env.trueExpr();
00568 break;
00569 default:
00570 multiplicity = env.trueExpr();
00571 }
00572
00573 return multiplicity.and(domain);
00574 }
00575 }
00576
00577
00578
00579
00580
00582 static final class FrameConstructor extends Tr {
00583 private final Frame frame;
00584 private final ForgeScene forgeScene;
00585
00586 public FrameConstructor(Frame frame, ForgeScene forgeScene) {
00587 this.frame = frame;
00588 this.forgeScene = forgeScene;
00589 }
00590
00591 @Override
00592 protected ForgeExpression visitFrame(ForgeEnv env, List<ForgeExpression> locations,
00593 List<Node> fields, List<ForgeExpression> selectors, List<ForgeExpression> lowers,
00594 List<ForgeExpression> uppers) {
00595 int size = locations.size();
00596
00597 for (int i = 0; i < size; i++) {
00598 Node node = fields.get(i);
00599 ForgeExpression loc = locations.get(i);
00600 ForgeExpression sub = selectors.get(i);
00601 ForgeExpression lower = lowers.get(i);
00602 ForgeExpression upper = uppers.get(i);
00603 if (node.getType() == FRAME_ALL) {
00604
00605
00606
00607
00608 throw new RuntimeException("FRAME_ALL not supported");
00609 } else {
00610 switch (node.decision()) {
00611 case GLOBAL:
00612 GlobalVariable var = forgeScene.global(node.field);
00613 frame.add(var, loc, sub, lower, upper);
00614 break;
00615 }
00616 }
00617 }
00618
00619 return env.trueExpr();
00620 }
00621
00622 @Override
00623 protected ForgeExpression visitFieldDeclaration(ForgeEnv env, Node ident, int op, Node set, Node frame, Node constraint) {
00624 if (frame != null)
00625 visit(env, frame);
00626 return env.trueExpr();
00627 }
00628 }
00629 }