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/AbsInt/AbstractInterpretation.cs | 14 +++++++------- Source/AbsInt/Traverse.cs | 2 +- 2 files changed, 8 insertions(+), 8 deletions(-) (limited to 'Source/AbsInt') diff --git a/Source/AbsInt/AbstractInterpretation.cs b/Source/AbsInt/AbstractInterpretation.cs index bf25434a..b1d16225 100644 --- a/Source/AbsInt/AbstractInterpretation.cs +++ b/Source/AbsInt/AbstractInterpretation.cs @@ -176,7 +176,7 @@ namespace Microsoft.Boogie.AbstractInterpretation { foreach (Implementation impl in implementations) { impl.AbstractFunction = AbstractFunction.Empty.WithPair(this.lattice.Bottom, this.lattice.Bottom); - this.implWorkItems.Enqueue(impl); + this.implWorkItems.Enqueue(impl); } while (this.implWorkItems.Count > 0) // until fixed point reached @@ -554,7 +554,7 @@ namespace Microsoft.Boogie.AbstractInterpretation { //PM: The following assertion follows from a nontrivial invariant of ArrayAssignCmd, //PM: which we do not have yet. Therefore, we put in an assume fo now. assume assmt.Index1 != null; - assert assmt.Index1 != null; + assert assmt.Index1 != null; // heap succession predicate Expr heapsucc = Expr.HeapSucc(oldHeap, newHeap, assmt.Index0, assmt.Index1); @@ -735,14 +735,14 @@ namespace Microsoft.Boogie.AbstractInterpretation { lattice.ToPredicate(incomingValue).DoVisit(freeVarsVisitorForA); lattice.ToPredicate(block.PreInvariant).DoVisit(freeVarsVisitorForB); - List! freeVarsOfA = freeVarsVisitorForA.FreeVariables; - List! freeVarsOfB = freeVarsVisitorForB.FreeVariables; + List! freeVarsOfA = freeVarsVisitorForA.FreeVariables; + List! freeVarsOfB = freeVarsVisitorForB.FreeVariables; System.Console.WriteLine("@@ Compared for block {0}:", block.Label); System.Console.WriteLine("@@ Incoming: {0}", lattice.ToPredicate((!) incomingValue)); - System.Console.WriteLine("@@ Free Variables : {0}", ToString(freeVarsOfA)); + System.Console.WriteLine("@@ Free Variables : {0}", ToString(freeVarsOfA)); System.Console.WriteLine("@@ Previous: {0}", lattice.ToPredicate(block.PreInvariant)); - System.Console.WriteLine("@@ Free Variables : {0}", ToString(freeVarsOfB)); + System.Console.WriteLine("@@ Free Variables : {0}", ToString(freeVarsOfB)); System.Console.WriteLine("@@ result = False"); System.Console.WriteLine("@@ end Compare"); string operation = ""; @@ -762,7 +762,7 @@ namespace Microsoft.Boogie.AbstractInterpretation { #endif // The default is to have have a widening that perform a (approximation of) the closure of the operands, so to improve the precision - // block.PreInvariant = WideningWithClosure.MorePreciseWiden(lattice, (!) block.PreInvariant, incomingValue); + // block.PreInvariant = WideningWithClosure.MorePreciseWiden(lattice, (!) block.PreInvariant, incomingValue); block.PreInvariant = (AI.Lattice.Element)lattice.Widen(block.PreInvariant, incomingValue); } block.iterations++; diff --git a/Source/AbsInt/Traverse.cs b/Source/AbsInt/Traverse.cs index 2890730b..c4f226d9 100644 --- a/Source/AbsInt/Traverse.cs +++ b/Source/AbsInt/Traverse.cs @@ -72,7 +72,7 @@ namespace Microsoft.Boogie { Contract.Assume(g.labelTargets != null); cce.BeginExpose(g.labelTargets); foreach (Block succ in g.labelTargets) - // invariant b.currentlyTraversed; + // invariant b.currentlyTraversed; //PM: The following loop invariant will work once properties are axiomatized //&& (g.labelNames != null && g.labelTargets != null ==> g.labelNames.Length == g.labelTargets.Length); { -- cgit v1.2.3