diff options
| author |  Rustan Leino <unknown> | 2015-10-02 15:26:56 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2015-10-02 15:26:56 -0700 |
| commit | 1885f7d7d1fb9bd6ceb8220450dbb5d890501337 (patch) | |
| tree | d85a7c88c668f883aadda5bb5412fe15f3bd5102 /Test/dafny0/CoinductiveProofs.dfy.expect | |
| parent | c5a1c58d3c89c55c31331cb419cd3c06e276b5dd (diff) | |
Hover text includes #[_k-1] suffix for terms rewritten in prefix predicates/lemmas (this fixes an item from the wishlist).
Include in hover text the extreme predicates for which an extreme lemmas has been rewritten (but don't include ==# in this list--or should it perhaps be included?).
Under a (temporary) switch /rewriteFocalPredicates, each use of a focal predicate P in a prefix lemma is rewritten into P#[_k-1].
Diffstat (limited to 'Test/dafny0/CoinductiveProofs.dfy.expect')
| -rw-r--r-- | Test/dafny0/CoinductiveProofs.dfy.expect | 65 |
1 files changed, 46 insertions, 19 deletions
diff --git a/Test/dafny0/CoinductiveProofs.dfy.expect b/Test/dafny0/CoinductiveProofs.dfy.expect index 2a5a2b0b..c4f4c405 100644 --- a/Test/dafny0/CoinductiveProofs.dfy.expect +++ b/Test/dafny0/CoinductiveProofs.dfy.expect @@ -1,50 +1,77 @@ -CoinductiveProofs.dfy(29,11): Error: assertion violation
+CoinductiveProofs.dfy(30,11): Error: assertion violation
+CoinductiveProofs.dfy(15,36): Related location
CoinductiveProofs.dfy(13,16): Related location
Execution trace:
(0,0): anon0
(0,0): anon5_Then
(0,0): anon6_Then
-CoinductiveProofs.dfy(59,0): Error BP5003: A postcondition might not hold on this return path.
-CoinductiveProofs.dfy(58,10): Related location: This is the postcondition that might not hold.
-CoinductiveProofs.dfy(54,2): Related location
+CoinductiveProofs.dfy(44,11): Error: assertion violation
+CoinductiveProofs.dfy(13,16): Related location
+Execution trace:
+ (0,0): anon0
+ (0,0): anon13_Then
+ (0,0): anon16_Then
+CoinductiveProofs.dfy(48,11): Error: assertion violation
+CoinductiveProofs.dfy(13,16): Related location
+Execution trace:
+ (0,0): anon0
+ (0,0): anon13_Then
+ (0,0): anon18_Then
+CoinductiveProofs.dfy(78,0): Error BP5003: A postcondition might not hold on this return path.
+CoinductiveProofs.dfy(77,10): Related location: This is the postcondition that might not hold.
+CoinductiveProofs.dfy(73,2): Related location
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-CoinductiveProofs.dfy(74,11): Error: assertion violation
-CoinductiveProofs.dfy(54,2): Related location
+CoinductiveProofs.dfy(94,11): Error: assertion violation
+CoinductiveProofs.dfy(87,29): Related location
+CoinductiveProofs.dfy(73,2): Related location
Execution trace:
(0,0): anon0
(0,0): anon5_Then
(0,0): anon6_Then
-CoinductiveProofs.dfy(91,0): Error BP5003: A postcondition might not hold on this return path.
-CoinductiveProofs.dfy(90,10): Related location: This is the postcondition that might not hold.
-CoinductiveProofs.dfy(80,2): Related location
+CoinductiveProofs.dfy(127,0): Error BP5003: A postcondition might not hold on this return path.
+CoinductiveProofs.dfy(126,10): Related location: This is the postcondition that might not hold.
+CoinductiveProofs.dfy(115,2): Related location
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-CoinductiveProofs.dfy(100,11): Error: assertion violation
-CoinductiveProofs.dfy(80,2): Related location
+CoinductiveProofs.dfy(136,11): Error: assertion violation
+CoinductiveProofs.dfy(117,29): Related location
+CoinductiveProofs.dfy(115,2): Related location
Execution trace:
(0,0): anon0
(0,0): anon5_Then
(0,0): anon6_Then
-CoinductiveProofs.dfy(111,0): Error BP5003: A postcondition might not hold on this return path.
-CoinductiveProofs.dfy(110,10): Related location: This is the postcondition that might not hold.
-CoinductiveProofs.dfy(106,2): Related location
+CoinductiveProofs.dfy(149,11): Error: assertion violation
+CoinductiveProofs.dfy(115,2): Related location
+Execution trace:
+ (0,0): anon0
+ (0,0): anon13_Then
+ (0,0): anon16_Then
+CoinductiveProofs.dfy(153,11): Error: assertion violation
+CoinductiveProofs.dfy(115,2): Related location
+Execution trace:
+ (0,0): anon0
+ (0,0): anon13_Then
+ (0,0): anon18_Then
+CoinductiveProofs.dfy(164,0): Error BP5003: A postcondition might not hold on this return path.
+CoinductiveProofs.dfy(163,10): Related location: This is the postcondition that might not hold.
+CoinductiveProofs.dfy(159,2): Related location
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-CoinductiveProofs.dfy(150,0): Error BP5003: A postcondition might not hold on this return path.
-CoinductiveProofs.dfy(149,21): Related location: This is the postcondition that might not hold.
+CoinductiveProofs.dfy(203,0): Error BP5003: A postcondition might not hold on this return path.
+CoinductiveProofs.dfy(202,21): Related location: This is the postcondition that might not hold.
CoinductiveProofs.dfy(4,23): Related location
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-CoinductiveProofs.dfy(156,0): Error BP5003: A postcondition might not hold on this return path.
-CoinductiveProofs.dfy(155,21): Related location: This is the postcondition that might not hold.
+CoinductiveProofs.dfy(209,0): Error BP5003: A postcondition might not hold on this return path.
+CoinductiveProofs.dfy(208,21): Related location: This is the postcondition that might not hold.
CoinductiveProofs.dfy(4,23): Related location
Execution trace:
(0,0): anon0
(0,0): anon3_Then
-Dafny program verifier finished with 35 verified, 8 errors
+Dafny program verifier finished with 42 verified, 12 errors
|