Merge

3 files changed, 16 insertions, 16 deletions

diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 58ba6701..8dceb6ba 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -459,7 +459,7 @@ module MyOwnModule {
   

 // ------------------- nameless constructors ------------------------------

 

-class YHWH {

+class Y {

   var data: int;

   constructor (x: int)

     modifies this;

@@ -470,22 +470,22 @@ class YHWH {
   {

   }

   method Test() {

-    var IAmWhoIAm := new YHWH(5);

-    IAmWhoIAm := new YHWH._ctor(7);  // but, in fact, it is also possible to use the underlying name

-    IAmWhoIAm := new YHWH;  // error: the class has a constructor, so one must be used

-    var s := new Lucifer.Init(5);

-    s := new Lucifer.FromArray(null);

-    s := new Lucifer(false);

-    s := new Lucifer._ctor(false);

-    s := new Lucifer.M();  // error: there is a constructor, so one must be called

-    s := new Lucifer;  // error: there is a constructor, so one must be called

+    var i := new Y(5);

+    i := new Y._ctor(7);  // but, in fact, it is also possible to use the underlying name

+    i := new Y;  // error: the class has a constructor, so one must be used

+    var s := new Luci.Init(5);

+    s := new Luci.FromArray(null);

+    s := new Luci(false);

+    s := new Luci._ctor(false);

+    s := new Luci.M();  // error: there is a constructor, so one must be called

+    s := new Luci;  // error: there is a constructor, so one must be called

     var l := new Lamb;

     l := new Lamb();  // error: there is no default constructor

     l := new Lamb.Gwen();

   }

 }

 

-class Lucifer {

+class Luci {

   constructor Init(y: int) { }

   constructor (nameless: bool) { }

   constructor FromArray(a: array<int>) { }

@@ -493,7 +493,7 @@ class Lucifer {
 }

 

 class Lamb {

-  method Jesus() { }

+  method Jess() { }

   method Gwen() { }

 }

 

diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
index b055184f..d1d826f4 100644
--- a/Test/dafny0/ResolutionErrors.dfy.expect
+++ b/Test/dafny0/ResolutionErrors.dfy.expect
@@ -173,9 +173,9 @@ ResolutionErrors.dfy(92,14): Error: the name 'David' denotes a datatype construc
 ResolutionErrors.dfy(93,14): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')

 ResolutionErrors.dfy(95,14): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')

 ResolutionErrors.dfy(97,18): Error: wrong number of arguments to datatype constructor David (found 2, expected 1)

-ResolutionErrors.dfy(475,14): Error: when allocating an object of type 'YHWH', one of its constructor methods must be called

-ResolutionErrors.dfy(480,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called

-ResolutionErrors.dfy(481,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called

+ResolutionErrors.dfy(475,6): Error: when allocating an object of type 'Y', one of its constructor methods must be called

+ResolutionErrors.dfy(480,6): Error: when allocating an object of type 'Luci', one of its constructor methods must be called

+ResolutionErrors.dfy(481,6): Error: when allocating an object of type 'Luci', one of its constructor methods must be called

 ResolutionErrors.dfy(483,9): Error: class Lamb does not have an anonymous constructor

 ResolutionErrors.dfy(853,11): Error: a modifies-clause expression must denote an object or a collection of objects (instead got int)

 ResolutionErrors.dfy(857,14): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)

diff --git a/Test/triggers/some-proofs-only-work-without-autoTriggers.dfy b/Test/triggers/some-proofs-only-work-without-autoTriggers.dfy
index 98cea392..bc2e0934 100644
--- a/Test/triggers/some-proofs-only-work-without-autoTriggers.dfy
+++ b/Test/triggers/some-proofs-only-work-without-autoTriggers.dfy
@@ -1,7 +1,7 @@
 // RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"

 // RUN: %diff "%s.expect" "%t"

 

-// The examples below work nicely with /autoTriggers:0, but break when we ass

+// The examples below work nicely with /autoTriggers:0, but break when we use

 // /autoTriggers.

 

 // The issue is that the axioms for sequences are missing a number of facts,