diff options
| author |  leino <unknown> | 2014-10-13 18:31:22 -0700 |
|---|---|---|
| committer | leino <unknown> | 2014-10-13 18:31:22 -0700 |
| commit | 25491156486a9e1a1642278f40ea6e9378c72da7 (patch) | |
| tree | 98f55cbdd7922f24a9ecb121ece57fddfbbfdbbc /Test/dafny0/Basics.dfy.expect | |
| parent | 969ef55e0c579e0538eff680f8bbf1b289777500 (diff) | |
Some more test cases for associativity and short-circuitness of <==
Diffstat (limited to 'Test/dafny0/Basics.dfy.expect')
| -rw-r--r-- | Test/dafny0/Basics.dfy.expect | 76 |
1 files changed, 63 insertions, 13 deletions
diff --git a/Test/dafny0/Basics.dfy.expect b/Test/dafny0/Basics.dfy.expect index 5fccdb36..db074f4a 100644 --- a/Test/dafny0/Basics.dfy.expect +++ b/Test/dafny0/Basics.dfy.expect @@ -12,11 +12,61 @@ Execution trace: Basics.dfy(69,82): anon17_Else
Basics.dfy(69,95): anon18_Else
(0,0): anon12
-Basics.dfy(113,16): Error: assertion violation
+Basics.dfy(93,14): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ Basics.dfy(83,14): anon27_Else
+ (0,0): anon2
+ Basics.dfy(84,14): anon28_Else
+ (0,0): anon4
+ (0,0): anon29_Then
+ Basics.dfy(89,12): anon30_Else
+ (0,0): anon8
+ Basics.dfy(90,12): anon32_Else
+ (0,0): anon11
+ Basics.dfy(91,13): anon34_Else
+ (0,0): anon35_Then
+ (0,0): anon15
+Basics.dfy(99,14): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ Basics.dfy(83,14): anon27_Else
+ (0,0): anon2
+ Basics.dfy(84,14): anon28_Else
+ (0,0): anon4
+ (0,0): anon29_Else
+ Basics.dfy(95,18): anon36_Else
+ (0,0): anon19
+ Basics.dfy(96,20): anon38_Else
+ (0,0): anon22
+ Basics.dfy(97,19): anon40_Else
+ (0,0): anon41_Then
+ (0,0): anon26
+Basics.dfy(112,28): Error: target object may be null
+Execution trace:
+ (0,0): anon0
+ Basics.dfy(105,20): anon13_Else
+ (0,0): anon2
+ Basics.dfy(106,20): anon14_Else
+ (0,0): anon4
+ Basics.dfy(107,24): anon15_Else
+ (0,0): anon6
+ (0,0): anon16_Then
+Basics.dfy(114,14): Error: target object may be null
+Execution trace:
+ (0,0): anon0
+ Basics.dfy(105,20): anon13_Else
+ (0,0): anon2
+ Basics.dfy(106,20): anon14_Else
+ (0,0): anon4
+ Basics.dfy(107,24): anon15_Else
+ (0,0): anon6
+ (0,0): anon16_Else
+Basics.dfy(149,16): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon10_Then
-Basics.dfy(132,10): Error: when left-hand sides 0 and 1 may refer to the same location, they must be assigned the same value
+Basics.dfy(168,10): Error: when left-hand sides 0 and 1 may refer to the same location, they must be assigned the same value
Execution trace:
(0,0): anon0
(0,0): anon10_Then
@@ -25,28 +75,28 @@ Execution trace: (0,0): anon6
(0,0): anon12_Then
(0,0): anon9
-Basics.dfy(146,10): Error: when left-hand sides 0 and 1 refer to the same location, they must be assigned the same value
+Basics.dfy(182,10): Error: when left-hand sides 0 and 1 refer to the same location, they must be assigned the same value
Execution trace:
(0,0): anon0
-Basics.dfy(158,19): Error: assertion violation
+Basics.dfy(194,19): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon11_Then
-Basics.dfy(160,10): Error: assignment may update an object not in the enclosing context's modifies clause
+Basics.dfy(196,10): Error: assignment may update an object not in the enclosing context's modifies clause
Execution trace:
(0,0): anon0
(0,0): anon3
-Basics.dfy(160,10): Error: target object may be null
+Basics.dfy(196,10): Error: target object may be null
Execution trace:
(0,0): anon0
(0,0): anon3
-Basics.dfy(165,12): Error: left-hand sides 0 and 1 may refer to the same location
+Basics.dfy(201,12): Error: left-hand sides 0 and 1 may refer to the same location
Execution trace:
(0,0): anon0
(0,0): anon11_Then
(0,0): anon3
(0,0): anon12_Then
-Basics.dfy(176,15): Error: assertion violation
+Basics.dfy(212,15): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon11_Then
@@ -56,22 +106,22 @@ Execution trace: (0,0): anon13_Then
(0,0): anon8
(0,0): anon14_Then
-Basics.dfy(238,10): Error: when left-hand sides 0 and 1 refer to the same location, they must be assigned the same value
+Basics.dfy(274,10): Error: when left-hand sides 0 and 1 refer to the same location, they must be assigned the same value
Execution trace:
(0,0): anon0
-Basics.dfy(429,12): Error: assertion violation
+Basics.dfy(465,12): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon4_Then
(0,0): anon3
-Basics.dfy(440,19): Error: assertion violation
+Basics.dfy(476,19): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon4_Else
-Basics.dfy(442,12): Error: assertion violation
+Basics.dfy(478,12): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon4_Then
(0,0): anon3
-Dafny program verifier finished with 61 verified, 14 errors
+Dafny program verifier finished with 63 verified, 18 errors
|