diff options
| author |  leino <unknown> | 2014-08-05 10:06:39 -0700 |
|---|---|---|
| committer | leino <unknown> | 2014-08-05 10:06:39 -0700 |
| commit | 498bff41addc9ca481926f668fb6b69b17b9deda (patch) | |
| tree | 7294a111a6b5ef3a11f0a864cebe5cfbb919630f /Test/dafny0/Trait | |
| parent | e17ec43d4f53d179c367b5c6bb52c893e0f57bff (diff) | |
Resolved further merge issues
Diffstat (limited to 'Test/dafny0/Trait')
| -rw-r--r-- | Test/dafny0/Trait/TraitBasix.dfy.expect | 4 | ||||
| -rw-r--r-- | Test/dafny0/Trait/TraitMultiModule.dfy.expect | 2 | ||||
| -rw-r--r-- | Test/dafny0/Trait/TraitOverride0.dfy.expect | 2 | ||||
| -rw-r--r-- | Test/dafny0/Trait/TraitOverride1.dfy.expect | 2 | ||||
| -rw-r--r-- | Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect | 2 |
5 files changed, 6 insertions, 6 deletions
diff --git a/Test/dafny0/Trait/TraitBasix.dfy.expect b/Test/dafny0/Trait/TraitBasix.dfy.expect index 1d44d0f6..4a908ee7 100644 --- a/Test/dafny0/Trait/TraitBasix.dfy.expect +++ b/Test/dafny0/Trait/TraitBasix.dfy.expect @@ -1,7 +1,7 @@ +TraitBasix.dfy(91,23): Error: unresolved identifier: IX
TraitBasix.dfy(77,13): Error: member in the class has been already inherited from its parent trait
TraitBasix.dfy(70,7): Error: class: I0Child does not implement trait member: Customizable
TraitBasix.dfy(80,7): Error: class: I0Child2 does not implement trait member: F
-TraitBasix.dfy(91,7): Error: unresolved identifier: IX
TraitBasix.dfy(98,6): Error: a trait is not allowed to declare a constructor
-TraitBasix.dfy(117,10): Error: new can not be applied to a trait
+TraitBasix.dfy(117,10): Error: new cannot be applied to a trait
6 resolution/type errors detected in TraitBasix.dfy
diff --git a/Test/dafny0/Trait/TraitMultiModule.dfy.expect b/Test/dafny0/Trait/TraitMultiModule.dfy.expect index 589fba07..b9031dac 100644 --- a/Test/dafny0/Trait/TraitMultiModule.dfy.expect +++ b/Test/dafny0/Trait/TraitMultiModule.dfy.expect @@ -1,2 +1,2 @@ -TraitMultiModule.dfy(21,9): Error: class M2.C2 is in a different module than trait M1.T1. A class may only extend a trait in the same module
+TraitMultiModule.dfy(21,20): Error: class M2.C2 is in a different module than trait M1.T1. A class may only extend a trait in the same module
1 resolution/type errors detected in TraitMultiModule.dfy
diff --git a/Test/dafny0/Trait/TraitOverride0.dfy.expect b/Test/dafny0/Trait/TraitOverride0.dfy.expect index 4020b880..1e7bface 100644 --- a/Test/dafny0/Trait/TraitOverride0.dfy.expect +++ b/Test/dafny0/Trait/TraitOverride0.dfy.expect @@ -1,4 +1,4 @@ -TraitOverride0.dfy(53,20): Error: a class can not override implemented functions
+TraitOverride0.dfy(53,20): Error: a class cannot override implemented functions
TraitOverride0.dfy(48,20): Error: function 'BodyLess1' is declared with a different number of parameter (1 instead of 0) than the corresponding function in the module it overrides
TraitOverride0.dfy(65,6): Error: class: C2 does not implement trait member: BodyLess1
TraitOverride0.dfy(65,6): Error: class: C2 does not implement trait member: BodyLess2
diff --git a/Test/dafny0/Trait/TraitOverride1.dfy.expect b/Test/dafny0/Trait/TraitOverride1.dfy.expect index 0f7b49e3..c90560b0 100644 --- a/Test/dafny0/Trait/TraitOverride1.dfy.expect +++ b/Test/dafny0/Trait/TraitOverride1.dfy.expect @@ -1,2 +1,2 @@ -Dafny program verifier finished with 62 verified, 0 errors
+Dafny program verifier finished with 52 verified, 0 errors
diff --git a/Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect b/Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect index 6849499c..b59d7b80 100644 --- a/Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect +++ b/Test/dafny0/Trait/TraitUsingParentMembers.dfy.expect @@ -5,4 +5,4 @@ Execution trace: (0,0): anon2
(0,0): anon6_Then
-Dafny program verifier finished with 9 verified, 1 error
+Dafny program verifier finished with 7 verified, 1 error
|