diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-05-31 00:08:09 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-05-31 00:08:09 -0700 |
| commit | 6f5ce54e615d395f55db2d358cd54ff2ce8f2782 (patch) | |
| tree | ffd75d7f9657f5ba24c649062f4c494abbfc8ad9 /Test/dafny0/Answer | |
| parent | bcc2de7ff9390509b1087c47d8b5e825ca9df3c1 (diff) | |
Dafny: translate call statements with fancy LHSs
Diffstat (limited to 'Test/dafny0/Answer')
| -rw-r--r-- | Test/dafny0/Answer | 38 |
1 files changed, 33 insertions, 5 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 75025b2f..2edd1c51 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -598,18 +598,18 @@ Execution trace: (0,0): anon10
Basics.dfy(66,95): anon18_Else
(0,0): anon12
-Basics.dfy(86,16): Error: assertion violation
+Basics.dfy(100,16): Error: assertion violation
Execution trace:
(0,0): anon0
(0,0): anon10_Then
-Basics.dfy(99,12): Error: left-hand sides 0 and 1 may refer to the same location
+Basics.dfy(113,12): Error: left-hand sides 0 and 1 may refer to the same location
Execution trace:
(0,0): anon0
(0,0): anon3
(0,0): anon11_Else
(0,0): anon6
(0,0): anon12_Then
-Basics.dfy(105,10): Error: left-hand sides 0 and 1 may refer to the same location
+Basics.dfy(119,10): Error: left-hand sides 0 and 1 may refer to the same location
Execution trace:
(0,0): anon0
(0,0): anon10_Then
@@ -618,11 +618,39 @@ Execution trace: (0,0): anon6
(0,0): anon12_Then
(0,0): anon9
-Basics.dfy(119,10): Error: left-hand sides 0 and 1 may refer to the same location
+Basics.dfy(133,10): Error: left-hand sides 0 and 1 may refer to the same location
+Execution trace:
+ (0,0): anon0
+Basics.dfy(145,19): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon11_Then
+Basics.dfy(147,10): Error: target object may be null
+Execution trace:
+ (0,0): anon0
+ (0,0): anon3
+Basics.dfy(147,10): Error: assignment may update an object not in the enclosing method's modifies clause
+Execution trace:
+ (0,0): anon0
+ (0,0): anon3
+Basics.dfy(152,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(163,15): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ (0,0): anon11_Then
+ (0,0): anon3
+ (0,0): anon12_Else
+ (0,0): anon6
+ (0,0): anon13_Then
+ (0,0): anon8
+ (0,0): anon14_Then
-Dafny program verifier finished with 9 verified, 6 errors
+Dafny program verifier finished with 16 verified, 11 errors
-------------------- ControlStructures.dfy --------------------
ControlStructures.dfy(5,3): Error: missing case in case statement: Blue
|