summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
Diffstat (limited to 'Test')
-rw-r--r--Test/dafny0/ResolutionErrors.dfy24
-rw-r--r--Test/dafny0/ResolutionErrors.dfy.expect6
-rw-r--r--Test/triggers/some-proofs-only-work-without-autoTriggers.dfy2
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,