Resolved further merge issues

7 files changed, 18 insertions, 7 deletions

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index aaf1291c..9f6c948a 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -1090,3 +1090,13 @@ module OpaqueTypes1 {
     assert p != q;  // error: types must be the same in order to do compare

   }

 }

+

+// ----- new trait -------------------------------------------

+

+

+trait J { }

+type JJ = J

+method TraitSynonym()

+{

+  var x := new JJ;  // error: new cannot be applied to a trait

+}

diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
index d5d12eb9..b11fa9f8 100644
--- a/Test/dafny0/ResolutionErrors.dfy.expect
+++ b/Test/dafny0/ResolutionErrors.dfy.expect
@@ -172,4 +172,5 @@ ResolutionErrors.dfy(956,10): Error: second argument to % must be of type int (i
 ResolutionErrors.dfy(960,7): Error: type conversion to real is allowed only from int (got real)

 ResolutionErrors.dfy(961,7): Error: type conversion to int is allowed only from real (got int)

 ResolutionErrors.dfy(962,7): Error: type conversion to int is allowed only from real (got nat)

-174 resolution/type errors detected in ResolutionErrors.dfy

+ResolutionErrors.dfy(1101,8): Error: new cannot be applied to a trait

+175 resolution/type errors detected in ResolutionErrors.dfy

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