diff options
| author |  leino <unknown> | 2015-09-20 21:51:42 -0700 |
|---|---|---|
| committer | leino <unknown> | 2015-09-20 21:51:42 -0700 |
| commit | 800885b4d7d0164803c0c2f117b78c65479283f9 (patch) | |
| tree | d5ffd8318ffeed8fa300a9e872461f38455c28ed /Test/dafny0/TypeTests.dfy.expect | |
| parent | b9319e38746bc6a2043cb7c979c4ccd4b175b86c (diff) | |
Preliminary refactoring of ghost-statement computations to after type checking
Diffstat (limited to 'Test/dafny0/TypeTests.dfy.expect')
| -rw-r--r-- | Test/dafny0/TypeTests.dfy.expect | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/dafny0/TypeTests.dfy.expect b/Test/dafny0/TypeTests.dfy.expect index 500b1af9..8206fd43 100644 --- a/Test/dafny0/TypeTests.dfy.expect +++ b/Test/dafny0/TypeTests.dfy.expect @@ -56,7 +56,7 @@ TypeTests.dfy(151,13): Error: sorry, cannot instantiate type parameter with a su TypeTests.dfy(152,2): Error: sorry, cannot instantiate type parameter with a subrange type
TypeTests.dfy(153,16): Error: sorry, cannot instantiate type parameter with a subrange type
TypeTests.dfy(154,14): Error: sorry, cannot instantiate type parameter with a subrange type
-TypeTests.dfy(177,15): Error: ghost variables are allowed only in specification contexts
+TypeTests.dfy(177,5): Error: non-ghost variable cannot be assigned a value that depends on a ghost
TypeTests.dfy(187,4): Error: cannot assign to non-ghost variable in a ghost context
TypeTests.dfy(188,7): Error: cannot assign to non-ghost variable in a ghost context
TypeTests.dfy(21,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed
|