summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
Diffstat (limited to 'Test')
-rw-r--r--Test/dafny0/Answer136
-rw-r--r--Test/dafny0/ControlStructures.dfy105
-rw-r--r--Test/dafny0/ResolutionErrors.dfy167
-rw-r--r--Test/dafny1/Substitution.dfy2
4 files changed, 406 insertions, 4 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index efcfa8bb..d997cba1 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -403,6 +403,22 @@ Dafny program verifier finished with 3 verified, 3 errors
-------------------- ResolutionErrors.dfy --------------------
ResolutionErrors.dfy(39,13): Error: 'this' is not allowed in a 'static' context
+ResolutionErrors.dfy(100,9): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(101,9): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')
+ResolutionErrors.dfy(105,11): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(106,9): Error: actual out-parameter 0 is required to be a ghost variable
+ResolutionErrors.dfy(113,15): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(117,23): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(124,4): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(128,21): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(129,35): Error: ghost variables are allowed only in specification contexts
+ResolutionErrors.dfy(138,9): Error: only ghost methods can be called from this context
+ResolutionErrors.dfy(144,16): Error: 'decreases *' is not allowed on ghost loops
+ResolutionErrors.dfy(185,27): Error: ghost-context break statement is not allowed to break out of non-ghost structure
+ResolutionErrors.dfy(208,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
+ResolutionErrors.dfy(220,12): Error: trying to break out of more loop levels than there are enclosing loops
+ResolutionErrors.dfy(224,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop
+ResolutionErrors.dfy(229,8): Error: return statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)
ResolutionErrors.dfy(10,16): Error: 'decreases *' is not allowed on ghost loops
ResolutionErrors.dfy(22,11): Error: array selection requires an array2 (got array3<T>)
ResolutionErrors.dfy(23,12): Error: sequence/array selection requires a sequence or array (got array3<T>)
@@ -422,7 +438,9 @@ ResolutionErrors.dfy(80,12): Error: the name 'David' denotes a datatype construc
ResolutionErrors.dfy(81,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
ResolutionErrors.dfy(83,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')
ResolutionErrors.dfy(85,12): Error: wrong number of arguments to datatype constructor Abc (found 2, expected 1)
-20 resolution/type errors detected in ResolutionErrors.dfy
+ResolutionErrors.dfy(247,4): Error: label shadows an enclosing label
+ResolutionErrors.dfy(252,2): Error: duplicate label
+38 resolution/type errors detected in ResolutionErrors.dfy
-------------------- Array.dfy --------------------
Array.dfy(10,12): Error: assignment may update an array element not in the enclosing method's modifies clause
@@ -597,8 +615,120 @@ ControlStructures.dfy(72,3): Error: alternative cases fail to cover all possibil
Execution trace:
(0,0): anon0
(0,0): anon5_Else
-
-Dafny program verifier finished with 15 verified, 6 errors
+ControlStructures.dfy(218,18): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ ControlStructures.dfy(197,3): anon62_LoopHead
+ (0,0): anon62_LoopBody
+ ControlStructures.dfy(197,3): anon63_Else
+ (0,0): anon3
+ ControlStructures.dfy(197,3): anon64_Else
+ (0,0): anon5
+ ControlStructures.dfy(201,5): anon65_LoopHead
+ (0,0): anon65_LoopBody
+ ControlStructures.dfy(201,5): anon66_Else
+ (0,0): anon8
+ ControlStructures.dfy(201,5): anon67_Else
+ (0,0): anon10
+ (0,0): anon71_Then
+ ControlStructures.dfy(213,9): anon72_LoopHead
+ (0,0): anon72_LoopBody
+ ControlStructures.dfy(213,9): anon73_Else
+ (0,0): anon20
+ (0,0): anon74_Then
+ (0,0): anon29
+ControlStructures.dfy(235,21): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ ControlStructures.dfy(197,3): anon62_LoopHead
+ (0,0): anon62_LoopBody
+ ControlStructures.dfy(197,3): anon63_Else
+ (0,0): anon3
+ ControlStructures.dfy(197,3): anon64_Else
+ (0,0): anon5
+ ControlStructures.dfy(201,5): anon65_LoopHead
+ (0,0): anon65_LoopBody
+ ControlStructures.dfy(201,5): anon66_Else
+ (0,0): anon8
+ ControlStructures.dfy(201,5): anon67_Else
+ (0,0): anon10
+ (0,0): anon71_Then
+ ControlStructures.dfy(213,9): anon72_LoopHead
+ (0,0): anon72_LoopBody
+ ControlStructures.dfy(213,9): anon73_Else
+ (0,0): anon20
+ ControlStructures.dfy(213,9): anon74_Else
+ (0,0): anon22
+ (0,0): anon75_Then
+ (0,0): after_4
+ ControlStructures.dfy(224,7): anon77_LoopHead
+ (0,0): anon77_LoopBody
+ ControlStructures.dfy(224,7): anon78_Else
+ (0,0): anon33
+ ControlStructures.dfy(224,7): anon79_Else
+ (0,0): anon35
+ (0,0): anon81_Then
+ (0,0): anon38
+ (0,0): after_9
+ (0,0): anon86_Then
+ (0,0): anon53
+ControlStructures.dfy(238,30): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ ControlStructures.dfy(197,3): anon62_LoopHead
+ (0,0): anon62_LoopBody
+ ControlStructures.dfy(197,3): anon63_Else
+ (0,0): anon3
+ ControlStructures.dfy(197,3): anon64_Else
+ (0,0): anon5
+ ControlStructures.dfy(201,5): anon65_LoopHead
+ (0,0): anon65_LoopBody
+ ControlStructures.dfy(201,5): anon66_Else
+ (0,0): anon8
+ ControlStructures.dfy(201,5): anon67_Else
+ (0,0): anon10
+ (0,0): anon68_Then
+ (0,0): after_5
+ (0,0): anon87_Then
+ (0,0): anon88_Then
+ (0,0): anon58
+ControlStructures.dfy(241,17): Error: assertion violation
+Execution trace:
+ (0,0): anon0
+ ControlStructures.dfy(197,3): anon62_LoopHead
+ (0,0): anon62_LoopBody
+ ControlStructures.dfy(197,3): anon63_Else
+ (0,0): anon3
+ ControlStructures.dfy(197,3): anon64_Else
+ (0,0): anon5
+ ControlStructures.dfy(201,5): anon65_LoopHead
+ (0,0): anon65_LoopBody
+ ControlStructures.dfy(201,5): anon66_Else
+ (0,0): anon8
+ ControlStructures.dfy(201,5): anon67_Else
+ (0,0): anon10
+ (0,0): anon71_Then
+ ControlStructures.dfy(213,9): anon72_LoopHead
+ (0,0): anon72_LoopBody
+ ControlStructures.dfy(213,9): anon73_Else
+ (0,0): anon20
+ ControlStructures.dfy(213,9): anon74_Else
+ (0,0): anon22
+ (0,0): anon75_Then
+ (0,0): after_4
+ ControlStructures.dfy(224,7): anon77_LoopHead
+ (0,0): anon77_LoopBody
+ ControlStructures.dfy(224,7): anon78_Else
+ (0,0): anon33
+ ControlStructures.dfy(224,7): anon79_Else
+ (0,0): anon35
+ (0,0): anon82_Then
+ (0,0): anon85_Then
+ (0,0): after_8
+ (0,0): anon89_Then
+ (0,0): anon61
+
+Dafny program verifier finished with 18 verified, 10 errors
-------------------- Termination.dfy --------------------
Termination.dfy(103,3): Error: cannot prove termination; try supplying a decreases clause for the loop
diff --git a/Test/dafny0/ControlStructures.dfy b/Test/dafny0/ControlStructures.dfy
index 2c9b3a35..5012e003 100644
--- a/Test/dafny0/ControlStructures.dfy
+++ b/Test/dafny0/ControlStructures.dfy
@@ -135,3 +135,108 @@ method B(x: int) returns (r: int)
r := r - 1;
}
}
+
+// --------------- breaks ---------------
+
+method TheBreaker_AllGood(M: int, N: int, O: int)
+{
+ var a, b, c, d, e;
+ var i := 0;
+ while (i < M)
+ {
+ var j := 0;
+ label InnerHasLabel:
+ while (j < N)
+ {
+ var u := 2000;
+ label MyLabelBlock:
+ label MyLabelBlockAgain:
+ if (*) {
+ a := 15; break;
+ } else if (*) {
+ b := 12; break break;
+ } else if (*) {
+ c := 21; break InnerHasLabel;
+ } else if (*) {
+ while (u < 10000) {
+ u := u + 3;
+ if (*) { u := 1998; break MyLabelBlock; }
+ if (*) { u := 1998; break MyLabelBlockAgain; }
+ }
+ assert 10000 <= u;
+ u := 1998;
+ } else {
+ u := u - 2;
+ }
+ assert u == 1998;
+ var k := 0;
+ while
+ decreases O - k;
+ {
+ case k < O && k % 2 == 0 =>
+ d := 187; break;
+ case k < O =>
+ if (*) { e := 4; break InnerHasLabel; }
+ if (*) { e := 7; break; }
+ if (*) { e := 37; break break break; }
+ k := k + 1;
+ }
+ assert O <= k || d == 187 || e == 7;
+ j := j + 1;
+ }
+ assert N <= j || a == 15 || c == 21 || e == 4;
+ i := i + 1;
+ }
+ assert M <= i || b == 12 || e == 37;
+}
+
+method TheBreaker_SomeBad(M: int, N: int, O: int)
+{
+ var a, b, c, d, e;
+ var i := 0;
+ while (i < M)
+ {
+ var j := 0;
+ label InnerHasLabel:
+ while (j < N)
+ {
+ var u := 2000;
+ label MyLabelBlock:
+ label MyLabelBlockAgain:
+ if (*) {
+ a := 15; break;
+ } else if (*) {
+ b := 12; break break;
+ } else if (*) {
+ c := 21; break InnerHasLabel;
+ } else if (*) {
+ while (u < 10000) {
+ u := u + 3;
+ if (*) { u := 1998; break MyLabelBlock; }
+ if (*) { u := 1998; break MyLabelBlockAgain; }
+ }
+ assert u < 2000; // error (and no way to get past this assert statement)
+ } else {
+ u := u - 2;
+ }
+ assert u == 1998;
+ var k := 0;
+ while
+ decreases O - k;
+ {
+ case k < O && k % 2 == 0 =>
+ d := 187; break;
+ case k < O =>
+ if (*) { e := 4; break InnerHasLabel; }
+ if (*) { e := 7; break; }
+ if (*) { e := 37; break break break; }
+ k := k + 1;
+ }
+ assert O <= k || e == 7; // error: d == 187
+ j := j + 1;
+ }
+ assert N <= j || c == 21 || e == 4; // error: a == 15
+ i := i + 1;
+ }
+ assert M <= i || b == 12; // error: e == 37
+}
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index 56d7575f..09307b2b 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -87,3 +87,170 @@ method TestNameResolution1() {
var e := Eleanor;
assert Tuv(e, this.Eleanor) == 10;
}
+
+// --------------- ghost tests -------------------------------------
+
+datatype GhostDt =
+ Nil(ghost extraInfo: int) |
+ Cons(data: int, tail: GhostDt, ghost moreInfo: int);
+
+class GhostTests {
+ method M(dt: GhostDt) returns (r: int) {
+ ghost var g := 5;
+ r := g; // error: RHS is ghost, LHS is not
+ r := F(18, g); // error: RHS is a ghost and will not be available at run time
+ r := G(20, g); // it's fine to pass a ghost as a parameter to a non-ghost, because
+ // only the ghost goes away during compilation
+ r := N(22, g); // ditto
+ r := N(g, 22); // error: passing in 'g' as non-ghost parameter
+ r := P(24, 22); // error: 'P' is ghost, but its result is assigned to a non-ghost
+
+ match (dt) {
+ case Nil(gg) =>
+ case Cons(dd, tt, gg) =>
+ r := G(dd, dd); // fine
+ r := G(dd, gg); // fine
+ r := G(gg, gg); // error: cannot pass ghost 'gg' as non-ghost parameter to 'G'
+ }
+ var dd;
+ dd := GhostDt.Nil(g); // fine
+ dd := GhostDt.Cons(g, dt, 2); // error: cannot pass 'g' as non-ghost parameter
+ ghost var dtg := GhostDt.Cons(g, dt, 2); // fine, since result is ghost
+ }
+ function F(x: int, y: int): int {
+ y
+ }
+ function method G(x: int, ghost y: int): int {
+ y // error: cannot return a ghost from a non-ghost function
+ }
+ function method H(dt: GhostDt): int {
+ match dt
+ case Nil(gg) => gg // error: cannot return a ghost from a non-ghost function
+ case Cons(dd, tt, gg) => dd + gg // error: ditto
+ }
+ method N(x: int, ghost y: int) returns (r: int) {
+ r := x;
+ }
+ ghost method P(x: int, y: int) returns (r: int) {
+ ghost var g := 5;
+ r := y; // allowed, since the entire method is ghost
+ r := r + g; // fine, for the same reason
+ r := N(20, 20); // error: call to non-ghost method from ghost method is not okay
+ }
+ ghost method NiceTry()
+ ensures false;
+ {
+ while (true)
+ decreases *; // error: not allowed in ghost context
+ {
+ }
+ }
+ ghost method BreaksAreFineHere(t: int)
+ {
+ var n := 0;
+ ghost var k := 0;
+ while (true)
+ invariant n <= 112;
+ decreases 112 - n;
+ {
+ label MyStructure: {
+ if (k % 17 == 0) { break MyStructure; } // this is fine, because it's a ghost method
+ k := k + 1;
+ }
+ label MyOtherStructure:
+ if (k % 17 == 0) {
+ break MyOtherStructure;
+ } else {
+ k := k + 1;
+ }
+
+ if (n == 112) {
+ break;
+ } else if (n == t) {
+ return;
+ }
+ n := n + 1;
+ }
+ }
+ method BreakMayNotBeFineHere(ghost t: int)
+ {
+ var n := 0;
+ ghost var k := 0;
+ var p := 0;
+ while (true)
+ invariant n <= 112;
+ decreases 112 - n;
+ {
+ label MyStructure: {
+ if (k % 17 == 0) { break MyStructure; } // error: break from ghost to non-ghost point
+ k := k + 1;
+ }
+ label MyOtherStructure:
+ if (k % 17 == 0) {
+ break MyOtherStructure; // this break is fine
+ } else {
+ k := k + 1;
+ }
+
+ var dontKnow;
+ if (n == 112) {
+ ghost var m := 0;
+ label LoopLabel0:
+ label LoopLabel1:
+ while (m < 200) {
+ if (m % 103 == 0) {
+ if {
+ case true => break; // fine, since this breaks out of the enclosing ghost loop
+ case true => break LoopLabel0; // fine
+ case true => break LoopLabel1; // fine
+ }
+ } else if (m % 101 == 0) {
+ break break; // error: break out of non-ghost loop from ghost context
+ }
+ m := m + 3;
+ }
+ break;
+ } else if (dontKnow == 708) {
+ var q := 0;
+ while (q < 1) {
+ label IfNest:
+ if (p == 67) {
+ break break; // fine, since this is not a ghost context
+ } else if (*) {
+ break break break; // error: tries to break out of more loop levels than there are
+ } else if (*) {
+ break break; // fine, since this is not a ghost context
+ } else if (k == 67) {
+ break break; // error, because this is a ghost context
+ }
+ q := q + 1;
+ }
+ } else if (n == t) {
+ return; // error: this is a ghost context trying to return from a non-ghost method
+ }
+ n := n + 1;
+ p := p + 1;
+ }
+ }
+}
+
+method DuplicateLabels(n: int) {
+ var x;
+ if (n < 7) {
+ label DuplicateLabel: x := x + 1;
+ } else {
+ label DuplicateLabel: x := x + 1;
+ }
+ label DuplicateLabel: x := x + 1;
+ label DuplicateLabel: {
+ label AnotherLabel:
+ label DuplicateLabel: // error: duplicate label
+ label OneMoreTime:
+ x := x + 1;
+ }
+ label DuplicateLabel:
+ label DuplicateLabel: // error: duplicate label
+ x := x + 1;
+ label DuplicateLabel: x := x + 1;
+
+}
diff --git a/Test/dafny1/Substitution.dfy b/Test/dafny1/Substitution.dfy
index d3e0e82e..11c8c878 100644
--- a/Test/dafny1/Substitution.dfy
+++ b/Test/dafny1/Substitution.dfy
@@ -99,7 +99,7 @@ static ghost method TheoremSeq(e: Expression, v: int, val: int)
}
}
-static ghost method LemmaSeq(ghost parent: Expression, ghost q: seq<Expression>, v: int, val: int)
+static ghost method LemmaSeq(parent: Expression, q: seq<Expression>, v: int, val: int)
requires (forall a :: a in q ==> a < parent);
ensures |SubstSeq(parent, q, v, val)| == |q|;
ensures (forall k :: 0 <= k && k < |q| ==>
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 04:14:10 +0000