summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
authorGravatar Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com>2013-03-13 10:02:01 -0700
committerGravatar Unknown <qadeer@FAIZ-AHMED-FAIZ.redmond.corp.microsoft.com>2013-03-13 10:02:01 -0700
commitdf2694faaf9b53d4b609270c431c76ec5b2068ff (patch)
treea9f969b405b3f66d9b7a2f4e0f666b064deeb363 /Test
parentc344350ef8cc83b5e0aa9332435fbe095bc84bc0 (diff)
added mod set checking to the linear type checker
Diffstat (limited to 'Test')
-rw-r--r--Test/linear/Answer1
-rw-r--r--Test/linear/runtest.bat8
-rw-r--r--Test/linear/typecheck.bpl9
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;
+}