From 764cd110aa83468a8f57b2dd8980f71ebee0a7af Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Thu, 27 Oct 2011 14:47:38 -0700
Subject: Boogie: removed unreachable or unused code

---
 Source/AbsInt/AbstractInterpretation.cs | 10 +++----
 Source/AbsInt/ExprFactories.cs          | 47 ++-------------------------------
 2 files changed, 7 insertions(+), 50 deletions(-)

(limited to 'Source/AbsInt')

diff --git a/Source/AbsInt/AbstractInterpretation.cs b/Source/AbsInt/AbstractInterpretation.cs
index 698141bb..a5847594 100644
--- a/Source/AbsInt/AbstractInterpretation.cs
+++ b/Source/AbsInt/AbstractInterpretation.cs
@@ -686,7 +686,7 @@ namespace Microsoft.Boogie.AbstractInterpretation {
     static public AbstractAlgebra BuildIntervalsAbstractDomain() {
       Contract.Ensures(Contract.Result<AbstractAlgebra>() != null);
 
-      AI.IQuantPropExprFactory propfactory = new BoogiePropFactory();
+      AI.IPropExprFactory propfactory = new BoogiePropFactory();
       AI.ILinearExprFactory linearfactory = new BoogieLinearFactory();
       AI.IValueExprFactory valuefactory = new BoogieValueFactory();
       IComparer variableComparer = new VariableComparer();
@@ -709,7 +709,7 @@ namespace Microsoft.Boogie.AbstractInterpretation {
 
       AI.Lattice returnLattice;
 
-      AI.IQuantPropExprFactory propfactory = new BoogiePropFactory();
+      AI.IPropExprFactory propfactory = new BoogiePropFactory();
       AI.ILinearExprFactory linearfactory = new BoogieLinearFactory();
       AI.IIntExprFactory intfactory = new BoogieIntFactory();
       AI.IValueExprFactory valuefactory = new BoogieValueFactory();
@@ -772,7 +772,7 @@ namespace Microsoft.Boogie.AbstractInterpretation {
     [Peer]
     private AI.Lattice lattice;
     [Peer]
-    private AI.IQuantPropExprFactory propFactory;
+    private AI.IPropExprFactory propFactory;
     [Peer]
     private AI.ILinearExprFactory linearFactory;
     [Peer]
@@ -797,7 +797,7 @@ namespace Microsoft.Boogie.AbstractInterpretation {
       }
     }
 
-    public AI.IQuantPropExprFactory PropositionFactory {
+    public AI.IPropExprFactory PropositionFactory {
       get {
         return this.propFactory;
       }
@@ -835,7 +835,7 @@ namespace Microsoft.Boogie.AbstractInterpretation {
 
     [Captured]
     public AbstractAlgebra(AI.Lattice lattice,
-                          AI.IQuantPropExprFactory propFactory,
+                          AI.IPropExprFactory propFactory,
                           AI.ILinearExprFactory linearFactory,
                           AI.IIntExprFactory intFactory,
                           AI.IValueExprFactory valueFactory,
diff --git a/Source/AbsInt/ExprFactories.cs b/Source/AbsInt/ExprFactories.cs
index 34564cac..9b1ea0a0 100644
--- a/Source/AbsInt/ExprFactories.cs
+++ b/Source/AbsInt/ExprFactories.cs
@@ -10,7 +10,8 @@ using Microsoft.Basetypes;
 
 namespace Microsoft.Boogie.AbstractInterpretation {
 
-  public class BoogiePropFactory : BoogieFactory, AI.IQuantPropExprFactory {
+  public class BoogiePropFactory : BoogieFactory, AI.IPropExprFactory
+  {
     public AI.IFunApp False {
       get {
         Contract.Ensures(Contract.Result<AI.IFunApp>() != null);
@@ -61,17 +62,6 @@ namespace Microsoft.Boogie.AbstractInterpretation {
 
       return (AI.IFunApp)(new ExistsExpr(Token.NoToken, new VariableSeq((Variable)p.Param), IExpr2Expr(p.Body))).IExpr;
     }
-    public AI.IFunApp Exists(AI.AIType paramType, AI.FunctionBody bodygen) {
-      //Contract.Requires(bodygen != null);
-      Contract.Ensures(Contract.Result<AI.IFunApp>() != null);
-
-      // generate a fresh new variable
-      Variable var = FreshBoundVariable(paramType);
-      Contract.Assert(var != null);
-      Expr expr = IExpr2Expr(bodygen(var));
-      Contract.Assert(expr != null);
-      return (AI.IFunApp)(new ExistsExpr(Token.NoToken, new VariableSeq(var), expr)).IExpr;
-    }
 
     public AI.IFunApp Forall(AI.IFunction p) {
       //Contract.Requires(p != null);
@@ -79,39 +69,6 @@ namespace Microsoft.Boogie.AbstractInterpretation {
 
       return (AI.IFunApp)(new ForallExpr(Token.NoToken, new VariableSeq((Variable)p.Param), IExpr2Expr(p.Body))).IExpr;
     }
-    public AI.IFunApp Forall(AI.AIType paramType, AI.FunctionBody bodygen) {
-      //Contract.Requires(bodygen != null);
-      Contract.Ensures(Contract.Result<AI.IFunApp>() != null);
-
-      // generate a fresh new variable
-      Variable var = FreshBoundVariable(paramType);
-      Contract.Assert(var != null);
-      Expr expr = IExpr2Expr(bodygen(var));
-      Contract.Assert(expr != null);
-      return (AI.IFunApp)(new ForallExpr(Token.NoToken, new VariableSeq(var), expr)).IExpr;
-    }
-
-    private static int freshVarNum = 0;
-    private static Variable FreshBoundVariable(AI.AIType paramType) {
-      Contract.Ensures(Contract.Result<Variable>() != null);
-
-      // TODO: Should use the AI.AIType given in Exists and Forall to determine what Boogie type
-      // to make this new variable?  For now, we use Type.Any.
-      Type t = Type.Int;
-      Contract.Assert(t != null);
-      /*
-        if (paramType is AI.Ref)
-          t = Type.Ref;
-        else if (paramType is AI.FieldName)
-          t = Type.Name;
-        else
-          System.Console.WriteLine("*** unsupported type in AI {0}", paramType); */
-      Contract.Assert(false);
-      throw new cce.UnreachableException();
-      TypedIdent id = new TypedIdent(Token.NoToken, "propfactory_freshvar" + freshVarNum, t);
-      freshVarNum++;
-      return new BoundVariable(Token.NoToken, id);
-    }
   }
 
   public class BoogieValueFactory : BoogieFactory, AI.IValueExprFactory {
-- 
cgit v1.2.3