Boogie: Removed trailing spaces in code

9 files changed, 42 insertions, 42 deletions

diff --git a/Source/AIFramework/CommonFunctionSymbols.ssc b/Source/AIFramework/CommonFunctionSymbols.ssc
index e05e8dac..bc59df97 100644
--- a/Source/AIFramework/CommonFunctionSymbols.ssc
+++ b/Source/AIFramework/CommonFunctionSymbols.ssc
@@ -441,7 +441,7 @@ namespace Microsoft.AbstractInterpretationFramework
         private static readonly AIType! heaptype = new Heap();

         public static AIType! Type { get { return heaptype; } }

 

-        // the types in the following, select1, select2, are hard-coded; 

+        // the types in the following, select1, select2, are hard-coded;
         // these types may not always be appropriate

         private static readonly FunctionSymbol! _select1 = new FunctionSymbol("sel1",

             // Heap x FieldName -> Prop

@@ -455,7 +455,7 @@ namespace Microsoft.AbstractInterpretationFramework
         );

         public static FunctionSymbol! Select2 { get { return _select2; } }

 

-        // the types in the following, store1, store2, are hard-coded; 

+        // the types in the following, store1, store2, are hard-coded;
         // these types may not always be appropriate

         private static readonly FunctionSymbol! _update1 = new FunctionSymbol("upd1",

             // Heap x FieldName x Value -> Heap

diff --git a/Source/AIFramework/Functional.ssc b/Source/AIFramework/Functional.ssc
index 1413230e..bee40031 100644
--- a/Source/AIFramework/Functional.ssc
+++ b/Source/AIFramework/Functional.ssc
@@ -102,7 +102,7 @@ namespace Microsoft.AbstractInterpretationFramework.Collections
             assume r != null;

             assert this.Contains(key);    // The entry must be defined

              

-            r[key] = value;  

+            r[key] = value;
             return new FunctionalHashtable(r);

         }

 

@@ -195,7 +195,7 @@ namespace Microsoft.AbstractInterpretationFramework.Collections
         public override int GetHashCode()

         {

             int h = this.first == null ? 0 : this.first.GetHashCode();

-            h ^= this.second == null ? 0 : this.second.GetHashCode(); 

+            h ^= this.second == null ? 0 : this.second.GetHashCode();
             return h;

         }

     }

@@ -232,7 +232,7 @@ namespace Microsoft.AbstractInterpretationFramework.Collections.Generic
         public override int GetHashCode()

         {

             int h = this.first == null ? 0 : this.first.GetHashCode();

-            h ^= this.second == null ? 0 : this.second.GetHashCode(); 

+            h ^= this.second == null ? 0 : this.second.GetHashCode();
             return h;

         }

         

@@ -271,7 +271,7 @@ namespace Microsoft.AbstractInterpretationFramework.Collections.Generic
         public override int GetHashCode()

         {

             int h = this.first == null ? 0 : this.first.GetHashCode();

-            h ^= this.second == null ? 0 : this.second.GetHashCode(); 

+            h ^= this.second == null ? 0 : this.second.GetHashCode();
             h ^= this.third == null ? 0 : this.third.GetHashCode();

             return h;

         }

diff --git a/Source/AIFramework/MultiLattice.ssc b/Source/AIFramework/MultiLattice.ssc
index 761f4c7e..514e2548 100644
--- a/Source/AIFramework/MultiLattice.ssc
+++ b/Source/AIFramework/MultiLattice.ssc
@@ -11,7 +11,7 @@ namespace Microsoft.AbstractInterpretationFramework
     using System.Diagnostics;

     using Microsoft.AbstractInterpretationFramework.Collections;

 

-    using Microsoft.Boogie;    

+    using Microsoft.Boogie;
     using ISet = Microsoft.Boogie.Set;

 

 

@@ -39,7 +39,7 @@ namespace Microsoft.AbstractInterpretationFramework
                     {

                         newEPL[i] = (Element) ((!)otherEPL[i]).Clone();

                     }

-                    this.elementPerLattice = newEPL;          

+                    this.elementPerLattice = newEPL;
                 }

             }

             

diff --git a/Source/AIFramework/Mutable.ssc b/Source/AIFramework/Mutable.ssc
index 36bb3647..6b5e0a20 100644
--- a/Source/AIFramework/Mutable.ssc
+++ b/Source/AIFramework/Mutable.ssc
@@ -5,7 +5,7 @@
 //-----------------------------------------------------------------------------

 namespace Microsoft.AbstractInterpretationFramework.Collections

 {

-    using System.Collections;   

+    using System.Collections;
     using Microsoft.Contracts;

 

     /// <summary>

@@ -52,7 +52,7 @@ namespace Microsoft.AbstractInterpretationFramework.Collections
         // ICollection members

         public void CopyTo (System.Array! a, int i) { 

           if (this.Count > a.Length - i) throw new System.ArgumentException();

-          int j = i; 

+          int j = i;
           foreach(object o in this){

             a.SetValue(o, j++);

           }

diff --git a/Source/AIFramework/Polyhedra/LinearConstraintSystem.ssc b/Source/AIFramework/Polyhedra/LinearConstraintSystem.ssc
index a99a4ee8..e444b0ca 100644
--- a/Source/AIFramework/Polyhedra/LinearConstraintSystem.ssc
+++ b/Source/AIFramework/Polyhedra/LinearConstraintSystem.ssc
@@ -717,7 +717,7 @@ namespace Microsoft.AbstractInterpretationFramework
 

       CHECK_NEXT_CONSTRAINT: {}

 #if DEBUG_PRINT

-        Console.WriteLine("Widen checking: done with that constraint"); 

+        Console.WriteLine("Widen checking: done with that constraint");
 #endif

       }

 

diff --git a/Source/AIFramework/VariableMap/ConstantAbstraction.ssc b/Source/AIFramework/VariableMap/ConstantAbstraction.ssc
index 97fb57ce..8ba3065f 100644
--- a/Source/AIFramework/VariableMap/ConstantAbstraction.ssc
+++ b/Source/AIFramework/VariableMap/ConstantAbstraction.ssc
@@ -67,13 +67,13 @@ namespace Microsoft.AbstractInterpretationFramework
         public override bool IsTop (Element! element)

         { 

             Elt e = (Elt)element;

-            return e.domainValue == Value.Top; 

+            return e.domainValue == Value.Top;
         }

 

         public override bool IsBottom    (Element! element)

         {

             Elt e = (Elt)element;

-            return e.domainValue == Value.Bottom; 

+            return e.domainValue == Value.Bottom;
         }

 

         public override Element! NontrivialJoin (Element! first, Element! second)

diff --git a/Source/AIFramework/VariableMap/ConstantExpressions.ssc b/Source/AIFramework/VariableMap/ConstantExpressions.ssc
index 306c4e8f..fcf49b25 100644
--- a/Source/AIFramework/VariableMap/ConstantExpressions.ssc
+++ b/Source/AIFramework/VariableMap/ConstantExpressions.ssc
@@ -82,7 +82,7 @@ namespace Microsoft.AbstractInterpretationFramework
         get

         {    

           assert (this.variableBindings == null) <==> (this.variableDependences == null);

-          return this.variableBindings == null && this.variableDependences == null;  

+          return this.variableBindings == null && this.variableDependences == null;
         }      

       }

 

@@ -91,7 +91,7 @@ namespace Microsoft.AbstractInterpretationFramework
       /// </summary>

       public static AbstractElement! Join(AbstractElement! left, AbstractElement! right)

       {

-        AbstractElement! result = new AbstractElement(); 

+        AbstractElement! result = new AbstractElement();
         

         // Put all the variables in the left

         foreach(IVariable! var in left.variableBindings.Keys)

@@ -103,7 +103,7 @@ namespace Microsoft.AbstractInterpretationFramework
 

           if(rightVal== null)   // the expression is not there

           {

-            result.variableBindings.Add(var, leftVal);  

+            result.variableBindings.Add(var, leftVal);
           }

           else    // both abstract elements have a definition for the variable....

           {

@@ -121,7 +121,7 @@ namespace Microsoft.AbstractInterpretationFramework
           

           if(rightVal== null)   // the expression is not there

           {

-            result.variableBindings.Add(var, rightVal);  

+            result.variableBindings.Add(var, rightVal);
           }

           else    // both abstract elements have a definition for the variable....

           {

@@ -219,18 +219,18 @@ namespace Microsoft.AbstractInterpretationFramework
           List<IVariable> depRight = right.variableDependences[var];

 

           // Intersect the two sets

-          result.variableDependences.Add(var, depLeft);    

+          result.variableDependences.Add(var, depLeft);
           foreach(IVariable v in depRight) 

           {

             if(!result.variableDependences.ContainsKey(v))

             {

-              result.variableDependences.Remove(v);              

+              result.variableDependences.Remove(v);
             }

           }              

         } 

 

         // Now we remove the dependencies with variables not in variableBindings

-        List<IVariable>! varsToRemove = new List<IVariable>();         

+        List<IVariable>! varsToRemove = new List<IVariable>();
     

        foreach(IVariable var in result.

           

@@ -252,7 +252,7 @@ namespace Microsoft.AbstractInterpretationFramework
         {

           List<IVariable> dependingVars = this.variableDependences[var];

           List<IVariable> clonedDependingVars = new List<IVariable>(dependingVars);

-          cloned.variableDependences.Add(var, clonedDependingVars);        

+          cloned.variableDependences.Add(var, clonedDependingVars);
         }

       }

 

@@ -268,7 +268,7 @@ namespace Microsoft.AbstractInterpretationFramework
 

       public override string! ToString() 

       {

-        string! retString = "";          

+        string! retString = "";
         retString += "Bindings";

         

         foreach(IVariable var in this.variableBindings.Keys)

diff --git a/Source/AIFramework/VariableMap/Intervals.ssc b/Source/AIFramework/VariableMap/Intervals.ssc
index 7f6211ba..f507e020 100644
--- a/Source/AIFramework/VariableMap/Intervals.ssc
+++ b/Source/AIFramework/VariableMap/Intervals.ssc
@@ -57,7 +57,7 @@ namespace Microsoft.AbstractInterpretationFramework
     {

       IntervalElement interval = (IntervalElement) element;

       

-      return interval.IsTop();      

+      return interval.IsTop();
     }

 

     /// <summary>

@@ -67,7 +67,7 @@ namespace Microsoft.AbstractInterpretationFramework
     {

       IntervalElement interval = (IntervalElement) element;

       

-      return interval.IsBottom(); 

+      return interval.IsBottom();
     }

 

     /// <summary>

@@ -83,7 +83,7 @@ namespace Microsoft.AbstractInterpretationFramework
 

       IntervalElement! join =  IntervalElement.Factory(inf, sup);

 

-      return join;    

+      return join;
     }

 

     /// <summary>

@@ -146,9 +146,9 @@ namespace Microsoft.AbstractInterpretationFramework
     /// </summary>

     public override IExpr! ToPredicate(IVariable! var, Element! element)

     {

-      IntervalElement! interval = (IntervalElement!) element;      

+      IntervalElement! interval = (IntervalElement!) element;
       IExpr lowerBound = null;

-      IExpr upperBound = null;      

+      IExpr upperBound = null;
 

       if(! (interval.Inf is InfinitaryInt)) 

       {

@@ -168,7 +168,7 @@ namespace Microsoft.AbstractInterpretationFramework
           return lowerBound;

       else 

         if(upperBound != null)

-          return upperBound;      

+          return upperBound;
       else      // If we reach this point, both lowerBound and upperBound are null, i.e. we have no bounds on var, so we return simply true...

           return this.factory.True;

     }    

@@ -178,7 +178,7 @@ namespace Microsoft.AbstractInterpretationFramework
     /// </summary>

     public override bool Understands(IFunctionSymbol! f, IList /*<IExpr*/ ! args)

     {          

-      return f.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq);  

+      return f.Equals(Microsoft.AbstractInterpretationFramework.Value.Eq);
     }

 

 

@@ -211,7 +211,7 @@ namespace Microsoft.AbstractInterpretationFramework
         }                

       }

       // otherwise we simply return Top

-      return IntervalElement.Top;      

+      return IntervalElement.Top;
     }

 

     /// <summary>

@@ -237,7 +237,7 @@ namespace Microsoft.AbstractInterpretationFramework
       }

       else if(exp is IFunApp)

       {    

-        IFunApp fun = (IFunApp) exp;      

+        IFunApp fun = (IFunApp) exp;
         

         if(fun.FunctionSymbol is IntSymbol)   // An integer

         {

@@ -271,7 +271,7 @@ namespace Microsoft.AbstractInterpretationFramework
           else if(fun.FunctionSymbol.Equals(Int.Div))

             retVal = leftVal / rightVal;

           else if(fun.FunctionSymbol.Equals(Int.Mod))

-            retVal = leftVal % rightVal;                

+            retVal = leftVal % rightVal;
         }

       }  

         

@@ -385,7 +385,7 @@ namespace Microsoft.AbstractInterpretationFramework
           ExtendedInt! inf = a.inf + b.inf;

           ExtendedInt! sup = a.sup + b.sup;

 

-          return Factory(inf, sup);                      

+          return Factory(inf, sup);
         }

 

          // Subtraction

@@ -394,7 +394,7 @@ namespace Microsoft.AbstractInterpretationFramework
           ExtendedInt! inf = a.inf - b.sup;

           ExtendedInt! sup = a.sup - b.inf;

 

-          IntervalElement! sub = Factory(inf, sup);                      

+          IntervalElement! sub = Factory(inf, sup);
 

           return sub;

         }       

diff --git a/Source/AIFramework/VariableMap/VariableMapLattice.ssc b/Source/AIFramework/VariableMap/VariableMapLattice.ssc
index 34f876f5..c0293493 100644
--- a/Source/AIFramework/VariableMap/VariableMapLattice.ssc
+++ b/Source/AIFramework/VariableMap/VariableMapLattice.ssc
@@ -78,7 +78,7 @@ namespace Microsoft.AbstractInterpretationFramework
 

             public bool IsBottom { 

                  get { 

-                   return this.constraints == null; 

+                   return this.constraints == null;
                  } 

             }

 

@@ -89,7 +89,7 @@ namespace Microsoft.AbstractInterpretationFramework
                   requires !this.IsBottom;

                 { 

                   assume this.constraints != null;

-                  return (!) this.constraints.Keys; 

+                  return (!) this.constraints.Keys;
                 } 

             }

 

@@ -117,7 +117,7 @@ namespace Microsoft.AbstractInterpretationFramework
                 requires !this.IsBottom;

                 { 

                   assume this.constraints != null;

-                  return (Element)constraints[key]; 

+                  return (Element)constraints[key];
                 } 

             }

 

@@ -303,7 +303,7 @@ namespace Microsoft.AbstractInterpretationFramework
             }

             Elt! join = new Elt(newMap);

         

-            // System.Console.WriteLine("{0} join {1} = {2} ", this.ToString(a), ToString(b), ToString(join)); 

+            // System.Console.WriteLine("{0} join {1} = {2} ", this.ToString(a), ToString(b), ToString(join));
 

             return join;

         }

@@ -368,9 +368,9 @@ namespace Microsoft.AbstractInterpretationFramework
             }

             Element! widen= new Elt(newMap);

       

-            // System.Console.WriteLine("{0} widen {1} = {2} ", this.ToString(a), ToString(b), ToString(widen)); 

+            // System.Console.WriteLine("{0} widen {1} = {2} ", this.ToString(a), ToString(b), ToString(widen));
 

-            return widen;  

+            return widen;
         }

 

         internal static ISet/*<IVariable!>*/! VariablesInExpression(IExpr! e, ISet/*<IVariable!>*/! ignoreVars)

@@ -482,7 +482,7 @@ namespace Microsoft.AbstractInterpretationFramework
           else 

           {

             IExpr! left = (IExpr!) fun.Arguments[0];

-            IExpr! right = (IExpr!) fun.Arguments[1];          

+            IExpr! right = (IExpr!) fun.Arguments[1];
 

             if(!(left is IVariable || right is IVariable))    // At least one of the two operands must be a variable

               return false;

@@ -493,7 +493,7 @@ namespace Microsoft.AbstractInterpretationFramework
                 || fun.FunctionSymbol.Equals(Int.Mul)

                 || fun.FunctionSymbol.Equals(Int.Div)

                 || fun.FunctionSymbol.Equals(Int.Mod))

-              return IsArithmeticExpr(left) && IsArithmeticExpr(right);          

+              return IsArithmeticExpr(left) && IsArithmeticExpr(right);
             else 

               return false;

           }