added mod set checking to the linear type checker

3 files changed, 16 insertions, 2 deletions

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;

+}