diff options
| author |  qadeer <unknown> | 2013-07-14 21:56:51 -0700 |
|---|---|---|
| committer | qadeer <unknown> | 2013-07-14 21:56:51 -0700 |
| commit | 4ef06586c73b8337c87d6b129315365b6ed6d96b (patch) | |
| tree | f367e1b10dde0e89c93b15ea06e6ffd42a7b6c7e /Test/linear | |
| parent | 58570d4912e129e3e8807f005b871fd5495006d5 (diff) | |
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
Diffstat (limited to 'Test/linear')
| -rw-r--r-- | Test/linear/typecheck.bpl | 21 |
1 files changed, 21 insertions, 0 deletions
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();
+}
|