From 471bfd72d5c49ae66f0c64504e5eacc006f083f1 Mon Sep 17 00:00:00 2001 From: tabarbe Date: Wed, 4 Aug 2010 21:52:41 +0000 Subject: Boogie: Removed trailing spaces in code --- Source/AIFramework/CommonFunctionSymbols.ssc | 4 ++-- Source/AIFramework/Functional.ssc | 8 ++++---- Source/AIFramework/MultiLattice.ssc | 4 ++-- Source/AIFramework/Mutable.ssc | 4 ++-- .../Polyhedra/LinearConstraintSystem.ssc | 2 +- .../VariableMap/ConstantAbstraction.ssc | 4 ++-- .../VariableMap/ConstantExpressions.ssc | 18 ++++++++-------- Source/AIFramework/VariableMap/Intervals.ssc | 24 +++++++++++----------- .../AIFramework/VariableMap/VariableMapLattice.ssc | 16 +++++++-------- 9 files changed, 42 insertions(+), 42 deletions(-) (limited to 'Source/AIFramework') 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; /// @@ -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 /// 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 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! varsToRemove = new List(); + List! varsToRemove = new List(); foreach(IVariable var in result. @@ -252,7 +252,7 @@ namespace Microsoft.AbstractInterpretationFramework { List dependingVars = this.variableDependences[var]; List clonedDependingVars = new List(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(); } /// @@ -67,7 +67,7 @@ namespace Microsoft.AbstractInterpretationFramework { IntervalElement interval = (IntervalElement) element; - return interval.IsBottom(); + return interval.IsBottom(); } /// @@ -83,7 +83,7 @@ namespace Microsoft.AbstractInterpretationFramework IntervalElement! join = IntervalElement.Factory(inf, sup); - return join; + return join; } /// @@ -146,9 +146,9 @@ namespace Microsoft.AbstractInterpretationFramework /// 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 /// public override bool Understands(IFunctionSymbol! f, IList /* @@ -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/**/! VariablesInExpression(IExpr! e, ISet/**/! 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; } -- cgit v1.2.3