Normalise line endings using a .gitattributes file. Unfortunately

this required that this commit globally modify most files. If you
want to use git blame to see the real author of a line use the
``-w`` flag so that whitespace changes are ignored.

1 files changed, 85 insertions, 85 deletions

diff --git a/Source/Doomed/DoomErrorHandler.cs b/Source/Doomed/DoomErrorHandler.cs
index 8d89bae3..ce14ff73 100644
--- a/Source/Doomed/DoomErrorHandler.cs
+++ b/Source/Doomed/DoomErrorHandler.cs
@@ -1,86 +1,86 @@
-using System;

-using System.Collections;

-using System.Collections.Generic;

-using System.Diagnostics;

-using System.Threading;

-using System.IO;

-using Microsoft.Boogie;

-using Microsoft.Boogie.GraphUtil;

-using System.Diagnostics.Contracts;

-using Microsoft.Basetypes;

-using Microsoft.Boogie.VCExprAST;

-

-namespace VC

-{

-    internal class DoomErrorHandler : ProverInterface.ErrorHandler

-    {

-

-        protected Dictionary<int, Absy> label2Absy;

-        protected VerifierCallback callback;

-        private List<Block> m_CurrentTrace = new List<Block>();

-

-        [ContractInvariantMethod]

-        void ObjectInvariant()

-        {

-            Contract.Invariant(label2Absy != null);

-            Contract.Invariant(callback != null);

-            Contract.Invariant(cce.NonNullElements(m_CurrentTrace));

-        }

-

-

-        public DoomErrorHandler(Dictionary<int, Absy> label2Absy, VerifierCallback callback)

-        {

-            Contract.Requires(label2Absy != null);

-            Contract.Requires(callback != null);

-            this.label2Absy = label2Absy;

-            this.callback = callback;

-        }

-

-        public override Absy Label2Absy(string label)

-        {

-            //Contract.Requires(label != null);

-            Contract.Ensures(Contract.Result<Absy>() != null);

-

-            int id = int.Parse(label);

-            return cce.NonNull((Absy)label2Absy[id]);

-        }

-

-        public override void OnProverWarning(string msg)

-        {

-            //Contract.Requires(msg != null);

-            this.callback.OnWarning(msg);

-        }

-

-

-        public List<Block>/*!>!*/ TraceNodes

-        {

-            get

-            {

-                Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));

-

-                return m_CurrentTrace;

-            }

-        }

-

-        public override void OnModel(IList<string>/*!>!*/ labels, Model model, ProverInterface.Outcome proverOutcome)

-        {

-            // TODO: it would be better to check which reachability variables are actually set to one!

-            List<Block> traceNodes = new List<Block>();

-            List<AssertCmd> assertNodes = new List<AssertCmd>();            

-            foreach (string s in labels)

-            {

-                Contract.Assert(s != null);

-                Absy node = Label2Absy(s);

-                if (node is Block)

-                {

-                    Block b = (Block)node;

-                    traceNodes.Add(b);

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

-                }

-            }

-            m_CurrentTrace.AddRange(traceNodes);

-        }

-

-    }

-

+using System;
+using System.Collections;
+using System.Collections.Generic;
+using System.Diagnostics;
+using System.Threading;
+using System.IO;
+using Microsoft.Boogie;
+using Microsoft.Boogie.GraphUtil;
+using System.Diagnostics.Contracts;
+using Microsoft.Basetypes;
+using Microsoft.Boogie.VCExprAST;
+
+namespace VC
+{
+    internal class DoomErrorHandler : ProverInterface.ErrorHandler
+    {
+
+        protected Dictionary<int, Absy> label2Absy;
+        protected VerifierCallback callback;
+        private List<Block> m_CurrentTrace = new List<Block>();
+
+        [ContractInvariantMethod]
+        void ObjectInvariant()
+        {
+            Contract.Invariant(label2Absy != null);
+            Contract.Invariant(callback != null);
+            Contract.Invariant(cce.NonNullElements(m_CurrentTrace));
+        }
+
+
+        public DoomErrorHandler(Dictionary<int, Absy> label2Absy, VerifierCallback callback)
+        {
+            Contract.Requires(label2Absy != null);
+            Contract.Requires(callback != null);
+            this.label2Absy = label2Absy;
+            this.callback = callback;
+        }
+
+        public override Absy Label2Absy(string label)
+        {
+            //Contract.Requires(label != null);
+            Contract.Ensures(Contract.Result<Absy>() != null);
+
+            int id = int.Parse(label);
+            return cce.NonNull((Absy)label2Absy[id]);
+        }
+
+        public override void OnProverWarning(string msg)
+        {
+            //Contract.Requires(msg != null);
+            this.callback.OnWarning(msg);
+        }
+
+
+        public List<Block>/*!>!*/ TraceNodes
+        {
+            get
+            {
+                Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));
+
+                return m_CurrentTrace;
+            }
+        }
+
+        public override void OnModel(IList<string>/*!>!*/ labels, Model model, ProverInterface.Outcome proverOutcome)
+        {
+            // TODO: it would be better to check which reachability variables are actually set to one!
+            List<Block> traceNodes = new List<Block>();
+            List<AssertCmd> assertNodes = new List<AssertCmd>();            
+            foreach (string s in labels)
+            {
+                Contract.Assert(s != null);
+                Absy node = Label2Absy(s);
+                if (node is Block)
+                {
+                    Block b = (Block)node;
+                    traceNodes.Add(b);
+                    //Console.Write("{0}, ", b.Label);
+                }
+            }
+            m_CurrentTrace.AddRange(traceNodes);
+        }
+
+    }
+
 }
\ No newline at end of file