diff options
author | 2014-12-18 20:59:10 -0800 | |
---|---|---|
committer | 2014-12-18 20:59:10 -0800 | |
commit | 84819ceb711f1ae83327e2006df9bb1003ccd65e (patch) | |
tree | 93c6a25cac65ef702793fe7508eddf89df2e737e /Test/linear/typecheck.bpl | |
parent | 86cb1bc74ca8b0242131145ce9d4cbab085c02fd (diff) |
changed type checking of yield procedures so that they can only call other yielding procedures
Diffstat (limited to 'Test/linear/typecheck.bpl')
-rw-r--r-- | Test/linear/typecheck.bpl | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/Test/linear/typecheck.bpl b/Test/linear/typecheck.bpl index 57080cb8..5c936dd0 100644 --- a/Test/linear/typecheck.bpl +++ b/Test/linear/typecheck.bpl @@ -65,9 +65,11 @@ procedure {:yields} {:layer 1} D() yield;
}
-procedure E({:linear_in "D"} a: X, {:linear_in "D"} b: X) returns ({:linear "D"} c: X, {:linear "D"} d: X)
+procedure {:yields} {:layer 1} E({:linear_in "D"} a: X, {:linear_in "D"} b: X) returns ({:linear "D"} c: X, {:linear "D"} d: X)
{
+ yield;
c := a;
+ yield;
}
procedure {:yields} {:layer 0} F({:linear_in "D"} a: X) returns ({:linear "D"} c: X);
|