Boogie: Removed trailing spaces in code

4 files changed, 31 insertions, 31 deletions

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;

           }