00001 00005 package edu.mit.csail.sdg.squander.spec; 00006 00007 import java.util.HashSet; 00008 import java.util.Set; 00009 00010 import forge.program.BinaryExpression; 00011 import forge.program.ConditionalExpression; 00012 import forge.program.ExpressionVisitor; 00013 import forge.program.ForgeLiteral; 00014 import forge.program.ForgeType; 00015 import forge.program.ForgeVariable; 00016 import forge.program.GlobalVariable; 00017 import forge.program.OldExpression; 00018 import forge.program.ProjectionExpression; 00019 import forge.program.QuantifyExpression; 00020 import forge.program.UnaryExpression; 00021 00022 public class FrameInference extends ExpressionVisitor<Void> { 00023 00024 private Set<GlobalVariable> globals = new HashSet<GlobalVariable>(); 00025 00026 public Set<GlobalVariable> globals() { return this.globals; } 00027 00028 @Override 00029 protected Void visit(ForgeType expr) { 00030 return null; 00031 } 00032 00033 @Override 00034 protected Void visit(ForgeLiteral expr) { 00035 return null; 00036 } 00037 00038 @Override 00039 protected Void visit(ForgeVariable expr) { 00040 if (expr.isGlobal()) 00041 globals.add((GlobalVariable) expr); 00042 return null; 00043 } 00044 00045 @Override 00046 protected Void visit(UnaryExpression expr) { 00047 expr.sub().accept(this); 00048 return null; 00049 } 00050 00051 @Override 00052 protected Void visit(BinaryExpression expr) { 00053 expr.left().accept(this); 00054 expr.right().accept(this); 00055 return null; 00056 } 00057 00058 @Override 00059 protected Void visit(ConditionalExpression expr) { 00060 expr.condition().accept(this); 00061 expr.thenExpr().accept(this); 00062 expr.elseExpr().accept(this); 00063 return null; 00064 } 00065 00066 @Override 00067 protected Void visit(ProjectionExpression expr) { 00068 expr.sub().accept(this); 00069 return null; 00070 } 00071 00072 @Override 00073 protected Void visit(QuantifyExpression expr) { 00074 expr.sub().accept(this); 00075 return null; 00076 } 00077 00078 @Override 00079 protected Void visit(OldExpression expr) { 00080 expr.variable().accept(this); 00081 return null; 00082 } 00083 00084 }