diff options
| author |  wuestholz <unknown> | 2013-05-26 15:53:05 -0700 |
|---|---|---|
| committer | wuestholz <unknown> | 2013-05-26 15:53:05 -0700 |
| commit | e6241dfdc9743cbbf3f1ae9fb61f3e3179a417f9 (patch) | |
| tree | 14ddef6c41595577c35fc8767bc56af1063ad813 | |
| parent | a05745053d88f93508d33eacd38c69b339a45d50 (diff) | |
Changed the 'CounterexampleComparer' to take traces into account.
| -rw-r--r-- | Source/VCGeneration/ConditionGeneration.cs | 34 | ||||
| -rw-r--r-- | Test/prover/Answer | 4 |
2 files changed, 36 insertions, 2 deletions
diff --git a/Source/VCGeneration/ConditionGeneration.cs b/Source/VCGeneration/ConditionGeneration.cs index d0f403d1..092d12d2 100644 --- a/Source/VCGeneration/ConditionGeneration.cs +++ b/Source/VCGeneration/ConditionGeneration.cs @@ -299,12 +299,46 @@ namespace Microsoft.Boogie { }
public class CounterexampleComparer : IComparer<Counterexample> {
+
+ private int Compare(BlockSeq bs1, BlockSeq bs2)
+ {
+ if (bs1.Length < bs2.Length)
+ {
+ return -1;
+ }
+ else if (bs2.Length < bs1.Length)
+ {
+ return 1;
+ }
+
+ for (int i = 0; i < bs1.Length; i++)
+ {
+ var b1 = bs1[i];
+ var b2 = bs2[i];
+ if (b1.tok.pos < b2.tok.pos)
+ {
+ return -1;
+ }
+ else if (b2.tok.pos < b1.tok.pos)
+ {
+ return 1;
+ }
+ }
+
+ return 0;
+ }
+
public int Compare(Counterexample c1, Counterexample c2)
{
//Contract.Requires(c1 != null);
//Contract.Requires(c2 != null);
if (c1.GetLocation() == c2.GetLocation())
{
+ var c = Compare(c1.Trace, c2.Trace);
+ if (c != 0)
+ {
+ return c;
+ }
// TODO(wuestholz): Generalize this to compare all IPotentialErrorNodes of the counterexample.
var a1 = c1 as AssertCounterexample;
var a2 = c2 as AssertCounterexample;
diff --git a/Test/prover/Answer b/Test/prover/Answer index 1ca6407c..13621984 100644 --- a/Test/prover/Answer +++ b/Test/prover/Answer @@ -4,7 +4,7 @@ z3mutl.bpl(20,5): Error BP5001: This assertion might not hold.
Execution trace:
z3mutl.bpl(5,1): start
- z3mutl.bpl(14,1): L3
+ z3mutl.bpl(8,1): L1
z3mutl.bpl(20,1): L5
z3mutl.bpl(20,5): Error BP5001: This assertion might not hold.
Execution trace:
@@ -14,7 +14,7 @@ Execution trace: z3mutl.bpl(20,5): Error BP5001: This assertion might not hold.
Execution trace:
z3mutl.bpl(5,1): start
- z3mutl.bpl(8,1): L1
+ z3mutl.bpl(14,1): L3
z3mutl.bpl(20,1): L5
Boogie program verifier finished with 0 verified, 3 errors
|