From 800885b4d7d0164803c0c2f117b78c65479283f9 Mon Sep 17 00:00:00 2001 From: leino Date: Sun, 20 Sep 2015 21:51:42 -0700 Subject: Preliminary refactoring of ghost-statement computations to after type checking --- Test/dafny0/AssumptionVariables0.dfy | 8 ++++++-- Test/dafny0/AssumptionVariables0.dfy.expect | 5 ++--- Test/dafny0/ParallelResolveErrors.dfy | 4 ++-- Test/dafny0/ParallelResolveErrors.dfy.expect | 5 +++-- Test/dafny0/ResolutionErrors.dfy | 16 ++++++++-------- Test/dafny0/ResolutionErrors.dfy.expect | 13 ++----------- Test/dafny0/TypeTests.dfy.expect | 2 +- 7 files changed, 24 insertions(+), 29 deletions(-) (limited to 'Test/dafny0') diff --git a/Test/dafny0/AssumptionVariables0.dfy b/Test/dafny0/AssumptionVariables0.dfy index a3e23b73..b9acc522 100644 --- a/Test/dafny0/AssumptionVariables0.dfy +++ b/Test/dafny0/AssumptionVariables0.dfy @@ -6,7 +6,7 @@ method test0(x: int) ghost var {:assumption} a0 := false; // error ghost var a1, {:assumption} a2 := true, false; // error ghost var {:assumption} a3: bool; - var {:assumption} a4; // 2 errors + ghost var {:assumption} a4; // error: type must be bool a0 := a0 && (0 < x); @@ -54,7 +54,7 @@ method test2() if (false) { - var {:assumption} a0: bool; // error + ghost var {:assumption} a0: bool; if (false) { @@ -73,3 +73,7 @@ method test2() } } } + +method test3() { + var {:assumption} a: bool; // error: assumption variable must be ghost +} diff --git a/Test/dafny0/AssumptionVariables0.dfy.expect b/Test/dafny0/AssumptionVariables0.dfy.expect index f2d43fe1..16572961 100644 --- a/Test/dafny0/AssumptionVariables0.dfy.expect +++ b/Test/dafny0/AssumptionVariables0.dfy.expect @@ -1,14 +1,13 @@ AssumptionVariables0.dfy(6,29): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && " AssumptionVariables0.dfy(7,33): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a2 && " -AssumptionVariables0.dfy(9,20): Error: assumption variable must be ghost AssumptionVariables0.dfy(9,2): Error: assumption variable must be of type 'bool' AssumptionVariables0.dfy(15,5): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a3 && " AssumptionVariables0.dfy(17,5): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a3 && " AssumptionVariables0.dfy(27,5): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && " AssumptionVariables0.dfy(31,5): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && " AssumptionVariables0.dfy(53,9): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && " -AssumptionVariables0.dfy(57,26): Error: assumption variable must be ghost AssumptionVariables0.dfy(61,37): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && " AssumptionVariables0.dfy(61,10): Error: assumption variable must be of type 'bool' AssumptionVariables0.dfy(69,15): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && " -13 resolution/type errors detected in AssumptionVariables0.dfy +AssumptionVariables0.dfy(78,20): Error: assumption variable must be ghost +12 resolution/type errors detected in AssumptionVariables0.dfy diff --git a/Test/dafny0/ParallelResolveErrors.dfy b/Test/dafny0/ParallelResolveErrors.dfy index 5e01f019..61956651 100644 --- a/Test/dafny0/ParallelResolveErrors.dfy +++ b/Test/dafny0/ParallelResolveErrors.dfy @@ -40,8 +40,8 @@ method M0(IS: set) { var x := i; x := x + 1; - y := 18; // (this statement is not allowed, since y is declared outside the forall, but that check happens only if the first resolution pass of the forall statement passes, which it doesn't in this case because of the next line) - z := 20; // error: assigning to a non-ghost variable inside a ghost forall block + y := 18; // error: assigning to a (ghost) variable inside a ghost forall block + z := 20; // error: assigning to a (non-ghost) variable inside a ghost forall block } forall (i | 0 <= i) diff --git a/Test/dafny0/ParallelResolveErrors.dfy.expect b/Test/dafny0/ParallelResolveErrors.dfy.expect index 7305bfce..00030994 100644 --- a/Test/dafny0/ParallelResolveErrors.dfy.expect +++ b/Test/dafny0/ParallelResolveErrors.dfy.expect @@ -1,7 +1,8 @@ ParallelResolveErrors.dfy(10,9): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) ParallelResolveErrors.dfy(21,4): Error: LHS of assignment must denote a mutable variable ParallelResolveErrors.dfy(26,6): Error: body of forall statement is attempting to update a variable declared outside the forall statement -ParallelResolveErrors.dfy(44,6): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) +ParallelResolveErrors.dfy(43,6): Error: body of forall statement is attempting to update a variable declared outside the forall statement +ParallelResolveErrors.dfy(44,6): Error: body of forall statement is attempting to update a variable declared outside the forall statement ParallelResolveErrors.dfy(56,13): Error: new allocation not supported in forall statements ParallelResolveErrors.dfy(61,13): Error: new allocation not allowed in ghost context ParallelResolveErrors.dfy(62,13): Error: new allocation not allowed in ghost context @@ -19,4 +20,4 @@ ParallelResolveErrors.dfy(96,24): Error: break label is undefined or not in scop ParallelResolveErrors.dfy(107,9): Error: the body of the enclosing forall statement is not allowed to update heap locations ParallelResolveErrors.dfy(115,29): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause ParallelResolveErrors.dfy(120,29): Error: the body of the enclosing forall statement is not allowed to update heap locations, so any call must be to a method with an empty modifies clause -21 resolution/type errors detected in ParallelResolveErrors.dfy +22 resolution/type errors detected in ParallelResolveErrors.dfy diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index 1354e533..5f0b22a2 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -195,7 +195,7 @@ class GhostTests { decreases 112 - n; { label MyStructure: { - if (k % 17 == 0) { break MyStructure; } // error: break from ghost to non-ghost point +//KRML(ghost) if (k % 17 == 0) { break MyStructure; } // error: break from ghost to non-ghost point k := k + 1; } label MyOtherStructure: @@ -218,7 +218,7 @@ class GhostTests { case true => break LoopLabel1; // fine } } else if (m % 101 == 0) { - break break; // error: break out of non-ghost loop from ghost context +//KRML(ghost) break break; // error: break out of non-ghost loop from ghost context } m := m + 3; } @@ -232,14 +232,14 @@ class GhostTests { } 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 +//KRML(ghost) break break; // fine, since this is not a ghost context } else if (k == 67) { - break break; // error, because this is a ghost context +//KRML(ghost) 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 +//KRML(ghost) return; // error: this is a ghost context trying to return from a non-ghost method } n := n + 1; p := p + 1; @@ -310,7 +310,7 @@ method DatatypeDestructors(d: DTD_List) { assert d.DTD_Cons? == d.Car; // type error assert d == DTD_Cons(hd, tl, 5); ghost var g0 := d.g; // fine - var g1 := d.g; // error: cannot use ghost member in non-ghost code +//KRML(ghost) var g1 := d.g; // error: cannot use ghost member in non-ghost code } } @@ -383,7 +383,7 @@ method TestCalc(m: int, n: int, a: bool, b: bool) } calc { n + m; - { print n + m; } // error: non-ghost statements are not allowed in hints +//KRML(ghost) { print n + m; } // error: non-ghost statements are not allowed in hints m + n; } } @@ -543,7 +543,7 @@ method LetSuchThat(ghost z: int, n: nat) var x: int; x := var y :| y < 0; y; // fine for the resolver (but would give a verification error for not being deterministic) - x := var y :| y < z; y; // error: contraint depend on ghost (z) +//KRML(ghost) x := var y :| y < z; y; // error: contraint depend on ghost (z) x := var w :| w == 2*w; w; // fine (even for the verifier, this one) x := var w := 2*w; w; // error: the 'w' in the RHS of the assignment is not in scope diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect index b5c93ac1..8debdbf9 100644 --- a/Test/dafny0/ResolutionErrors.dfy.expect +++ b/Test/dafny0/ResolutionErrors.dfy.expect @@ -21,14 +21,12 @@ ResolutionErrors.dfy(642,21): Error: the type of this variable is underspecified ResolutionErrors.dfy(680,13): Error: calls to methods with side-effects are not allowed inside a hint ResolutionErrors.dfy(690,17): Error: only ghost methods can be called from this context ResolutionErrors.dfy(693,15): Error: 'decreases *' is not allowed on ghost loops -ResolutionErrors.dfy(704,11): Error: Assignment to non-ghost field 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(704,11): Error: a hint is not allowed to update heap locations ResolutionErrors.dfy(705,16): Error: a hint is not allowed to update heap locations ResolutionErrors.dfy(706,13): Error: calls to methods with side-effects are not allowed inside a hint ResolutionErrors.dfy(709,14): Error: a while statement used inside a hint is not allowed to have a modifies clause ResolutionErrors.dfy(728,17): Error: only ghost methods can be called from this context ResolutionErrors.dfy(731,15): Error: 'decreases *' is not allowed on ghost loops -ResolutionErrors.dfy(736,11): Error: Assignment to non-ghost field 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(736,11): Error: a hint is not allowed to update heap locations ResolutionErrors.dfy(737,16): Error: a hint is not allowed to update heap locations ResolutionErrors.dfy(738,4): Error: calls to methods with side-effects are not allowed inside a hint @@ -126,11 +124,7 @@ ResolutionErrors.dfy(141,21): Error: ghost variables are allowed only in specifi ResolutionErrors.dfy(142,35): Error: ghost variables are allowed only in specification contexts ResolutionErrors.dfy(151,10): Error: only ghost methods can be called from this context ResolutionErrors.dfy(157,16): Error: 'decreases *' is not allowed on ghost loops -ResolutionErrors.dfy(198,27): Error: ghost-context break statement is not allowed to break out of non-ghost structure -ResolutionErrors.dfy(221,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop ResolutionErrors.dfy(233,12): Error: trying to break out of more loop levels than there are enclosing loops -ResolutionErrors.dfy(237,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop -ResolutionErrors.dfy(242,8): Error: return statement is not allowed in this context (because it is guarded by a specification-only expression) ResolutionErrors.dfy(408,11): Error: calls to methods with side-effects are not allowed inside a hint ResolutionErrors.dfy(410,14): Error: a hint is not allowed to update heap locations ResolutionErrors.dfy(412,10): Error: a hint is not allowed to update a variable declared outside the hint @@ -170,7 +164,6 @@ ResolutionErrors.dfy(294,9): Error: a constructor is allowed to be called only w ResolutionErrors.dfy(308,16): Error: arguments must have the same type (got int and DTD_List) ResolutionErrors.dfy(309,16): Error: arguments must have the same type (got DTD_List and int) ResolutionErrors.dfy(310,25): Error: arguments must have the same type (got bool and int) -ResolutionErrors.dfy(313,18): Error: ghost fields are allowed only in specification contexts ResolutionErrors.dfy(322,15): Error: ghost variables are allowed only in specification contexts ResolutionErrors.dfy(347,5): Error: incorrect type of method in-parameter 1 (expected GenericClass, got GenericClass) ResolutionErrors.dfy(359,18): Error: incorrect type of datatype constructor argument (found GList<_T0>, expected GList) @@ -182,10 +175,8 @@ ResolutionErrors.dfy(376,10): Error: first argument to ==> must be of type bool ResolutionErrors.dfy(376,10): Error: second argument to ==> must be of type bool (instead got int) ResolutionErrors.dfy(381,10): Error: first argument to ==> must be of type bool (instead got int) ResolutionErrors.dfy(381,10): Error: second argument to ==> must be of type bool (instead got int) -ResolutionErrors.dfy(386,6): Error: print 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(470,7): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(476,12): Error: ghost variables are allowed only in specification contexts -ResolutionErrors.dfy(546,20): Error: ghost variables are allowed only in specification contexts +ResolutionErrors.dfy(476,2): Error: non-ghost variable cannot be assigned a value that depends on a ghost ResolutionErrors.dfy(549,18): Error: unresolved identifier: w ResolutionErrors.dfy(656,11): Error: lemmas are not allowed to have modifies clauses ResolutionErrors.dfy(918,9): Error: unresolved identifier: s @@ -200,4 +191,4 @@ ResolutionErrors.dfy(1106,8): Error: new cannot be applied to a trait ResolutionErrors.dfy(1127,13): Error: first argument to / must be of numeric type (instead got set) ResolutionErrors.dfy(1134,18): Error: a call to a possibly non-terminating method is allowed only if the calling method is also declared (with 'decreases *') to be possibly non-terminating ResolutionErrors.dfy(1149,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating -202 resolution/type errors detected in ResolutionErrors.dfy +193 resolution/type errors detected in ResolutionErrors.dfy diff --git a/Test/dafny0/TypeTests.dfy.expect b/Test/dafny0/TypeTests.dfy.expect index 500b1af9..8206fd43 100644 --- a/Test/dafny0/TypeTests.dfy.expect +++ b/Test/dafny0/TypeTests.dfy.expect @@ -56,7 +56,7 @@ TypeTests.dfy(151,13): Error: sorry, cannot instantiate type parameter with a su TypeTests.dfy(152,2): Error: sorry, cannot instantiate type parameter with a subrange type TypeTests.dfy(153,16): Error: sorry, cannot instantiate type parameter with a subrange type TypeTests.dfy(154,14): Error: sorry, cannot instantiate type parameter with a subrange type -TypeTests.dfy(177,15): Error: ghost variables are allowed only in specification contexts +TypeTests.dfy(177,5): Error: non-ghost variable cannot be assigned a value that depends on a ghost TypeTests.dfy(187,4): Error: cannot assign to non-ghost variable in a ghost context TypeTests.dfy(188,7): Error: cannot assign to non-ghost variable in a ghost context TypeTests.dfy(21,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed -- cgit v1.2.3