From 41c1ea3efbbf1b5d7758ab334ab456462300f555 Mon Sep 17 00:00:00 2001
From: qadeer <unknown>
Date: Mon, 15 Dec 2014 11:33:23 -0800
Subject: 1. made variable introduction layer explicit in the test cases 2. if
 a single layer is specified for a global variable, that layer is the
 introduction layer

---
 Test/og/DeviceCache.bpl    | 8 ++++----
 Test/og/FlanaganQadeer.bpl | 4 ++--
 Test/og/Program1.bpl       | 2 +-
 Test/og/Program2.bpl       | 2 +-
 Test/og/Program3.bpl       | 2 +-
 Test/og/Program4.bpl       | 2 +-
 Test/og/akash.bpl          | 4 ++--
 Test/og/bar.bpl            | 2 +-
 Test/og/civl-paper.bpl     | 6 +++---
 Test/og/foo.bpl            | 2 +-
 Test/og/linear-set.bpl     | 4 ++--
 Test/og/linear-set2.bpl    | 4 ++--
 Test/og/lock.bpl           | 2 +-
 Test/og/lock2.bpl          | 2 +-
 Test/og/multiset.bpl       | 8 ++++----
 Test/og/new1.bpl           | 2 +-
 Test/og/one.bpl            | 2 +-
 Test/og/parallel1.bpl      | 2 +-
 Test/og/parallel2.bpl      | 2 +-
 Test/og/parallel4.bpl      | 2 +-
 Test/og/parallel5.bpl      | 2 +-
 Test/og/perm.bpl           | 2 +-
 Test/og/t1.bpl             | 4 ++--
 Test/og/ticket.bpl         | 8 ++++----
 Test/og/treiber-stack.bpl  | 6 +++---
 25 files changed, 43 insertions(+), 43 deletions(-)

(limited to 'Test')

diff --git a/Test/og/DeviceCache.bpl b/Test/og/DeviceCache.bpl
index b74b52c5..703456ef 100644
--- a/Test/og/DeviceCache.bpl
+++ b/Test/og/DeviceCache.bpl
@@ -3,10 +3,10 @@
 type X;
 function {:builtin "MapConst"} mapconstbool(bool): [X]bool;
 const nil: X;
-var {:layer 1} ghostLock: X;
-var {:layer 1} lock: X;
-var {:layer 1} currsize: int;
-var {:layer 1} newsize: int;
+var {:layer 0,1} ghostLock: X;
+var {:layer 0,1} lock: X;
+var {:layer 0,1} currsize: int;
+var {:layer 0,1} newsize: int;
 
 function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;
 function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool
diff --git a/Test/og/FlanaganQadeer.bpl b/Test/og/FlanaganQadeer.bpl
index 9eb11495..04255cf2 100644
--- a/Test/og/FlanaganQadeer.bpl
+++ b/Test/og/FlanaganQadeer.bpl
@@ -2,8 +2,8 @@
 // RUN: %diff "%s.expect" "%t"
 type X;
 const nil: X;
-var {:layer 1} l: X;
-var {:layer 1} x: int;
+var {:layer 0,1} l: X;
+var {:layer 0,1} x: int;
 
 function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;
 function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool
diff --git a/Test/og/Program1.bpl b/Test/og/Program1.bpl
index 5704b680..f405b92a 100644
--- a/Test/og/Program1.bpl
+++ b/Test/og/Program1.bpl
@@ -1,6 +1,6 @@
 // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
-var {:layer 1} x:int;
+var {:layer 0,1} x:int;
 
 procedure {:yields} {:layer 1} p() 
 requires {:layer 1} x >= 5; 
diff --git a/Test/og/Program2.bpl b/Test/og/Program2.bpl
index f9d28a5d..75c83c67 100644
--- a/Test/og/Program2.bpl
+++ b/Test/og/Program2.bpl
@@ -1,6 +1,6 @@
 // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
-var {:layer 1} x:int;
+var {:layer 0,1} x:int;
 
 procedure {:yields} {:layer 1} yield_x(n: int)
 requires {:layer 1} x >= n; 
diff --git a/Test/og/Program3.bpl b/Test/og/Program3.bpl
index ae8c6eed..f8c4e132 100644
--- a/Test/og/Program3.bpl
+++ b/Test/og/Program3.bpl
@@ -1,6 +1,6 @@
 // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
-var {:layer 1} x:int;
+var {:layer 0,1} x:int;
 
 procedure {:yields} {:layer 1} yield_x()
 ensures {:layer 1} x >= old(x); 
diff --git a/Test/og/Program4.bpl b/Test/og/Program4.bpl
index 61d4fcdc..0228adc9 100644
--- a/Test/og/Program4.bpl
+++ b/Test/og/Program4.bpl
@@ -13,7 +13,7 @@ function {:inline} {:linear "tid"} TidSetCollector(x: [Tid]bool) : [Tid]bool
   x
 }
 
-var {:layer 1} a:[Tid]int;
+var {:layer 0,1} a:[Tid]int;
 
 procedure Allocate() returns ({:linear "tid"} tid:Tid); 
 
diff --git a/Test/og/akash.bpl b/Test/og/akash.bpl
index f5d71caa..744029f1 100644
--- a/Test/og/akash.bpl
+++ b/Test/og/akash.bpl
@@ -27,8 +27,8 @@ ensures {:layer 1} xls == mapconstbool(true);
 procedure Allocate_2() returns ({:linear "2"} xls: [int]bool);
 ensures {:layer 1} xls == mapconstbool(true);
 
-var {:layer 1} g: int;
-var {:layer 1} h: int;
+var {:layer 0,1} g: int;
+var {:layer 0,1} h: int;
 
 procedure {:yields} {:layer 0,1} SetG(val:int);
 ensures {:atomic} |{A: g := val; return true; }|;
diff --git a/Test/og/bar.bpl b/Test/og/bar.bpl
index ac2ec1b6..4eef8378 100644
--- a/Test/og/bar.bpl
+++ b/Test/og/bar.bpl
@@ -1,6 +1,6 @@
 // RUN: %boogie -noinfer "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
-var {:layer 1} g:int;
+var {:layer 0,1} g:int;
 
 procedure {:yields} {:layer 1} PB()
 {
diff --git a/Test/og/civl-paper.bpl b/Test/og/civl-paper.bpl
index e6a673d8..a7042c6a 100644
--- a/Test/og/civl-paper.bpl
+++ b/Test/og/civl-paper.bpl
@@ -15,9 +15,9 @@ function map(lmap): [int]int;
 function cons([int]bool, [int]int) : lmap;
 axiom (forall x: [int]bool, y: [int]int :: {cons(x,y)} dom(cons(x, y)) == x && map(cons(x,y)) == y);
 
-var {:layer 3} {:linear "mem"} g: lmap;
-var {:layer 3} lock: X;
-var {:layer 1} b: bool;
+var {:layer 0,3} {:linear "mem"} g: lmap;
+var {:layer 0,3} lock: X;
+var {:layer 0,1} b: bool;
 
 const p: int;
 
diff --git a/Test/og/foo.bpl b/Test/og/foo.bpl
index bd8c6ef7..7eeab890 100644
--- a/Test/og/foo.bpl
+++ b/Test/og/foo.bpl
@@ -1,6 +1,6 @@
 // RUN: %boogie -noinfer "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
-var {:layer 1} g:int;
+var {:layer 0,1} g:int;
 
 procedure {:yields} {:layer 1} PB()
 {
diff --git a/Test/og/linear-set.bpl b/Test/og/linear-set.bpl
index 4b6692c5..73849250 100644
--- a/Test/og/linear-set.bpl
+++ b/Test/og/linear-set.bpl
@@ -20,8 +20,8 @@ function {:inline} {:linear "x"} XCollector(xs: [X]bool) : [X]bool
   xs
 }
 
-var {:layer 1} x: int;
-var {:layer 1} l: [X]bool;
+var {:layer 0,1} x: int;
+var {:layer 0,1} l: [X]bool;
 
 procedure Split({:linear_in "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool);
 ensures xls == MapOr(xls1, xls2) && xls1 != None() && xls2 != None();
diff --git a/Test/og/linear-set2.bpl b/Test/og/linear-set2.bpl
index 93ede868..81d30521 100644
--- a/Test/og/linear-set2.bpl
+++ b/Test/og/linear-set2.bpl
@@ -20,8 +20,8 @@ function {:inline} {:linear "x"} XCollector(xs: [X]bool) : [X]bool
   xs
 }
 
-var {:layer 1} x: int;
-var {:layer 1} l: X;
+var {:layer 0,1} x: int;
+var {:layer 0,1} l: X;
 const nil: X;
 
 procedure Split({:linear_in "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [X]bool);
diff --git a/Test/og/lock.bpl b/Test/og/lock.bpl
index db563cce..9341591f 100644
--- a/Test/og/lock.bpl
+++ b/Test/og/lock.bpl
@@ -1,6 +1,6 @@
 // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
-var {:layer 2} b: bool;
+var {:layer 0,2} b: bool;
 
 procedure {:yields} {:layer 2} main()
 {
diff --git a/Test/og/lock2.bpl b/Test/og/lock2.bpl
index 7f0dde84..4809a8f5 100644
--- a/Test/og/lock2.bpl
+++ b/Test/og/lock2.bpl
@@ -1,6 +1,6 @@
 // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
-var {:layer 2} b: int;
+var {:layer 0,2} b: int;
 
 procedure {:yields} {:layer 2} main()
 {
diff --git a/Test/og/multiset.bpl b/Test/og/multiset.bpl
index 0f56dd7e..308e4b8b 100644
--- a/Test/og/multiset.bpl
+++ b/Test/og/multiset.bpl
@@ -6,10 +6,10 @@ const unique null : int;
 const unique nil: X;
 const unique done: X;
 
-var elt : [int]int;
-var valid : [int]bool;
-var lock : [int]X;
-var owner : [int]X;
+var {:layer 0} elt : [int]int;
+var {:layer 0} valid : [int]bool;
+var {:layer 0} lock : [int]X;
+var {:layer 0} owner : [int]X;
 const max : int;
 
 function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;
diff --git a/Test/og/new1.bpl b/Test/og/new1.bpl
index 3faa9156..a6b50215 100644
--- a/Test/og/new1.bpl
+++ b/Test/og/new1.bpl
@@ -2,7 +2,7 @@
 // RUN: %diff "%s.expect" "%t"
 function {:builtin "MapConst"} mapconstbool(x:bool): [int]bool;
 
-var {:layer 1} g:int;
+var {:layer 0,1} g:int;
 
 function {:inline} {:linear "Perm"} SetCollectorPerm(x: [int]bool) : [int]bool
 {
diff --git a/Test/og/one.bpl b/Test/og/one.bpl
index 45cbbda3..663b2da0 100644
--- a/Test/og/one.bpl
+++ b/Test/og/one.bpl
@@ -1,6 +1,6 @@
 // RUN: %boogie -noinfer "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
-var {:layer 1} x:int;
+var {:layer 0,1} x:int;
 
 procedure {:yields} {:layer 0,1} Set(v: int);
 ensures {:atomic}
diff --git a/Test/og/parallel1.bpl b/Test/og/parallel1.bpl
index 96231f5b..20dd3c79 100644
--- a/Test/og/parallel1.bpl
+++ b/Test/og/parallel1.bpl
@@ -1,6 +1,6 @@
 // RUN: %boogie -noinfer "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
-var {:layer 1} g:int;
+var {:layer 0,1} g:int;
 
 procedure {:yields} {:layer 1} PB()
 {
diff --git a/Test/og/parallel2.bpl b/Test/og/parallel2.bpl
index 20de0875..4f2cbd5b 100644
--- a/Test/og/parallel2.bpl
+++ b/Test/og/parallel2.bpl
@@ -1,6 +1,6 @@
 // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
-var {:layer 1} a:[int]int;
+var {:layer 0,1} a:[int]int;
 
 function {:builtin "MapConst"} MapConstBool(bool) : [int]bool;
 function {:inline} {:linear "tid"} TidCollector(x: int) : [int]bool
diff --git a/Test/og/parallel4.bpl b/Test/og/parallel4.bpl
index bb9c631b..41d45b79 100644
--- a/Test/og/parallel4.bpl
+++ b/Test/og/parallel4.bpl
@@ -1,6 +1,6 @@
 // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
-var {:layer 1} a:int;
+var {:layer 0,1} a:int;
 
 procedure Allocate() returns ({:linear "tid"} xls: int);
 
diff --git a/Test/og/parallel5.bpl b/Test/og/parallel5.bpl
index 7ef565e1..bed51241 100644
--- a/Test/og/parallel5.bpl
+++ b/Test/og/parallel5.bpl
@@ -1,6 +1,6 @@
 // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
-var {:layer 1} a:[int]int;
+var {:layer 0,1} a:[int]int;
 
 procedure Allocate() returns ({:linear "tid"} xls: int);
 
diff --git a/Test/og/perm.bpl b/Test/og/perm.bpl
index 66ae5285..f0de76d5 100644
--- a/Test/og/perm.bpl
+++ b/Test/og/perm.bpl
@@ -1,6 +1,6 @@
 // RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
-var {:layer 1} x: int;
+var {:layer 0,1} x: int;
 function {:builtin "MapConst"} ch_mapconstbool(x: bool) : [int]bool;
 
 function {:builtin "MapOr"} ch_mapunion(x: [int]bool, y: [int]bool) : [int]bool;
diff --git a/Test/og/t1.bpl b/Test/og/t1.bpl
index 305f1ed1..b2f02bda 100644
--- a/Test/og/t1.bpl
+++ b/Test/og/t1.bpl
@@ -27,8 +27,8 @@ ensures {:layer 1} xls == mapconstbool(true);
 procedure Allocate_2() returns ({:linear "2"} xls: [int]bool);
 ensures {:layer 1} xls == mapconstbool(true);
 
-var {:layer 1} g: int;
-var {:layer 1} h: int;
+var {:layer 0,1} g: int;
+var {:layer 0,1} h: int;
 
 procedure {:yields} {:layer 0,1} SetG(val:int);
 ensures {:atomic} |{A: g := val; return true; }|;
diff --git a/Test/og/ticket.bpl b/Test/og/ticket.bpl
index 70fe1d4c..f875d6e5 100644
--- a/Test/og/ticket.bpl
+++ b/Test/og/ticket.bpl
@@ -8,10 +8,10 @@ axiom (forall x: int, y: int :: RightClosed(x)[y] <==> y <= x);
 type X;
 function {:builtin "MapConst"} mapconstbool(bool): [X]bool;
 const nil: X;
-var {:layer 2} t: int;
-var {:layer 2} s: int;
-var {:layer 2} cs: X;
-var {:layer 2} T: [int]bool;
+var {:layer 0,2} t: int;
+var {:layer 0,2} s: int;
+var {:layer 0,2} cs: X;
+var {:layer 0,2} T: [int]bool;
 
 function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;
 function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool
diff --git a/Test/og/treiber-stack.bpl b/Test/og/treiber-stack.bpl
index 47dcc515..9a612eb2 100644
--- a/Test/og/treiber-stack.bpl
+++ b/Test/og/treiber-stack.bpl
@@ -38,8 +38,8 @@ ensures {:atomic} |{ A: goto B,C;
                         B: assume oldVal == TopOfStack; TopOfStack := newVal; Used := Add(Used, oldVal, map(Stack)[oldVal]); Stack := Remove(Stack, oldVal); r := true; return true;
 		        C: assume oldVal != TopOfStack; r := false; return true; }|;
 
-var TopOfStack: Node;
-var {:linear "Node"} Stack: lmap;
+var {:layer 0} TopOfStack: Node;
+var {:linear "Node"} {:layer 0} Stack: lmap;
 
 
 function {:inline} Inv(TopOfStack: Node, Stack: lmap) : (bool)
@@ -48,7 +48,7 @@ function {:inline} Inv(TopOfStack: Node, Stack: lmap) : (bool)
   Subset(Difference(BetweenSet(map(Stack), TopOfStack, null), Singleton(null)), dom(Stack))
 }
 
-var {:linear "Node"} Used: lmap;
+var {:linear "Node"} {:layer 0} Used: lmap;
 
 procedure {:yields} {:layer 1} push(x: Node, {:linear_in "Node"} x_lmap: lmap)
 requires {:layer 1} dom(x_lmap)[x];
-- 
cgit v1.2.3