1 files changed, 41 insertions, 16 deletions
diff --git a/Source/VCGeneration/DoomErrorHandler.cs b/Source/VCGeneration/DoomErrorHandler.cs
index 860f5334..010fce95 100644
--- a/Source/VCGeneration/DoomErrorHandler.cs
+++ b/Source/VCGeneration/DoomErrorHandler.cs
@@ -7,7 +7,7 @@ using System.IO;
 using Microsoft.Boogie;
 using Graphing;
 using AI = Microsoft.AbstractInterpretationFramework;
-using Microsoft.Contracts;
+using System.Diagnostics.Contracts;
 using Microsoft.Basetypes;
 using Microsoft.Boogie.VCExprAST;
 
@@ -15,49 +15,74 @@ namespace VC
 {
     internal class DoomErrorHandler : ProverInterface.ErrorHandler {
 
-        protected Hashtable! label2Absy;
-        protected VerifierCallback! callback;
-        
+        protected Hashtable label2Absy;
+        protected VerifierCallback callback;
+        private List<Block> m_CurrentTrace = new List<Block>();
         public Variable m_Reachvar;
-        public List<Block!> m_DoomedBlocks, m_TraceBlocks;
+        public List<Block> m_DoomedBlocks, m_TraceBlocks;
         
+      [ContractInvariantMethod]
+void ObjectInvariant() 
+{
+    Contract.Invariant(label2Absy!=null);
+        Contract.Invariant(callback != null);
+        Contract.Invariant(cce.NonNullElements(m_CurrentTrace));
+        Contract.Invariant(m_Reachvar != null);
+        Contract.Invariant(m_DoomedBlocks != null);
+        Contract.Invariant(m_TraceBlocks != null);
+}
+
         
-        public DoomErrorHandler(Hashtable! label2Absy, VerifierCallback! callback) {
+        public DoomErrorHandler(Hashtable label2Absy, VerifierCallback callback) {
+          Contract.Requires(label2Absy != null);
+          Contract.Requires(callback != null);
           this.label2Absy = label2Absy;
           this.callback = callback;
         }
         
-        public override Absy! Label2Absy(string! label) {
+        public override Absy Label2Absy(string label) {
+          Contract.Requires(label != null);
+          Contract.Ensures(Contract.Result<Absy>() != null);
+
           int id = int.Parse(label);
-          return (Absy!) label2Absy[id];
+          return cce.NonNull((Absy) label2Absy[id]);
         }
         
-        public override void OnProverWarning(string! msg) {
+        public override void OnProverWarning(string msg) {
+          Contract.Requires(msg != null);
           this.callback.OnWarning(msg);
         }
    
-        public void OnDoom(Variable! reachvar, List<Block!>! doomedblocks, List<Block!>! traceblocks) {
+        public void OnDoom(Variable reachvar, List<Block>/*!>!*/ doomedblocks, List<Block>/*!>!*/ traceblocks) {
+      Contract.Requires(reachvar != null);
+          Contract.Requires(cce.NonNullElements(doomedblocks));
+          Contract.Requires(cce.NonNullElements(traceblocks));
             m_Reachvar = reachvar;
             m_DoomedBlocks = doomedblocks;
             m_TraceBlocks = traceblocks;            
         }
         
-        private List<Block!>! m_CurrentTrace = new List<Block!>();
         
-        public List<Block!>! TraceNodes 
+        
+        public List<Block>/*!>!*/ TraceNodes 
         {
             get
             {
+              Contract.Ensures(cce.NonNullElements(Contract.Result<List<Block>>()));
+              
                 return m_CurrentTrace;
             }
         }
         
-        public override void OnModel(IList<string!>! labels, ErrorModel errModel) {
+        public override void OnModel(IList<string>/*!>!*/ labels, ErrorModel errModel) {
+          Contract.Requires(labels != null);
+          
         m_CurrentTrace.Clear();
         //Console.Write("Used Blocks: ");
-        List<Block!> traceNodes = new List<Block!>();
-        List<AssertCmd!> assertNodes = new List<AssertCmd!>();
-        foreach (string! s in labels) {
+        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;