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

25 files changed, 43 insertions, 43 deletions

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];