diff options
| author |  Jason Koenig <unknown> | 2011-06-29 17:41:26 -0700 |
|---|---|---|
| committer | Jason Koenig <unknown> | 2011-06-29 17:41:26 -0700 |
| commit | 0c344651c1b3d9b4f1e073980b3c4cc9332a6d54 (patch) | |
| tree | ea05159d30764a53ba709a12ecd0d3e6437890ac /Test/dafny0/ReturnErrors.dfy | |
| parent | 6c554ef06d3e90aff8162ca6dcba5ad2e4bc247a (diff) | |
Added regression tests for new return statements with parameters.
Diffstat (limited to 'Test/dafny0/ReturnErrors.dfy')
| -rw-r--r-- | Test/dafny0/ReturnErrors.dfy | 42 |
1 files changed, 42 insertions, 0 deletions
diff --git a/Test/dafny0/ReturnErrors.dfy b/Test/dafny0/ReturnErrors.dfy new file mode 100644 index 00000000..1141808a --- /dev/null +++ b/Test/dafny0/ReturnErrors.dfy @@ -0,0 +1,42 @@ +
+class N
+{
+ var i: int;
+ method newN(n: N)
+ requires n != null;
+ modifies this, n;
+ {
+ n.i := 1;
+ i := 1;
+ }
+ method safe(n: N)
+ requires n != null;
+ modifies this;
+ {
+ i := n.i;
+ }
+}
+
+method m(v: int, n: N) returns (r: int)
+ modifies n;
+ ensures r == v;
+{
+ r := v;
+}
+method testing1() returns (s: int)
+ ensures s == 3;
+{
+ var n := new N;
+ return m(3, n); // methods disallowed.
+}
+method testing2() returns (s: int, b: int)
+ ensures s == 3;
+{
+ var n := new N;
+ return m(3, n), 2; // methods disallowed.
+}
+
+method testing3() returns (n: N)
+{
+ return new N.newN(n); // disallowed, as newN() modifies n
+}
\ No newline at end of file |