4 files changed, 141 insertions, 6 deletions
diff --git a/Test/dafny0/Backticks.dfy b/Test/dafny0/Backticks.dfy
new file mode 100644
index 00000000..08606b55
--- /dev/null
+++ b/Test/dafny0/Backticks.dfy
@@ -0,0 +1,80 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+class C {
+  var x: int
+  var y: int
+  ghost var z: int
+
+  function F(): int
+    reads `x
+  {
+    x
+  }
+
+  function G(): int
+    reads `x
+  {
+    F()
+  }
+
+  function H(): int
+    reads this
+  {
+    F()
+  }
+
+  function I(n: nat): int
+    reads this
+  {
+    x + y + z + J(n)
+  }
+
+  function J(n: nat): int
+    reads `x, this`z
+    decreases {this}, n, 0
+  {
+    if n == 0 then 5 else
+    I(n-1)  // error: insufficient reads clause
+  }
+
+  function K(n: nat): int
+    reads `x
+    decreases {this}, n+1
+  {
+    L(n)
+  }
+
+  function L(n: nat): int
+    reads `x
+  {
+    if n < 2 then 5 else K(n-2)
+  }
+
+  method M()
+    modifies `x
+  {
+    N();
+  }
+
+  method N()
+    modifies `x
+  {
+    x := x + 1;
+  }
+
+  method O(n: nat)
+    modifies this
+  {
+    P(n);
+  }
+  method P(n: nat)
+    modifies `x
+    decreases n, 0
+  {
+    x := x + 1;
+    if n != 0 {
+      O(n-1);  // error: insufficient modifies clause to make call
+    }
+  }
+}
diff --git a/Test/dafny0/Backticks.dfy.expect b/Test/dafny0/Backticks.dfy.expect
new file mode 100644
index 00000000..82fc2933
--- /dev/null
+++ b/Test/dafny0/Backticks.dfy.expect
@@ -0,0 +1,11 @@
+Backticks.dfy(38,5): Error: insufficient reads clause to invoke function
+Execution trace:
+    (0,0): anon0
+    (0,0): anon5_Else
+    (0,0): anon6_Else
+Backticks.dfy(77,7): Error: call may violate context's modifies clause
+Execution trace:
+    (0,0): anon0
+    (0,0): anon3_Then
+
+Dafny program verifier finished with 13 verified, 2 errors
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy
index e324393d..bb51b01f 100644
--- a/Test/dafny0/ResolutionErrors.dfy
+++ b/Test/dafny0/ResolutionErrors.dfy
@@ -1259,3 +1259,45 @@ module SignatureCompletion {
   function F2<A,B>(s: set, x: A -> B): int
   function F3<A,B>(x: A -> B, s: set): int
 }
+
+// -------------- more fields as frame targets --------------------
+
+module FrameTargetFields {
+  class C {
+    var x: int
+    var y: int
+    ghost var z: int
+
+    method M()
+      modifies this
+    {
+      var n := 0;
+      ghost var save := y;
+      while n < x
+        modifies `x
+      {
+        n, x := n + 1, x - 1;
+      }
+      assert y == save;
+    }
+
+    ghost method N()
+      modifies this
+      modifies `y  // resolution error: cannot mention non-ghost here
+      modifies `z  // cool
+    {
+    }
+
+    method P()
+      modifies this
+    {
+      ghost var h := x;
+      while 0 <= h
+        modifies `x  // resolution error: cannot mention non-ghost here
+        modifies `z  // cool
+      {
+        h, z := h - 1, 5 * z;
+      }
+    }
+  }
+}
diff --git a/Test/dafny0/ResolutionErrors.dfy.expect b/Test/dafny0/ResolutionErrors.dfy.expect
index 3b768c84..7789c6f8 100644
--- a/Test/dafny0/ResolutionErrors.dfy.expect
+++ b/Test/dafny0/ResolutionErrors.dfy.expect
@@ -85,6 +85,8 @@ ResolutionErrors.dfy(1222,29): Error: the type of this variable is underspecifie
 ResolutionErrors.dfy(1232,34): Error: the type of this variable is underspecified
 ResolutionErrors.dfy(1248,21): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)
 ResolutionErrors.dfy(1249,24): Error: Undeclared top-level type or type parameter: X (did you forget to qualify a name?)
+ResolutionErrors.dfy(1286,16): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (y)
+ResolutionErrors.dfy(1296,18): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
 ResolutionErrors.dfy(429,2): Error: More than one anonymous constructor
 ResolutionErrors.dfy(50,13): Error: 'this' is not allowed in a 'static' context
 ResolutionErrors.dfy(111,9): Error: ghost variables are allowed only in specification contexts
@@ -108,11 +110,11 @@ ResolutionErrors.dfy(440,6): Error: when allocating an object of type 'Lucifer',
 ResolutionErrors.dfy(441,6): Error: when allocating an object of type 'Lucifer', one of its constructor methods must be called
 ResolutionErrors.dfy(443,9): Error: class Lamb does not have a anonymous constructor
 ResolutionErrors.dfy(839,11): Error: a modifies-clause expression must denote an object or a collection of objects (instead got int)
-ResolutionErrors.dfy(843,14): Error: in a ghost context, only ghost fields can be mentioned as frame targets (x)
-ResolutionErrors.dfy(846,12): Error: in a ghost context, only ghost fields can be mentioned as frame targets (x)
-ResolutionErrors.dfy(854,14): Error: in a ghost context, only ghost fields can be mentioned as frame targets (x)
-ResolutionErrors.dfy(864,18): Error: in a ghost context, only ghost fields can be mentioned as frame targets (x)
-ResolutionErrors.dfy(875,16): Error: in a ghost context, only ghost fields can be mentioned as frame targets (x)
+ResolutionErrors.dfy(843,14): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
+ResolutionErrors.dfy(846,12): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
+ResolutionErrors.dfy(854,14): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
+ResolutionErrors.dfy(864,18): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
+ResolutionErrors.dfy(875,16): Error: in a ghost context, only ghost fields can be mentioned as modifies frame targets (x)
 ResolutionErrors.dfy(1031,23): Error: unresolved identifier: x
 ResolutionErrors.dfy(1034,20): Error: unresolved identifier: x
 ResolutionErrors.dfy(1037,23): Error: unresolved identifier: x
@@ -182,4 +184,4 @@ ResolutionErrors.dfy(1101,8): Error: new cannot be applied to a trait
 ResolutionErrors.dfy(1122,13): Error: first argument to / must be of numeric type (instead got set<bool>)
 ResolutionErrors.dfy(1129,2): 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(1144,14): Error: a possibly infinite loop is allowed only if the enclosing method is declared (with 'decreases *') to be possibly non-terminating
-184 resolution/type errors detected in ResolutionErrors.dfy
+186 resolution/type errors detected in ResolutionErrors.dfy