summaryrefslogtreecommitdiff
path: root/Test/linear/typecheck.bpl
diff options
context:
space:
mode:
Diffstat (limited to 'Test/linear/typecheck.bpl')
-rw-r--r--Test/linear/typecheck.bpl9
1 files changed, 8 insertions, 1 deletions
diff --git a/Test/linear/typecheck.bpl b/Test/linear/typecheck.bpl
index c188d5b5..ff2d7da4 100644
--- a/Test/linear/typecheck.bpl
+++ b/Test/linear/typecheck.bpl
@@ -66,4 +66,11 @@ procedure E({:linear "D"} a: X, {:linear "D"} b: X) returns ({:linear "D"} c: X,
c := a;
}
-procedure F({:linear "D"} a: X) returns ({:linear "D"} c: X); \ No newline at end of file
+procedure F({:linear "D"} a: X) returns ({:linear "D"} c: X);
+
+var{:linear "x"} g:int;
+
+procedure G(i:int) returns({:linear "x"} r:int)
+{
+ r := g;
+}