diff options
| author |  Rustan Leino <unknown> | 2013-08-06 03:52:25 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2013-08-06 03:52:25 -0700 |
| commit | dd65717941251e2be9df829694a42ec4d015bb53 (patch) | |
| tree | 87a044a7a8a16d569aa3bb969df08c367b14ed73 /Test/dafny0/ResolutionErrors.dfy | |
| parent | 739d4aeff0124e69e30f17880d403b59fd008670 (diff) | |
Allow calls to side-effect-free ghost methods from expressions
Diffstat (limited to 'Test/dafny0/ResolutionErrors.dfy')
| -rw-r--r-- | Test/dafny0/ResolutionErrors.dfy | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index b96b0867..926f08ae 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -747,4 +747,19 @@ module StatementsInExpressions { }
5;
}
+
+ ghost method MyLemma()
+ ghost method MyGhostMethod()
+ modifies this;
+ method OrdinaryMethod()
+ ghost method OutParamMethod() returns (y: int)
+
+ function UseLemma(): int
+ {
+ MyLemma();
+ MyGhostMethod(); // error: modifies state
+ OrdinaryMethod(); // error: not a ghost
+ OutParamMethod(); // error: has out-parameters
+ 10
+ }
}
|