diff options
| author |  Rustan Leino <unknown> | 2014-02-23 22:06:56 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-02-23 22:06:56 -0800 |
| commit | e2f9a3153a2e80c055f9a6d1a2abf8ba9c787009 (patch) | |
| tree | 4f9b4d34c0714bc6a3ab8ff2892f2e6b4acf93a9 | |
| parent | 297f9d4f1b409b2204b536f8393db3f6ccec18e2 (diff) | |
Added another colemma-calls-function-recursively test
| -rw-r--r-- | Test/dafny0/Answer | 3 | ||||
| -rw-r--r-- | Test/dafny0/CoResolution.dfy | 10 |
2 files changed, 12 insertions, 1 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 78d6c126..7b546c36 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1404,7 +1404,8 @@ CoResolution.dfy(132,17): Error: a recursive call from a copredicate can go only CoResolution.dfy(138,17): Error: a recursive call from a copredicate can go only to other copredicates
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
-20 resolution/type errors detected in CoResolution.dfy
+CoResolution.dfy(164,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas
+21 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 bf224f25..1219db90 100644 --- a/Test/dafny0/CoResolution.dfy +++ b/Test/dafny0/CoResolution.dfy @@ -158,4 +158,14 @@ module CallGraph { calc { true; { assert P#[n](n); } }
101
}
+
+ colemma J()
+ {
+ var f := JF(); // error: cannot call non-colemma recursively from colemma
+ }
+ function JF(): int
+ {
+ J();
+ 5
+ }
}
|