summaryrefslogtreecommitdiff
path: root/Source/Doomed/DoomErrorHandler.cs
diff options
context:
space:
mode:
authorGravatar Dan Liew <daniel.liew@imperial.ac.uk>2015-06-28 01:44:30 +0100
committerGravatar Dan Liew <daniel.liew@imperial.ac.uk>2015-06-28 01:44:30 +0100
commit962f8d5252b3f5ec4d19e0cd2a430934bd55cc6d (patch)
tree27d5f9b0d130c6c1a6758bc0b7456b0aa51e34e0 /Source/Doomed/DoomErrorHandler.cs
parente11d65009d0b4ba1327f5f5dd6b26367330611f0 (diff)
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.
Diffstat (limited to 'Source/Doomed/DoomErrorHandler.cs')
-rw-r--r--Source/Doomed/DoomErrorHandler.cs170
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