summaryrefslogtreecommitdiff
path: root/Test/linear/typecheck.bpl
diff options
context:
space:
mode:
authorGravatar Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com>2013-03-03 22:43:56 -0800
committerGravatar Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com>2013-03-03 22:43:56 -0800
commit68a39909f93535ad4d091fce647d8a0e8539508f (patch)
tree2b1f666381bcb13849cdc3797b4d36cf9a84a47f /Test/linear/typecheck.bpl
parent8f5515633b1273670a96a2c6b961317293d07ebf (diff)
fixed bugs in both parallel calls and linear stuff (reported by Chris)
also added improved error reporting suggested by Chris
Diffstat (limited to 'Test/linear/typecheck.bpl')
-rw-r--r--Test/linear/typecheck.bpl6
1 files changed, 5 insertions, 1 deletions
diff --git a/Test/linear/typecheck.bpl b/Test/linear/typecheck.bpl
index f79f8fb5..c188d5b5 100644
--- a/Test/linear/typecheck.bpl
+++ b/Test/linear/typecheck.bpl
@@ -57,9 +57,13 @@ procedure D()
call a, x := E(c, x);
call c, x := E(a, x);
+
+ call a := F(a) | x := F(a);
}
procedure E({:linear "D"} a: X, {:linear "D"} b: X) returns ({:linear "D"} c: X, {:linear "D"} d: X)
{
c := a;
-} \ No newline at end of file
+}
+
+procedure F({:linear "D"} a: X) returns ({:linear "D"} c: X); \ No newline at end of file