From ebbb5597c34d69490704b7425cf80830b8e99f7e Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Sun, 4 Aug 2013 18:38:50 -0700
Subject: Disallow call-graph clusters that mix co-methods / prefix methods
 with other things. Disallow call-graph clusters that mix co-predicates /
 prefix predicates with other things.

---
 Test/dafny0/Answer           |  8 +++++-
 Test/dafny0/CoResolution.dfy | 62 ++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 69 insertions(+), 1 deletion(-)

(limited to 'Test')

diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer
index c79d166a..b462465d 100644
--- a/Test/dafny0/Answer
+++ b/Test/dafny0/Answer
@@ -1242,7 +1242,13 @@ CoResolution.dfy(70,31): Error: a copredicate is not allowed to declare any ensu
 CoResolution.dfy(79,20): Error: a recursive call from a copredicate can go only to other copredicates
 CoResolution.dfy(83,20): Error: a recursive call from a copredicate can go only to other copredicates
 CoResolution.dfy(92,4): Error: a recursive call from a comethod can go only to other comethods and prefix methods
-10 resolution/type errors detected in CoResolution.dfy
+CoResolution.dfy(106,13): Error: a recursive call from a comethod can go only to other comethods and prefix methods
+CoResolution.dfy(107,13): Error: a recursive call from a comethod can go only to other comethods and prefix methods
+CoResolution.dfy(126,13): Error: a recursive call from a comethod can go only to other comethods and prefix methods
+CoResolution.dfy(127,13): Error: a recursive call from a comethod can go only to other comethods and prefix methods
+CoResolution.dfy(146,4): Error: a recursive call from a copredicate can go only to other copredicates
+CoResolution.dfy(148,4): Error: a recursive call from a copredicate can go only to other copredicates
+16 resolution/type errors detected in CoResolution.dfy
 
 -------------------- CoPrefix.dfy --------------------
 CoPrefix.dfy(161,3): Error BP5003: A postcondition might not hold on this return path.
diff --git a/Test/dafny0/CoResolution.dfy b/Test/dafny0/CoResolution.dfy
index 1b1923c3..9ab52d53 100644
--- a/Test/dafny0/CoResolution.dfy
+++ b/Test/dafny0/CoResolution.dfy
@@ -97,3 +97,65 @@ module Mojul1 {
   comethod G() { H(); }
   comethod H() { G#[10](); }  // fine for comethod/prefix-method
 }
+
+module CallGraph {
+  // comethod -> copredicate -> comethod
+  // comethod -> copredicate -> prefix method
+  comethod CoLemma(n: nat)
+  {
+    var q := Q(n);  // error
+    var r := R(n);  // error
+  }
+
+  copredicate Q(n: nat)
+  {
+    calc { 87; { CoLemma(n); } }
+    false
+  }
+
+  copredicate R(n: nat)
+  {
+    calc { 87; { CoLemma#[n](n); } }
+    false
+  }
+
+  // comethod -> prefix predicate -> comethod
+  // comethod -> prefix predicate -> prefix method
+  comethod CoLemma_D(n: nat)
+  {
+    var q := Q_D#[n](n);  // error
+    var r := R_D#[n](n);  // error
+  }
+
+  copredicate Q_D(n: nat)
+  {
+    calc { 88; { CoLemma_D(n); } }
+    false
+  }
+
+  copredicate R_D(n: nat)
+  {
+    calc { 89; { CoLemma_D#[n](n); } }
+    false
+  }
+
+  // copredicate -> function -> copredicate
+  // copredicate -> function -> prefix predicate
+  copredicate P(n: nat)
+  {
+    G0(n)  // error
+    <
+    G1(n)  // error
+  }
+
+  function G0(n: nat): int
+  {
+    calc { true; { assert P(n); } }
+    100
+  }
+  function G1(n: nat): int
+  {
+    calc { true; { assert P#[n](n); } }
+    101
+  }
+}
-- 
cgit v1.2.3