More line ending fixups.

7 files changed, 64 insertions, 64 deletions

diff --git a/Source/VCGeneration/Check.cs b/Source/VCGeneration/Check.cs
index 51318640..29574966 100644
--- a/Source/VCGeneration/Check.cs
+++ b/Source/VCGeneration/Check.cs
@@ -227,7 +227,7 @@ void ObjectInvariant()
     public void PushVCExpr(VCExpr vc)

     {

       Contract.Requires(vc != null);

-      //thmProver.Context.AddAxiom(vc);
+      //thmProver.Context.AddAxiom(vc);

       thmProver.PushVCExpression(vc);

     }

 

@@ -326,7 +326,7 @@ void ObjectInvariant()
   public class ErrorModel {

     public Dictionary<string/*!*/, int>/*!*/ identifierToPartition;

     public List<List<string/*!>>!*/>> partitionToIdentifiers;

-    public List<Object>/*!*/ partitionToValue;
+    public List<Object>/*!*/ partitionToValue;

     public Dictionary<object, int>/*!*/ valueToPartition;

     public Dictionary<string/*!*/, List<List<int>>/*!*/>/*!*/ definedFunctions;

 

@@ -436,7 +436,7 @@ void ObjectInvariant()
         {

           if (values[i] == tuple[j]) {

             // succeeded in matching tuple[j]

-            j++;
+            j++;

             if (j == tuple.Count-1) return tuple[tuple.Count - 1];

           }

         }

diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs
index 28744b27..b5f35b1e 100644
--- a/Source/VCGeneration/ConditionGeneration.cs
+++ b/Source/VCGeneration/ConditionGeneration.cs
@@ -78,7 +78,7 @@ namespace Microsoft.Boogie {
         if (b.tok == null) {

           Console.WriteLine("    <intermediate block>");

         } else {

-          // for ErrorTrace == 1 restrict the output;
+          // for ErrorTrace == 1 restrict the output;

           // do not print tokens with -17:-4 as their location because they have been 

           // introduced in the translation and do not give any useful feedback to the user

           if (!(CommandLineOptions.Clo.ErrorTrace == 1 && b.tok.line == -17 && b.tok.col == -4)) {

diff --git a/Source/VCGeneration/Context.cs b/Source/VCGeneration/Context.cs
index 81273319..da0bc5b0 100644
--- a/Source/VCGeneration/Context.cs
+++ b/Source/VCGeneration/Context.cs
@@ -252,7 +252,7 @@ void ObjectInvariant()
   public abstract class VCExprTranslator : ICloneable {

     public abstract string translate(VCExpr expr, int polarity);

     public abstract string Lookup(VCExprVar var);

-    public abstract Object Clone();
+    public abstract Object Clone();

   }

 

   [ContractClassFor(typeof(VCExprTranslator))]

diff --git a/Source/VCGeneration/DoomCheck.cs b/Source/VCGeneration/DoomCheck.cs
index d4ee1f35..2407fecf 100644
--- a/Source/VCGeneration/DoomCheck.cs
+++ b/Source/VCGeneration/DoomCheck.cs
@@ -39,12 +39,12 @@ void ObjectInvariant()
 }

 

         private Checker m_Checker;

-        private DoomErrorHandler m_ErrorHandler;
+        private DoomErrorHandler m_ErrorHandler;

         

         [NotDelayed]

         public Evc(Checker check) {

           Contract.Requires(check != null);

-            m_Checker = check;
+            m_Checker = check;

                    

         }

         

@@ -61,11 +61,11 @@ void ObjectInvariant()
             // Todo: Check if vc is trivial true or false            

             outcome = ProverInterface.Outcome.Undetermined;

             Contract.Assert( m_ErrorHandler !=null);

-            m_Checker.BeginCheck(reachvar.Name, vc, m_ErrorHandler);
+            m_Checker.BeginCheck(reachvar.Name, vc, m_ErrorHandler);

             m_Checker.ProverDone.WaitOne();

             

             try {

-              outcome = m_Checker.ReadOutcome();
+              outcome = m_Checker.ReadOutcome();

             } catch (UnexpectedProverOutputException e)

             {

               if (CommandLineOptions.Clo.TraceVerify) { 

@@ -102,17 +102,17 @@ void ObjectInvariant()
             }

         }

         

-        private DoomErrorHandler m_ErrHandler;
-        private Checker m_Check;
-        private InclusionOrder m_Order;
-        private Evc m_Evc;
+        private DoomErrorHandler m_ErrHandler;

+        private Checker m_Check;

+        private InclusionOrder m_Order;

+        private Evc m_Evc;

         #endregion

         

         [NotDelayed]

         public DoomCheck (Implementation passive_impl, Checker check) {

           Contract.Requires(passive_impl != null);

           Contract.Requires(check != null);

-            m_Check = check;
+            m_Check = check;

             if (!VC.DCGen.UseItAsDebugger ) {  

                 m_Order = new InclusionOrder(passive_impl.Blocks[0]);

             } else {

@@ -126,7 +126,7 @@ void ObjectInvariant()
             Contract.Assert( l2a!=null);

             Label2Absy = l2a;

 //            vce = check.VCExprGen.Implies(vce, vce);

-            m_Evc.Initialize(vce);
+            m_Evc.Initialize(vce);

         }

 

         /* - Set b to the next block that needs to be checked.

@@ -148,9 +148,9 @@ void ObjectInvariant()
                 if (!m_Order.SetCurrentResult(reachvar, outcome, m_ErrHandler)) {

                     outcome = ProverInterface.Outcome.Undetermined;

                 }

-                return true;
+                return true;

             } else {

-                m_Order.SetCurrentResult(reachvar, ProverInterface.Outcome.Undetermined, m_ErrHandler);
+                m_Order.SetCurrentResult(reachvar, ProverInterface.Outcome.Undetermined, m_ErrHandler);

                 return false;

             }

         }

@@ -215,8 +215,8 @@ void ObjectInvariant()
                             ConsoleColor col = Console.ForegroundColor;

                             Console.ForegroundColor = ConsoleColor.Green; 					    

 					        Console.WriteLine(vc.ToString());

-                            Console.ForegroundColor = col;
-                            Console.WriteLine(" ... was asked.");
+                            Console.ForegroundColor = col;

+                            Console.WriteLine(" ... was asked.");

                         */

                                                                  

 					    }

@@ -227,7 +227,7 @@ void ObjectInvariant()
 				    default:

 					    Contract.Assert(false);throw new cce.UnreachableException();  // unexpected enumeration value

 			    }

-			    return vc;
+			    return vc;

         }

 

         public VCExpr LetVC(Block startBlock,

@@ -294,7 +294,7 @@ void ObjectInvariant()
 

             VCExpr vc = Wlp.Block(block, SuccCorrect, context);

 

-            v = gen.Variable(block.Label + "_correct", Microsoft.Boogie.Type.Bool);
+            v = gen.Variable(block.Label + "_correct", Microsoft.Boogie.Type.Bool);

             

             bindings.Add(gen.LetBinding(v, vc));

             blockVariables.Add(block, v);

@@ -314,7 +314,7 @@ void ObjectInvariant()
             public List<List<Block/*!*/>/*!*/>/*!*/ DetectedBlock = new List<List<Block/*!*/>/*!*/>();

  

             

-            InclusionTree RootNode = new InclusionTree(null);
+            InclusionTree RootNode = new InclusionTree(null);

             InclusionTree currentNode = null;

             [ContractInvariantMethod]

 void ObjectInvariant() 

@@ -340,7 +340,7 @@ void ObjectInvariant()
                 Dictionary<Block, List<Block>> unavoidablemap = new Dictionary<Block, List<Block>>();

 

                 Block exitblock = BreadthFirst(rootblock, map2);Contract.Assert(exitblock != null);

-                BreadthFirstBwd(exitblock, map);
+                BreadthFirstBwd(exitblock, map);

 

                 foreach (KeyValuePair<Block, TraceNode> kvp in map) {

                   Contract.Assert(kvp.Key != null);Contract.Assert(kvp.Value != null);

@@ -371,7 +371,7 @@ void ObjectInvariant()
                     Insert2Tree(RootNode,kvp);

                 }

                 InitCurrentNode(RootNode);

-                //printtree(RootNode, "",0);
+                //printtree(RootNode, "",0);

             }

                                   

             void InitCurrentNode(InclusionTree n) {Contract.Requires(n != null);

@@ -424,12 +424,12 @@ void ObjectInvariant()
                     if (currentNode != null) {

                         currentNode.IsDoomed = false;

                         currentNode.HasBeenChecked = true;

-                        MarkUndoomedParents(currentNode);
+                        MarkUndoomedParents(currentNode);

                         if (cb != null) {

                             //Console.WriteLine("CE contains: ");

                             foreach (Block b in cb.TraceNodes)

                             {Contract.Assert(b != null);

-                                //Console.Write("{0}, ", b.Label);
+                                //Console.Write("{0}, ", b.Label);

                                 MarkUndoomedFromCE(b, RootNode);

                             }

                             //Console.WriteLine();

@@ -447,14 +447,14 @@ void ObjectInvariant()
 //                        if (ECContainsAssertFalse(currentNode.EquivBlock)) {  

 //                        

 //                            ConsoleColor col = Console.ForegroundColor;

-//                            Console.ForegroundColor = ConsoleColor.Blue;
+//                            Console.ForegroundColor = ConsoleColor.Blue;

 //                            Console.WriteLine("Assert false or PossiblyUnreachable was detected, but ignored");

-//                            Console.ForegroundColor = col;
+//                            Console.ForegroundColor = col;

 //

-//                            currentNode.HasBeenChecked = true;
-//                            currentNode.IsDoomed = false;
-//                            currentNode = currentNode.Parent;
-//                            return false;
+//                            currentNode.HasBeenChecked = true;

+//                            currentNode.IsDoomed = false;

+//                            currentNode = currentNode.Parent;

+//                            return false;

 //                        }

                         

                         List<Block> traceblocks = new List<Block>();

@@ -464,7 +464,7 @@ void ObjectInvariant()
                         

 //                        cb.OnWarning("Doomed program points found!");

                         if (cb != null) {

-                            cb.OnDoom(reachvar, currentNode.EquivBlock, traceblocks);
+                            cb.OnDoom(reachvar, currentNode.EquivBlock, traceblocks);

                         }

                                                 

                         if (currentNode.EquivBlock.Count>0) {

@@ -596,7 +596,7 @@ void ObjectInvariant()
                                     

             InclusionTree FindNextNode(InclusionTree n) {Contract.Requires(n != null);

                 Contract.Assert( n!=n.Parent);

-                InclusionTree next = n.Parent;
+                InclusionTree next = n.Parent;

                 if (next!=null) {

                   foreach (InclusionTree n0 in next.Children) {

                     Contract.Assert(n0 != null);

@@ -604,7 +604,7 @@ void ObjectInvariant()
                             return n0;

                         }

                     }

-                    return FindNextNode(next);
+                    return FindNextNode(next);

                 }                

                 return next;

             }

@@ -662,7 +662,7 @@ void ObjectInvariant()
             bool IsSubset(List<Block> sub, List<Block> super ) {Contract.Requires(sub!=null);Contract.Requires(cce.NonNullElements(super));

                 foreach (Block b in sub) {

                   Contract.Assert(b != null);

-                    if (!super.Contains(b) ) return false;
+                    if (!super.Contains(b) ) return false;

                 }

                 return true;

             }

@@ -683,7 +683,7 @@ void ObjectInvariant()
             private class InclusionTree {

                 public InclusionTree(InclusionTree p) {

                     Parent = p;

-                    HasBeenChecked=false;
+                    HasBeenChecked=false;

                     IsDoomed = false;

                 }

                 

@@ -731,7 +731,7 @@ void ObjectInvariant()
                         Contract.Assert( firstpred!=null);

                         if (blockmap.TryGetValue(firstpred, out t0)) {

                             Contract.Assert( t0 !=null);

-                            tn.Unavoidables.AddRange(t0.Unavoidables);
+                            tn.Unavoidables.AddRange(t0.Unavoidables);

                         }

                     }   

                                          

@@ -739,8 +739,8 @@ void ObjectInvariant()
                         TraceNode t = null;

                         if (blockmap.TryGetValue(b0, out t)) {

                             Contract.Assert( t!=null);

-                            tn.Predecessors.Add(t);
-                            IntersectUnavoidables(t,tn);
+                            tn.Predecessors.Add(t);

+                            IntersectUnavoidables(t,tn);

                             if (!t.Successors.Contains(tn)) t.Successors.Add(tn);

                             blockmap[b0]=t;

                         }

@@ -807,7 +807,7 @@ void ObjectInvariant()
                         Contract.Assert( firstpred!=null);

                         if (blockmap.TryGetValue(firstpred, out t0)) {

                             Contract.Assert( t0 !=null);

-                            tn.Unavoidables.AddRange(t0.Unavoidables);
+                            tn.Unavoidables.AddRange(t0.Unavoidables);

                         }

                       

                                          

@@ -815,8 +815,8 @@ void ObjectInvariant()
                             TraceNode t = null;

                             if (blockmap.TryGetValue(b0, out t)) {

                                 Contract.Assert( t!=null);

-                                tn.Successors.Add(t);
-                                IntersectUnavoidables(t,tn);
+                                tn.Successors.Add(t);

+                                IntersectUnavoidables(t,tn);

                                 if (!t.Predecessors.Contains(tn)) t.Predecessors.Add(tn);

                                 blockmap[b0]=t;

                             }

@@ -880,7 +880,7 @@ void ObjectInvariant()
 

                 public TraceNode(Block b) {

                   Contract.Requires(b != null);

-                    block=b;
+                    block=b;

                 }

                 

             }

diff --git a/Source/VCGeneration/DoomErrorHandler.cs b/Source/VCGeneration/DoomErrorHandler.cs
index f31b597e..0bcf15f8 100644
--- a/Source/VCGeneration/DoomErrorHandler.cs
+++ b/Source/VCGeneration/DoomErrorHandler.cs
@@ -59,7 +59,7 @@ void ObjectInvariant()
           Contract.Requires(cce.NonNullElements(traceblocks));

             m_Reachvar = reachvar;

             m_DoomedBlocks = doomedblocks;

-            m_TraceBlocks = traceblocks;
+            m_TraceBlocks = traceblocks;

         }

         

         

@@ -90,7 +90,7 @@ void ObjectInvariant()
             //Console.Write("{0}, ", b.Label);

           } else {

             AssertCmd a = (AssertCmd)node;

-            assertNodes.Add(a);
+            assertNodes.Add(a);

           }

         }

         m_CurrentTrace.AddRange(traceNodes);

diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index cf386e77..287d3a27 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1706,7 +1706,7 @@ namespace VC {
       CheckIntAttributeOnImpl(impl, "vcs_max_splits", ref max_splits);

       CheckIntAttributeOnImpl(impl, "vcs_max_keep_going_splits", ref max_kg_splits);

       if (tmp_max_vc_cost >= 0) { 

-        max_vc_cost = tmp_max_vc_cost;
+        max_vc_cost = tmp_max_vc_cost;

       }

 

       Outcome outcome = Outcome.Correct;

@@ -1721,7 +1721,7 @@ namespace VC {
       int total = 0;

       int no = max_splits == 1 && !keep_going ? -1 : 0;

       bool first_round = true;

-      bool do_splitting = keep_going || max_splits > 1;
+      bool do_splitting = keep_going || max_splits > 1;

       double remaining_cost = 0.0, proven_cost = 0.0;

 

       if (do_splitting) {

@@ -1952,7 +1952,7 @@ namespace VC {
 		   reporter.underapproximationMode = false;

 	       

 		   //Console.Write("Checking with preds == true: "); Console.Out.Flush();

-		   ret = CheckVC(vc, reporter, checker, impl.Name);
+		   ret = CheckVC(vc, reporter, checker, impl.Name);

 		   //Console.WriteLine(ret.ToString());

 	       

 		   if(ret == Outcome.Correct) {

@@ -2220,7 +2220,7 @@ namespace VC {
         VCExprNAry vnary = node as VCExprNAry;

         if(vnary == null) return true;

         VCExprBoogieFunctionOp bop = vnary.Op as VCExprBoogieFunctionOp;

-        if(bop == null) return true;
+        if(bop == null) return true;

         if(implName2StratifiedInliningInfo.ContainsKey(bop.Func.Name)) {

            fcalls.Add(vnary);

         }

@@ -3236,7 +3236,7 @@ namespace VC {
         {

           Block entryBlock = cce.NonNull( impl.Blocks[0]);

           RemoveEmptyBlocks(entryBlock);

-          impl.PruneUnreachableBlocks();
+          impl.PruneUnreachableBlocks();

         }

         #endregion Get rid of empty blocks

         

@@ -3318,7 +3318,7 @@ namespace VC {
         for (int i = 0; i < cmds.Length; i++)

         {

           Cmd cmd = cce.NonNull( cmds[i]);

-          AssertCmd assertCmd = cmd as AssertCmd;
+          AssertCmd assertCmd = cmd as AssertCmd;

           if (assertCmd != null && errModel.LookupControlFlowFunctionAt(cfcValue, assertCmd.UniqueId) == 0)

           {

             Counterexample newCounterexample;

@@ -3468,7 +3468,7 @@ namespace VC {
         string calleeName = naryExpr.Fun.FunctionName;

         if (!implName2LazyInliningInfo.ContainsKey(calleeName)) continue;

         VCExprTranslator vcExprTranslator = cce.NonNull(context.exprTranslator);

-        Boogie2VCExprTranslator boogieExprTranslator = context.BoogieExprTranslator;
+        Boogie2VCExprTranslator boogieExprTranslator = context.BoogieExprTranslator;

         Contract.Assert(boogieExprTranslator != null);

         List<int> args = new List<int>();

         foreach (Expr expr in naryExpr.Args)

diff --git a/Source/VCGeneration/VCDoomed.cs b/Source/VCGeneration/VCDoomed.cs
index 55b1131f..d44547a8 100644
--- a/Source/VCGeneration/VCDoomed.cs
+++ b/Source/VCGeneration/VCDoomed.cs
@@ -182,7 +182,7 @@ namespace VC {
         Dictionary<Block, Block> tmpdict = new Dictionary<Block, Block>();

         CopyImplBlocks(impl.Blocks[0], ref blist, impl.Blocks[0], ref tmpdict);

         blist.Reverse();

-        //_tmpImpl = new Implementation(impl.tok, impl.Name, impl.TypeParameters, impl.InParams, impl.OutParams, impl.LocVars, blist);
+        //_tmpImpl = new Implementation(impl.tok, impl.Name, impl.TypeParameters, impl.InParams, impl.OutParams, impl.LocVars, blist);

 

         #endregion ////////////////////////////////////

 

@@ -291,7 +291,7 @@ namespace VC {
       UseItAsDebugger = CommandLineOptions.Clo.useDoomDebug;

       Stopwatch watch = new Stopwatch();

 

-      //Impl2Dot(impl, String.Format("c:/dot/{0}_raw.dot", impl.Name) );
+      //Impl2Dot(impl, String.Format("c:/dot/{0}_raw.dot", impl.Name) );

 

       if (CommandLineOptions.Clo.TraceVerify) {

         Console.WriteLine(">>> Checking function {0} for doomed points.", impl.Name);

@@ -333,10 +333,10 @@ namespace VC {
 

 

       #endregion

-      //EmitImpl(impl,false);
+      //EmitImpl(impl,false);

 

 

-      //Impl2Dot(impl, String.Format("c:/dot/{0}_passive.dot", impl.Name) );
+      //Impl2Dot(impl, String.Format("c:/dot/{0}_passive.dot", impl.Name) );

 

       // ---------------------------------------------------------------------------

       if (UseItAsDebugger) {

@@ -350,9 +350,9 @@ namespace VC {
       }

       // ---------------------------------------------------------------------------      

 

-      // EmitImpl(impl,false);
+      // EmitImpl(impl,false);

 

-      //Impl2Dot(impl, String.Format("c:/dot/{0}_final.dot", impl.Name) );
+      //Impl2Dot(impl, String.Format("c:/dot/{0}_final.dot", impl.Name) );

 

       bool __debug = false;

 

@@ -419,7 +419,7 @@ namespace VC {
       #region Try to produce a counter example (brute force)

       if (dc.DoomedSequences.Count > 0) {

         ConsoleColor col = Console.ForegroundColor;

-        //        Console.ForegroundColor = ConsoleColor.Red;
+        //        Console.ForegroundColor = ConsoleColor.Red;

         //        Console.WriteLine("  {0} is DOOMED!", impl.Name);

         //        foreach (List<Block!> bl in dc.DoomedSequences) {

         //            Console.Write("Doomed Blocks: ");

@@ -715,12 +715,12 @@ namespace VC {
             //                    Console.Write("   Witness (");

             //                    

             //                    ConsoleColor col = Console.ForegroundColor;

-            //                    Console.ForegroundColor = ConsoleColor.White;
-            //                    Console.Write("{0};{1}", b.Cmds[endidx].tok.line, b.Cmds[endidx].tok.col );
+            //                    Console.ForegroundColor = ConsoleColor.White;

+            //                    Console.Write("{0};{1}", b.Cmds[endidx].tok.line, b.Cmds[endidx].tok.col );

             //                    Console.ForegroundColor = col;

-            //                    Console.Write("):   ");
+            //                    Console.Write("):   ");

             //                    Console.ForegroundColor = ConsoleColor.Yellow;

-            //                    b.Cmds[endidx].Emit(new TokenTextWriter("<console>", Console.Out, false), 0);
+            //                    b.Cmds[endidx].Emit(new TokenTextWriter("<console>", Console.Out, false), 0);

             //                    Console.ForegroundColor = col;

 

             m_doomedCmds.Add(b.Cmds[endidx]);