diff options
| author |  leino <unknown> | 2015-09-28 13:16:15 -0700 |
|---|---|---|
| committer | leino <unknown> | 2015-09-28 13:16:15 -0700 |
| commit | 0c1ec594e68dab4fcd458a00f9f7a1ac6de2e218 (patch) | |
| tree | cb89d6ef66c96bfa171f954898548f295a3cabc0 /Test/dafny0/CallStmtTests.dfy | |
| parent | ebaaa36321463925dc9030455e87ae17732b2353 (diff) | |
Changed computation of ghosts until pass 2 of resolution.
Other clean-up in resolution passes, like:
Include everything of type "char" into bounds that are discovered, and likewise for reference types.
Allow more set comprehensions, determining if they are finite based on their argument type.
Changed CalcExpr.SubExpressions to not include computed expressions.
Diffstat (limited to 'Test/dafny0/CallStmtTests.dfy')
| -rw-r--r-- | Test/dafny0/CallStmtTests.dfy | 34 |
1 files changed, 19 insertions, 15 deletions
diff --git a/Test/dafny0/CallStmtTests.dfy b/Test/dafny0/CallStmtTests.dfy index 67e66b34..46c466ff 100644 --- a/Test/dafny0/CallStmtTests.dfy +++ b/Test/dafny0/CallStmtTests.dfy @@ -1,23 +1,27 @@ // RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
-method testing1(t: int)
-{
- t := m(); // error: should be checked at the Dafny level, not fall to Boogie.
-}
+module M0 {
+ method testing1(t: int)
+ {
+ t := m(); // error: should be checked at the Dafny level, not fall to Boogie.
+ }
-method m() returns (r: int)
-{
- return 3;
+ method m() returns (r: int)
+ {
+ return 3;
+ }
}
-method testing2()
-{
- var v;
- v := m2(); // error: v needs to be ghost because r is.
-}
+module M1 {
+ method testing2()
+ {
+ var v;
+ v := m2(); // error: v needs to be ghost because r is.
+ }
-method m2() returns (ghost r: int)
-{
- r := 23;
+ method m2() returns (ghost r: int)
+ {
+ r := 23;
+ }
}
|