From df2694faaf9b53d4b609270c431c76ec5b2068ff Mon Sep 17 00:00:00 2001
From: Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com>
Date: Wed, 13 Mar 2013 10:02:01 -0700
Subject: added mod set checking to the linear type checker

---
 Test/linear/Answer        | 1 +
 Test/linear/runtest.bat   | 8 +++++++-
 Test/linear/typecheck.bpl | 9 ++++++++-
 3 files changed, 16 insertions(+), 2 deletions(-)

(limited to 'Test/linear')

diff --git a/Test/linear/Answer b/Test/linear/Answer
index 69caec25..680f9895 100644
--- a/Test/linear/Answer
+++ b/Test/linear/Answer
@@ -14,6 +14,7 @@ typecheck.bpl(55,4): Error: The domains of formal and actual parameters must be
 typecheck.bpl(57,4): Error: Only a linear argument can be passed to a linear parameter
 typecheck.bpl(61,4): Error: A linear set can occur only once as an in parameter
 typecheck.bpl(66,6): Error: Only linear variable can be assigned to another linear variable
+typecheck.bpl(75,4): Error: A linear variable on the right hand side of an assignment must be in the modifies set
 0 type checking errors detected in typecheck.bpl
 
 -------------------- list.bpl --------------------
diff --git a/Test/linear/runtest.bat b/Test/linear/runtest.bat
index d054b097..5681784a 100644
--- a/Test/linear/runtest.bat
+++ b/Test/linear/runtest.bat
@@ -3,7 +3,13 @@ setlocal
 
 set BGEXE=..\..\Binaries\Boogie.exe
 
-for %%f in (typecheck.bpl list.bpl allocator.bpl) do (
+for %%f in (typecheck.bpl) do (
+  echo.
+  echo -------------------- %%f --------------------
+  %BGEXE% %* /nologo /noinfer /typeEncoding:m /useArrayTheory %%f
+)
+
+for %%f in (list.bpl allocator.bpl) do (
   echo.
   echo -------------------- %%f --------------------
   %BGEXE% %* /nologo /noinfer /typeEncoding:m /useArrayTheory /doModSetAnalysis %%f
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;
+}
-- 
cgit v1.2.3