diff options
| author |  Rustan Leino <unknown> | 2013-08-04 17:55:06 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2013-08-04 17:55:06 -0700 |
| commit | a1710a324a8d92935cd7bc8ecbda115b9cd09748 (patch) | |
| tree | 0da87df5c79764cc7d46da695561ea8134f60146 /Test/dafny0/ResolutionErrors.dfy | |
| parent | 8af0f2d97ab5ca1a212c7f4901c43059ccb08e36 (diff) | |
Set up call-graph to keep track of edges between functions and methods. (To be done: replace InMethodContext with a Function/Method-Height in translator.)
Diffstat (limited to 'Test/dafny0/ResolutionErrors.dfy')
| -rw-r--r-- | Test/dafny0/ResolutionErrors.dfy | 95 |
1 files changed, 95 insertions, 0 deletions
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index 92b4aa80..b96b0867 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -653,3 +653,98 @@ lemma MyLemma(x: int) returns (y: int) {
y := x;
}
+
+// ------------------------- statements in expressions ------------------------------
+
+module StatementsInExpressions {
+ ghost method SideEffect()
+ modifies this;
+ {
+ }
+
+ method NonGhostMethod()
+ {
+ }
+
+ ghost method M()
+ modifies this;
+ {
+ calc {
+ 5;
+ { SideEffect(); } // error: cannot call method with side effects
+ 5;
+ }
+ }
+
+ function F(): int
+ {
+ calc {
+ 6;
+ { assert 6 < 8; }
+ { NonGhostMethod(); } // error: cannot call non-ghost method
+ { var x := 8;
+ while x != 0
+ decreases *; // error: cannot use 'decreases *' in a ghost context
+ {
+ x := x - 1;
+ }
+ }
+ { var x := 8;
+ while x != 0
+ {
+ x := x - 1;
+ }
+ }
+ { MyField := 12; } // error: cannot assign to a field
+ { MyGhostField := 12; } // error: cannot assign to any field
+ { SideEffect(); } // error: cannot call (ghost) method with a modifies clause
+ { var x := 8;
+ while x != 0
+ modifies this; // error: cannot use a modifies clause on a loop
+ {
+ x := x - 1;
+ }
+ }
+ 6;
+ }
+ 5
+ }
+
+ var MyField: int;
+ ghost var MyGhostField: int;
+
+ method N()
+ {
+ var y :=
+ calc {
+ 6;
+ { assert 6 < 8; }
+ { NonGhostMethod(); } // error: cannot call non-ghost method
+ { var x := 8;
+ while x != 0
+ decreases *; // error: cannot use 'decreases *' in a ghost context
+ {
+ x := x - 1;
+ }
+ }
+ { MyField := 12; } // error: cannot assign to a field
+ { MyGhostField := 12; } // error: cannot assign to any field
+ { M(); } // error: cannot call (ghost) method with a modifies clause
+ { var x := 8;
+ while x != 0
+ modifies this; // error: cannot use a modifies clause on a loop
+ {
+ x := x - 1;
+ }
+ }
+ { var x := 8;
+ while x != 0
+ {
+ x := x - 1;
+ }
+ }
+ 6;
+ }
+ 5;
+ }
+}
|