Boogie: removed unreachable or unused code

2 files changed, 7 insertions, 50 deletions

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 {