diff options
author | Jason Koenig <unknown> | 2011-07-06 14:10:11 -0700 |
---|---|---|
committer | Jason Koenig <unknown> | 2011-07-06 14:10:11 -0700 |
commit | 98b0ebe1adba86bbf8452bcb036f01c884b69b90 (patch) | |
tree | d0636bc39de34e2adaccc33a7671226b85bc50a1 /Test/dafny0/CallStmtTests.dfy | |
parent | 1a2271a8bc81a8ff96b033c3911cb80db6832dc1 (diff) |
Dafny: Fixed bug in call statements where mutability of out parameters was not checked.
Added regression test.
Diffstat (limited to 'Test/dafny0/CallStmtTests.dfy')
-rw-r--r-- | Test/dafny0/CallStmtTests.dfy | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/Test/dafny0/CallStmtTests.dfy b/Test/dafny0/CallStmtTests.dfy new file mode 100644 index 00000000..735efe81 --- /dev/null +++ b/Test/dafny0/CallStmtTests.dfy @@ -0,0 +1,21 @@ +
+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 testing2()
+{
+ var v;
+ v := m2(); // error: v needs to be ghost because r is.
+}
+
+method m2() returns (ghost r: int)
+{
+ r := 23;
+}
|