From 4ef06586c73b8337c87d6b129315365b6ed6d96b Mon Sep 17 00:00:00 2001
From: qadeer <unknown>
Date: Sun, 14 Jul 2013 21:56:51 -0700
Subject: 1. changed values passed to additional parameters to procedures;
 async and parallel calls treated exactly the same now 2. fixed bug in
 collection of available linear vars for parallel calls; added more test cases
 to regression

---
 Test/linear/typecheck.bpl | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

(limited to 'Test/linear')

diff --git a/Test/linear/typecheck.bpl b/Test/linear/typecheck.bpl
index 7bdb339e..ebd3d07d 100644
--- a/Test/linear/typecheck.bpl
+++ b/Test/linear/typecheck.bpl
@@ -80,3 +80,24 @@ modifies g;
 {
   g := r;
 }
+
+procedure I({:linear ""} x:int) returns({:linear ""} x':int)
+{
+  x' := x;
+}
+
+procedure J()
+{
+}
+
+procedure P1({:linear ""} x:int) returns({:linear ""} x':int)
+{
+  call x' := I(x) | J();
+  call x' := I(x');
+}
+
+procedure P2({:linear ""} x:int) returns({:linear ""} x':int)
+{
+  call x' := I(x);
+  call x' := I(x') | J();
+}
-- 
cgit v1.2.3