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 /Test/dafny0/CoResolution.dfy | |
| parent | 297f9d4f1b409b2204b536f8393db3f6ccec18e2 (diff) | |
Added another colemma-calls-function-recursively test
Diffstat (limited to 'Test/dafny0/CoResolution.dfy')
| -rw-r--r-- | Test/dafny0/CoResolution.dfy | 10 |
1 files changed, 10 insertions, 0 deletions
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
+ }
}
|