Added back in various ghost tests

2 files changed, 13 insertions, 6 deletions

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<int>, got GenericClass<bool>)

 ResolutionErrors.dfy(412,18): Error: incorrect type of datatype constructor argument (found GList<_T0>, expected GList<int>)

@@ -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<bool>)

 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