From 029f016b365c844137399b2153bf59339d5612b7 Mon Sep 17 00:00:00 2001 From: leino Date: Sun, 20 Sep 2015 22:11:33 -0700 Subject: Added back in various ghost tests --- Test/dafny0/ResolutionErrors.dfy | 10 +++++----- Test/dafny0/ResolutionErrors.dfy.expect | 9 ++++++++- 2 files changed, 13 insertions(+), 6 deletions(-) (limited to 'Test') diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index d38d2506..2fab6bf3 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -238,7 +238,7 @@ class GhostTests { p := p + 1; } } -/***KRML method BreakMayNotBeFineHere_Ghost(ghost t: int) +method BreakMayNotBeFineHere_Ghost(ghost t: int) { var n := 0; ghost var k := 0; @@ -295,7 +295,7 @@ class GhostTests { n := n + 1; p := p + 1; } - }****/ + } } method DuplicateLabels(n: int) { @@ -364,7 +364,7 @@ method DatatypeDestructors(d: DTD_List) { } } method DatatypeDestructors_Ghost(d: DTD_List) { -//KRML var g1 := d.g; // error: cannot use ghost member in non-ghost code + var g1 := d.g; // error: cannot use ghost member in non-ghost code } // ------------------- print statements --------------------------------------- @@ -439,7 +439,7 @@ method TestCalc_Ghost(m: int, n: int, a: bool, b: bool) { calc { n + m; -//KRML { print n + m; } // error: non-ghost statements are not allowed in hints + { print n + m; } // error: non-ghost statements are not allowed in hints m + n; } } @@ -605,7 +605,7 @@ method LetSuchThat(ghost z: int, n: nat) } method LetSuchThat_Ghost(ghost z: int, n: nat) { -//KRML var x := var y :| y < z; y; // error: contraint depend on ghost (z) + var x := var y :| y < z; y; // error: contraint depend on ghost (z) } // ------------ quantified variables whose types are not inferred ---------- diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect index 55d2e79c..0286778b 100644 --- a/Test/dafny0/ResolutionErrors.dfy.expect +++ b/Test/dafny0/ResolutionErrors.dfy.expect @@ -125,6 +125,10 @@ ResolutionErrors.dfy(142,35): Error: ghost variables are allowed only in specifi 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(231,12): Error: trying to break out of more loop levels than there are enclosing loops +ResolutionErrors.dfy(251,27): Error: ghost-context break statement is not allowed to break out of non-ghost structure +ResolutionErrors.dfy(274,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop +ResolutionErrors.dfy(288,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop +ResolutionErrors.dfy(293,8): Error: return statement is not allowed in this context (because it is guarded by a specification-only expression) ResolutionErrors.dfy(464,11): Error: calls to methods with side-effects are not allowed inside a hint ResolutionErrors.dfy(466,14): Error: a hint is not allowed to update heap locations ResolutionErrors.dfy(468,10): Error: a hint is not allowed to update a variable declared outside the hint @@ -164,6 +168,7 @@ ResolutionErrors.dfy(345,9): Error: a constructor is allowed to be called only w ResolutionErrors.dfy(359,16): Error: arguments must have the same type (got int and DTD_List) ResolutionErrors.dfy(360,16): Error: arguments must have the same type (got DTD_List and int) ResolutionErrors.dfy(361,25): Error: arguments must have the same type (got bool and int) +ResolutionErrors.dfy(367,14): Error: ghost fields are allowed only in specification contexts ResolutionErrors.dfy(375,15): Error: ghost variables are allowed only in specification contexts ResolutionErrors.dfy(400,5): Error: incorrect type of method in-parameter 1 (expected GenericClass, got GenericClass) ResolutionErrors.dfy(412,18): Error: incorrect type of datatype constructor argument (found GList<_T0>, expected GList) @@ -175,9 +180,11 @@ ResolutionErrors.dfy(429,10): Error: first argument to ==> must be of type bool ResolutionErrors.dfy(429,10): Error: second argument to ==> must be of type bool (instead got int) ResolutionErrors.dfy(434,10): Error: first argument to ==> must be of type bool (instead got int) ResolutionErrors.dfy(434,10): Error: second argument to ==> must be of type bool (instead got int) +ResolutionErrors.dfy(442,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(526,7): Error: ghost variables are allowed only in specification contexts ResolutionErrors.dfy(532,2): Error: non-ghost variable cannot be assigned a value that depends on a ghost ResolutionErrors.dfy(603,18): Error: unresolved identifier: w +ResolutionErrors.dfy(608,24): Error: ghost variables are allowed only in specification contexts ResolutionErrors.dfy(714,11): Error: lemmas are not allowed to have modifies clauses ResolutionErrors.dfy(976,9): Error: unresolved identifier: s ResolutionErrors.dfy(987,32): Error: RHS (of type (int,int,real)) not assignable to LHS (of type (int,real,int)) @@ -191,4 +198,4 @@ ResolutionErrors.dfy(1164,8): Error: new cannot be applied to a trait ResolutionErrors.dfy(1185,13): Error: first argument to / must be of numeric type (instead got set) ResolutionErrors.dfy(1192,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(1207,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating -193 resolution/type errors detected in ResolutionErrors.dfy +200 resolution/type errors detected in ResolutionErrors.dfy -- cgit v1.2.3