diff options
author | wuestholz <unknown> | 2013-05-24 10:01:07 -0700 |
---|---|---|
committer | wuestholz <unknown> | 2013-05-24 10:01:07 -0700 |
commit | a05745053d88f93508d33eacd38c69b339a45d50 (patch) | |
tree | 441d95aef81095f3038e809e88e53a6281005123 /Source/VCGeneration/ConditionGeneration.cs | |
parent | 21f72bdf46f12d214ac1f58bcc1041de2827ff40 (diff) |
Changed the 'CounterexampleComparer' to take error messages of assertions into account.
Diffstat (limited to 'Source/VCGeneration/ConditionGeneration.cs')
-rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 20 |
1 files changed, 19 insertions, 1 deletions
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index 8e28362b..d0f403d1 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -299,13 +299,31 @@ namespace Microsoft.Boogie { }
public class CounterexampleComparer : IComparer<Counterexample> {
- public int Compare(Counterexample c1, Counterexample c2) {
+ public int Compare(Counterexample c1, Counterexample c2)
+ {
//Contract.Requires(c1 != null);
//Contract.Requires(c2 != null);
if (c1.GetLocation() == c2.GetLocation())
+ {
+ // TODO(wuestholz): Generalize this to compare all IPotentialErrorNodes of the counterexample.
+ var a1 = c1 as AssertCounterexample;
+ var a2 = c2 as AssertCounterexample;
+ if (a1 != null && a2 != null)
+ {
+ var s1 = a1.FailingAssert.ErrorData as string;
+ var s2 = a2.FailingAssert.ErrorData as string;
+ if (s1 != null && s2 != null)
+ {
+ return s1.CompareTo(s2);
+ }
+ }
+
return 0;
+ }
if (c1.GetLocation() > c2.GetLocation())
+ {
return 1;
+ }
return -1;
}
}
|