diff options
| author |  Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2013-03-13 10:02:01 -0700 |
|---|---|---|
| committer | Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com> | 2013-03-13 10:02:01 -0700 |
| commit | df2694faaf9b53d4b609270c431c76ec5b2068ff (patch) | |
| tree | a9f969b405b3f66d9b7a2f4e0f666b064deeb363 /Test/linear/typecheck.bpl | |
| parent | c344350ef8cc83b5e0aa9332435fbe095bc84bc0 (diff) | |
added mod set checking to the linear type checker
Diffstat (limited to 'Test/linear/typecheck.bpl')
| -rw-r--r-- | Test/linear/typecheck.bpl | 9 |
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;
+}
|