summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/Concurrency/LinearSets.cs102
-rw-r--r--Test/linear/allocator.bpl4
-rw-r--r--Test/linear/async-bug.bpl9
-rw-r--r--Test/linear/async-bug.bpl.expect4
-rw-r--r--Test/linear/f1.bpl4
-rw-r--r--Test/linear/f2.bpl4
-rw-r--r--Test/linear/f3.bpl2
-rw-r--r--Test/linear/list.bpl2
-rw-r--r--Test/linear/typecheck.bpl10
-rw-r--r--Test/og/DeviceCache.bpl34
-rw-r--r--Test/og/FlanaganQadeer.bpl4
-rw-r--r--Test/og/Program4.bpl6
-rw-r--r--Test/og/Program5.bpl12
-rw-r--r--Test/og/akash.bpl6
-rw-r--r--Test/og/civl-paper.bpl14
-rw-r--r--Test/og/linear-set.bpl6
-rw-r--r--Test/og/linear-set2.bpl6
-rw-r--r--Test/og/lock-introduced.bpl8
-rw-r--r--Test/og/multiset.bpl22
-rw-r--r--Test/og/new1.bpl6
-rw-r--r--Test/og/parallel2.bpl6
-rw-r--r--Test/og/parallel4.bpl2
-rw-r--r--Test/og/parallel5.bpl6
-rw-r--r--Test/og/perm.bpl6
-rw-r--r--Test/og/t1.bpl6
-rw-r--r--Test/og/ticket.bpl18
-rw-r--r--Test/og/treiber-stack.bpl6
27 files changed, 179 insertions, 136 deletions
diff --git a/Source/Concurrency/LinearSets.cs b/Source/Concurrency/LinearSets.cs
index 9e649551..f9a791bc 100644
--- a/Source/Concurrency/LinearSets.cs
+++ b/Source/Concurrency/LinearSets.cs
@@ -14,7 +14,7 @@ namespace Microsoft.Boogie
{
if (iter == null) return null;
iter.Next = RemoveLinearAttribute(iter.Next);
- return (iter.Key == "linear" || iter.Key == "cnst") ? iter.Next : iter;
+ return (iter.Key == "linear" || iter.Key == "linear_in" || iter.Key == "linear_out") ? iter.Next : iter;
}
public override Variable VisitVariable(Variable node)
@@ -26,7 +26,8 @@ namespace Microsoft.Boogie
public enum LinearKind {
LINEAR,
- CONST
+ LINEAR_IN,
+ LINEAR_OUT
}
public class LinearTypeChecker : ReadOnlyVisitor
@@ -166,8 +167,12 @@ namespace Microsoft.Boogie
string domainName = FindDomainName(v);
if (domainName != null)
{
- inParamToLinearQualifier[node.InParams[i]] = new LinearQualifier(domainName, FindLinearKind(v));
- start.Add(node.InParams[i]);
+ var kind = FindLinearKind(v);
+ inParamToLinearQualifier[node.InParams[i]] = new LinearQualifier(domainName, kind);
+ if (kind == LinearKind.LINEAR || kind == LinearKind.LINEAR_IN)
+ {
+ start.Add(node.InParams[i]);
+ }
}
}
for (int i = 0; i < node.OutParams.Count; i++)
@@ -200,6 +205,11 @@ namespace Microsoft.Boogie
{
Error(b.TransferCmd, string.Format("Global variable {0} must be available at a return", g.Name));
}
+ foreach (Variable v in node.InParams)
+ {
+ if (FindDomainName(v) == null || FindLinearKind(v) == LinearKind.LINEAR_IN || end.Contains(v)) continue;
+ Error(b.TransferCmd, string.Format("Input variable {0} must be available at a return", v.Name));
+ }
foreach (Variable v in node.OutParams)
{
if (FindDomainName(v) == null || end.Contains(v)) continue;
@@ -253,8 +263,11 @@ namespace Microsoft.Boogie
IdentifierExpr ie = callCmd.Ins[i] as IdentifierExpr;
if (ie == null) continue;
Variable v = callCmd.Proc.InParams[i];
- if (FindDomainName(v) == null || FindLinearKind(v) == LinearKind.LINEAR) continue;
- start.Add(ie.Decl);
+ if (FindDomainName(v) == null) continue;
+ if (FindLinearKind(v) == LinearKind.LINEAR_OUT)
+ {
+ start.Add(ie.Decl);
+ }
}
}
public void AddAvailableVars(ParCallCmd parCallCmd, HashSet<Variable> start)
@@ -279,10 +292,6 @@ namespace Microsoft.Boogie
{
Error(ie, "unavailable source for a linear read");
}
- else if (FindLinearKind(ie.Decl) == LinearKind.CONST)
- {
- Error(ie, "const linear vars cannot occur on the right side of a linear assignment");
- }
else
{
start.Remove(ie.Decl);
@@ -303,15 +312,27 @@ namespace Microsoft.Boogie
CallCmd callCmd = (CallCmd)cmd;
for (int i = 0; i < callCmd.Proc.InParams.Count; i++)
{
- if (FindDomainName(callCmd.Proc.InParams[i]) == null) continue;
+ Variable param = callCmd.Proc.InParams[i];
+ if (FindDomainName(param) == null) continue;
IdentifierExpr ie = callCmd.Ins[i] as IdentifierExpr;
+ LinearKind paramKind = FindLinearKind(param);
if (start.Contains(ie.Decl))
{
- start.Remove(ie.Decl);
+ if (callCmd.IsAsync || paramKind == LinearKind.LINEAR_IN)
+ {
+ start.Remove(ie.Decl);
+ }
}
else
{
- Error(ie, "unavailable source for a linear read");
+ if (paramKind == LinearKind.LINEAR_OUT)
+ {
+ start.Add(ie.Decl);
+ }
+ else
+ {
+ Error(ie, "unavailable source for a linear read");
+ }
}
}
availableLinearVars[callCmd] = new HashSet<Variable>(start);
@@ -328,15 +349,27 @@ namespace Microsoft.Boogie
{
for (int i = 0; i < callCmd.Proc.InParams.Count; i++)
{
- if (FindDomainName(callCmd.Proc.InParams[i]) == null) continue;
+ Variable param = callCmd.Proc.InParams[i];
+ if (FindDomainName(param) == null) continue;
IdentifierExpr ie = callCmd.Ins[i] as IdentifierExpr;
+ LinearKind paramKind = FindLinearKind(param);
if (start.Contains(ie.Decl))
{
- start.Remove(ie.Decl);
+ if (paramKind == LinearKind.LINEAR_IN)
+ {
+ start.Remove(ie.Decl);
+ }
}
else
{
- Error(ie, "unavailable source for a linear read");
+ if (paramKind == LinearKind.LINEAR_OUT)
+ {
+ start.Add(ie.Decl);
+ }
+ else
+ {
+ Error(ie, "unavailable source for a linear read");
+ }
}
}
}
@@ -374,7 +407,10 @@ namespace Microsoft.Boogie
string domainName = QKeyValue.FindStringAttribute(v.Attributes, "linear");
if (domainName != null)
return domainName;
- return QKeyValue.FindStringAttribute(v.Attributes, "cnst");
+ domainName = QKeyValue.FindStringAttribute(v.Attributes, "linear_in");
+ if (domainName != null)
+ return domainName;
+ return QKeyValue.FindStringAttribute(v.Attributes, "linear_out");
}
public LinearKind FindLinearKind(Variable v)
{
@@ -385,18 +421,22 @@ namespace Microsoft.Boogie
if (outParamToDomainName.ContainsKey(v))
return LinearKind.LINEAR;
- if (QKeyValue.FindStringAttribute(v.Attributes, "cnst") != null)
+ if (QKeyValue.FindStringAttribute(v.Attributes, "linear") != null)
{
- return LinearKind.CONST;
+ return LinearKind.LINEAR;
}
- else if (QKeyValue.FindStringAttribute(v.Attributes, "linear") != null)
+ else if (QKeyValue.FindStringAttribute(v.Attributes, "linear_in") != null)
{
- return LinearKind.LINEAR;
+ return LinearKind.LINEAR_IN;
+ }
+ else if (QKeyValue.FindStringAttribute(v.Attributes, "linear_out") != null)
+ {
+ return LinearKind.LINEAR_OUT;
}
else
{
Debug.Assert(false);
- return LinearKind.CONST;
+ return LinearKind.LINEAR;
}
}
public override Variable VisitVariable(Variable node)
@@ -408,6 +448,14 @@ namespace Microsoft.Boogie
{
domainNameToCollectors[domainName] = new Dictionary<Type,Function>();
}
+ LinearKind kind = FindLinearKind(node);
+ if (kind != LinearKind.LINEAR)
+ {
+ if (node is GlobalVariable || node is LocalVariable || (node is Formal && !(node as Formal).InComing))
+ {
+ Error(node, "Variable must be declared linear (as opposed to linear_in or linear_out)");
+ }
+ }
}
return base.VisitVariable(node);
}
@@ -482,16 +530,6 @@ namespace Microsoft.Boogie
Error(node, "Only local linear variable can be an actual input parameter of a procedure call");
continue;
}
- if (FindLinearKind(actual.Decl) == LinearKind.CONST && FindLinearKind(formal) == LinearKind.LINEAR)
- {
- Error(node, "Const linear variable cannot be an argument for a linear input parameter of a procedure call");
- continue;
- }
- if (FindLinearKind(actual.Decl) == LinearKind.CONST && FindLinearKind(formal) == LinearKind.CONST && node.IsAsync)
- {
- Error(node, "Const linear variable cannot be an argument for a const parameter of an async procedure call");
- continue;
- }
if (inVars.Contains(actual.Decl))
{
Error(node, string.Format("Linear variable {0} can occur only once as an input parameter", actual.Decl.Name));
diff --git a/Test/linear/allocator.bpl b/Test/linear/allocator.bpl
index 31f54f7e..147d700f 100644
--- a/Test/linear/allocator.bpl
+++ b/Test/linear/allocator.bpl
@@ -1,9 +1,9 @@
// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory -doModSetAnalysis "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
-procedure A({:linear "tid"} i': int) returns ({:linear "tid"} i: int);
+procedure A({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int);
ensures i == i';
-procedure{:entrypoint} B({:linear "tid"} i': int) returns ({:linear "tid"} i: int)
+procedure B({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int)
{
i := i';
call i := A(i);
diff --git a/Test/linear/async-bug.bpl b/Test/linear/async-bug.bpl
index faa1a65d..ff6cdded 100644
--- a/Test/linear/async-bug.bpl
+++ b/Test/linear/async-bug.bpl
@@ -2,12 +2,17 @@
// RUN: %diff "%s.expect" "%t"
const GcTid:int;
-procedure {:yields} {:phase 100} Initialize({:cnst "tid"} tid:int)
+procedure {:yields} {:phase 100} Initialize({:linear "tid"} tid:int)
requires{:phase 100} tid == GcTid;
{
yield;
assert{:phase 100} tid == GcTid;
+ call GarbageCollect(tid);
+
+ yield;
+ assert{:phase 100} tid == GcTid;
+
async call GarbageCollect(tid);
yield;
@@ -22,7 +27,7 @@ requires{:phase 100} tid == GcTid;
assert{:phase 100} tid == GcTid;
}
-procedure {:yields} {:phase 100} GarbageCollect({:cnst "tid"} tid:int)
+procedure {:yields} {:phase 100} GarbageCollect({:linear "tid"} tid:int)
requires{:phase 100} tid == GcTid;
{
yield;
diff --git a/Test/linear/async-bug.bpl.expect b/Test/linear/async-bug.bpl.expect
index 8bfe61d1..73a5eaee 100644
--- a/Test/linear/async-bug.bpl.expect
+++ b/Test/linear/async-bug.bpl.expect
@@ -1,3 +1,3 @@
-async-bug.bpl(11,10): Error: Const linear variable cannot be an argument for a const parameter of an async procedure call
-async-bug.bpl(16,10): Error: Const linear variable cannot be an argument for a const parameter of an async procedure call
+async-bug.bpl(21,30): Error: unavailable source for a linear read
+async-bug.bpl(28,0): Error: Input variable tid must be available at a return
2 type checking errors detected in async-bug.bpl
diff --git a/Test/linear/f1.bpl b/Test/linear/f1.bpl
index e18fab9f..0d255149 100644
--- a/Test/linear/f1.bpl
+++ b/Test/linear/f1.bpl
@@ -21,7 +21,7 @@ axiom(!b6);
axiom(!b7);
axiom(b8);
-procedure {:entrypoint} main({:linear "1"} x_in: [int]bool)
+procedure main({:linear_in "1"} x_in: [int]bool)
requires b0 ==> x_in == mapconstbool(true);
requires b1 ==> x_in != mapconstbool(false);
{
@@ -35,7 +35,7 @@ procedure {:entrypoint} main({:linear "1"} x_in: [int]bool)
assert b8 ==> x == mapconstbool(false);
}
-procedure foo({:linear "1"} x_in: [int]bool)
+procedure foo({:linear_in "1"} x_in: [int]bool)
requires b2 ==> x_in == mapconstbool(true);
requires b3 ==> x_in != mapconstbool(false);
{
diff --git a/Test/linear/f2.bpl b/Test/linear/f2.bpl
index 16863154..18f518da 100644
--- a/Test/linear/f2.bpl
+++ b/Test/linear/f2.bpl
@@ -3,12 +3,12 @@
function {:builtin "MapConst"} mapconstbool(bool) : [int]bool;
function {:builtin "MapOr"} mapunion([int]bool, [int]bool) : [int]bool;
-procedure Split({:linear "1"} xls: [int]bool) returns ({:linear "1"} xls1: [int]bool, {:linear "1"} xls2: [int]bool);
+procedure Split({:linear_in "1"} xls: [int]bool) returns ({:linear "1"} xls1: [int]bool, {:linear "1"} xls2: [int]bool);
ensures xls == mapunion(xls1, xls2) && xls1 != mapconstbool(false) && xls2 != mapconstbool(false);
procedure Allocate() returns ({:linear "1"} x: [int]bool);
-procedure {:entrypoint} main()
+procedure main()
{
var {:linear "1"} x: [int] bool;
var {:linear "1"} x1: [int] bool;
diff --git a/Test/linear/f3.bpl b/Test/linear/f3.bpl
index f5e08277..3a0e855c 100644
--- a/Test/linear/f3.bpl
+++ b/Test/linear/f3.bpl
@@ -2,7 +2,7 @@
// RUN: %diff "%s.expect" "%t"
procedure A() {}
-procedure B({:linear ""} tid:int) returns({:linear ""} tid':int)
+procedure B({:linear_in ""} tid:int) returns({:linear ""} tid':int)
{
tid' := tid;
call A();
diff --git a/Test/linear/list.bpl b/Test/linear/list.bpl
index 72f165fb..804cb7e2 100644
--- a/Test/linear/list.bpl
+++ b/Test/linear/list.bpl
@@ -18,7 +18,7 @@ const nil: X;
procedure malloc() returns (x: X, {:linear "Mem"} M: [X]bool);
ensures M == MapConstBool(false)[x := true];
-procedure Join({:linear "Mem"} A: [X]bool);
+procedure Join({:linear_in "Mem"} A: [X]bool);
modifies D;
ensures MapOr(old(D), A) == D;
diff --git a/Test/linear/typecheck.bpl b/Test/linear/typecheck.bpl
index a3980a3e..057718cf 100644
--- a/Test/linear/typecheck.bpl
+++ b/Test/linear/typecheck.bpl
@@ -65,12 +65,12 @@ procedure {:yields} {:phase 1} D()
yield;
}
-procedure E({:linear "D"} a: X, {:linear "D"} b: X) returns ({:linear "D"} c: X, {:linear "D"} d: X)
+procedure E({:linear_in "D"} a: X, {:linear_in "D"} b: X) returns ({:linear "D"} c: X, {:linear "D"} d: X)
{
c := a;
}
-procedure {:yields} {:phase 0} F({:linear "D"} a: X) returns ({:linear "D"} c: X);
+procedure {:yields} {:phase 0} F({:linear_in "D"} a: X) returns ({:linear "D"} c: X);
var {:linear "x"} g:int;
@@ -85,7 +85,7 @@ modifies g;
g := r;
}
-procedure {:yields} {:phase 0} I({:linear ""} x:int) returns({:linear ""} x':int)
+procedure {:yields} {:phase 0} I({:linear_in ""} x:int) returns({:linear ""} x':int)
{
x' := x;
}
@@ -94,7 +94,7 @@ procedure {:yields} {:phase 0} J()
{
}
-procedure {:yields} {:phase 1} P1({:linear ""} x:int) returns({:linear ""} x':int)
+procedure {:yields} {:phase 1} P1({:linear_in ""} x:int) returns({:linear ""} x':int)
{
yield;
par x' := I(x) | J();
@@ -103,7 +103,7 @@ procedure {:yields} {:phase 1} P1({:linear ""} x:int) returns({:linear ""} x':in
yield;
}
-procedure {:yields} {:phase 1} P2({:linear ""} x:int) returns({:linear ""} x':int)
+procedure {:yields} {:phase 1} P2({:linear_in ""} x:int) returns({:linear ""} x':int)
{
yield;
call x' := I(x);
diff --git a/Test/og/DeviceCache.bpl b/Test/og/DeviceCache.bpl
index e7e3abe9..ad75f1f9 100644
--- a/Test/og/DeviceCache.bpl
+++ b/Test/og/DeviceCache.bpl
@@ -24,7 +24,7 @@ function {:inline} Inv(ghostLock: X, currsize: int, newsize: int) : (bool)
(ghostLock == nil <==> currsize == newsize)
}
-procedure {:yields} {:phase 1} YieldToReadCache({:cnst "tid"} tid: X)
+procedure {:yields} {:phase 1} YieldToReadCache({:linear "tid"} tid: X)
requires {:phase 1} Inv(ghostLock, currsize, newsize) && tid != nil;
ensures {:phase 1} Inv(ghostLock, currsize, newsize) && old(currsize) <= currsize;
{
@@ -32,7 +32,7 @@ ensures {:phase 1} Inv(ghostLock, currsize, newsize) && old(currsize) <= currsiz
assert {:phase 1} Inv(ghostLock, currsize, newsize) && old(currsize) <= currsize;
}
-procedure {:yields} {:phase 1} YieldToWriteCache({:cnst "tid"} tid: X)
+procedure {:yields} {:phase 1} YieldToWriteCache({:linear "tid"} tid: X)
requires {:phase 1} Inv(ghostLock, currsize, newsize) && ghostLock == tid && tid != nil;
ensures {:phase 1} Inv(ghostLock, currsize, newsize) && ghostLock == tid && old(currsize) == currsize && old(newsize) == newsize;
{
@@ -40,10 +40,10 @@ ensures {:phase 1} Inv(ghostLock, currsize, newsize) && ghostLock == tid && old(
assert {:phase 1} Inv(ghostLock, currsize, newsize) && tid != nil && ghostLock == tid && old(currsize) == currsize && old(newsize) == newsize;
}
-procedure Allocate({:linear "tid"} xls': [X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X);
+procedure Allocate({:linear_in "tid"} xls': [X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X);
ensures {:phase 1} xl != nil;
-procedure {:yields} {:phase 1} main({:linear "tid"} xls':[X]bool)
+procedure {:yields} {:phase 1} main({:linear_in "tid"} xls':[X]bool)
requires {:phase 1} xls' == mapconstbool(true);
{
var {:linear "tid"} tid: X;
@@ -70,7 +70,7 @@ requires {:phase 1} xls' == mapconstbool(true);
yield;
}
-procedure {:yields} {:phase 1} Thread({:cnst "tid"} tid: X)
+procedure {:yields} {:phase 1} Thread({:linear "tid"} tid: X)
requires {:phase 1} tid != nil;
requires {:phase 1} Inv(ghostLock, currsize, newsize);
{
@@ -81,7 +81,7 @@ requires {:phase 1} Inv(ghostLock, currsize, newsize);
call bytesRead := Read(tid, start, size);
}
-procedure {:yields} {:phase 1} Read({:cnst "tid"} tid: X, start : int, size : int) returns (bytesRead : int)
+procedure {:yields} {:phase 1} Read({:linear "tid"} tid: X, start : int, size : int) returns (bytesRead : int)
requires {:phase 1} tid != nil;
requires {:phase 1} 0 <= start && 0 <= size;
requires {:phase 1} Inv(ghostLock, currsize, newsize);
@@ -121,7 +121,7 @@ COPY_TO_BUFFER:
call ReadCache(tid, start, bytesRead);
}
-procedure {:yields} {:phase 1} WriteCache({:cnst "tid"} tid: X, index: int)
+procedure {:yields} {:phase 1} WriteCache({:linear "tid"} tid: X, index: int)
requires {:phase 1} Inv(ghostLock, currsize, newsize);
requires {:phase 1} ghostLock == tid && tid != nil;
ensures {:phase 1} ghostLock == tid;
@@ -142,7 +142,7 @@ ensures {:phase 1} Inv(ghostLock, currsize, newsize) && old(currsize) == currsiz
par YieldToWriteCache(tid);
}
-procedure {:yields} {:phase 1} ReadCache({:cnst "tid"} tid: X, start: int, bytesRead: int)
+procedure {:yields} {:phase 1} ReadCache({:linear "tid"} tid: X, start: int, bytesRead: int)
requires {:phase 1} Inv(ghostLock, currsize, newsize);
requires {:phase 1} tid != nil;
requires {:phase 1} 0 <= start && 0 <= bytesRead;
@@ -168,29 +168,29 @@ ensures {:phase 1} Inv(ghostLock, currsize, newsize);
par YieldToReadCache(tid);
}
-procedure {:yields} {:phase 0,1} Init({:cnst "tid"} xls:[X]bool);
+procedure {:yields} {:phase 0,1} Init({:linear "tid"} xls:[X]bool);
ensures {:atomic} |{ A: assert xls == mapconstbool(true); currsize := 0; newsize := 0; lock := nil; ghostLock := nil; return true; }|;
-procedure {:yields} {:phase 0,1} ReadCurrsize({:cnst "tid"} tid: X) returns (val: int);
+procedure {:yields} {:phase 0,1} ReadCurrsize({:linear "tid"} tid: X) returns (val: int);
ensures {:right} |{A: assert tid != nil; assert lock == tid || ghostLock == tid; val := currsize; return true; }|;
-procedure {:yields} {:phase 0,1} ReadNewsize({:cnst "tid"} tid: X) returns (val: int);
+procedure {:yields} {:phase 0,1} ReadNewsize({:linear "tid"} tid: X) returns (val: int);
ensures {:right} |{A: assert tid != nil; assert lock == tid || ghostLock == tid; val := newsize; return true; }|;
-procedure {:yields} {:phase 0,1} WriteNewsize({:cnst "tid"} tid: X, val: int);
+procedure {:yields} {:phase 0,1} WriteNewsize({:linear "tid"} tid: X, val: int);
ensures {:atomic} |{A: assert tid != nil; assert lock == tid && ghostLock == nil; newsize := val; ghostLock := tid; return true; }|;
-procedure {:yields} {:phase 0,1} WriteCurrsize({:cnst "tid"} tid: X, val: int);
+procedure {:yields} {:phase 0,1} WriteCurrsize({:linear "tid"} tid: X, val: int);
ensures {:atomic} |{A: assert tid != nil; assert lock == tid && ghostLock == tid; currsize := val; ghostLock := nil; return true; }|;
-procedure {:yields} {:phase 0,1} ReadCacheEntry({:cnst "tid"} tid: X, index: int);
+procedure {:yields} {:phase 0,1} ReadCacheEntry({:linear "tid"} tid: X, index: int);
ensures {:atomic} |{ A: assert 0 <= index && index < currsize; return true; }|;
-procedure {:yields} {:phase 0,1} WriteCacheEntry({:cnst "tid"} tid: X, index: int);
+procedure {:yields} {:phase 0,1} WriteCacheEntry({:linear "tid"} tid: X, index: int);
ensures {:right} |{ A: assert tid != nil; assert currsize <= index && ghostLock == tid; return true; }|;
-procedure {:yields} {:phase 0,1} acquire({:cnst "tid"} tid: X);
+procedure {:yields} {:phase 0,1} acquire({:linear "tid"} tid: X);
ensures {:right} |{ A: assert tid != nil; assume lock == nil; lock := tid; return true; }|;
-procedure {:yields} {:phase 0,1} release({:cnst "tid"} tid: X);
+procedure {:yields} {:phase 0,1} release({:linear "tid"} tid: X);
ensures {:left} |{ A: assert tid != nil; assert lock == tid; lock := nil; return true; }|;
diff --git a/Test/og/FlanaganQadeer.bpl b/Test/og/FlanaganQadeer.bpl
index de2faaa8..1e98fa6d 100644
--- a/Test/og/FlanaganQadeer.bpl
+++ b/Test/og/FlanaganQadeer.bpl
@@ -38,7 +38,7 @@ ensures {:atomic} |{A: l := nil; return true; }|;
procedure {:yields} {:phase 0,1} Set(val: int);
ensures {:atomic} |{A: x := val; return true; }|;
-procedure {:yields} {:phase 1} foo({:linear "tid"} tid': X, val: int)
+procedure {:yields} {:phase 1} foo({:linear_in "tid"} tid': X, val: int)
requires {:phase 1} tid' != nil;
{
var {:linear "tid"} tid: X;
@@ -55,7 +55,7 @@ requires {:phase 1} tid' != nil;
yield;
}
-procedure {:yields} {:phase 1} Yield({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X)
+procedure {:yields} {:phase 1} Yield({:linear_in "tid"} tid': X) returns ({:linear "tid"} tid: X)
requires {:phase 1} tid' != nil;
ensures {:phase 1} tid == tid';
ensures {:phase 1} old(l) == tid ==> old(l) == l && old(x) == x;
diff --git a/Test/og/Program4.bpl b/Test/og/Program4.bpl
index c936cab7..d189ee44 100644
--- a/Test/og/Program4.bpl
+++ b/Test/og/Program4.bpl
@@ -31,7 +31,7 @@ procedure {:yields} {:phase 1} main() {
yield;
}
-procedure {:yields} {:phase 1} P({:cnst "tid"} tid: Tid)
+procedure {:yields} {:phase 1} P({:linear "tid"} tid: Tid)
ensures {:phase 1} a[tid] == old(a)[tid] + 1;
{
var t:int;
@@ -46,13 +46,13 @@ ensures {:phase 1} a[tid] == old(a)[tid] + 1;
assert {:phase 1} a[tid] == t + 1;
}
-procedure {:yields} {:phase 0,1} Read({:cnst "tid"} tid: Tid) returns (val: int);
+procedure {:yields} {:phase 0,1} Read({:linear "tid"} tid: Tid) returns (val: int);
ensures {:atomic}
|{A:
val := a[tid]; return true;
}|;
-procedure {:yields} {:phase 0,1} Write({:cnst "tid"} tid: Tid, val: int);
+procedure {:yields} {:phase 0,1} Write({:linear "tid"} tid: Tid, val: int);
ensures {:atomic}
|{A:
a[tid] := val; return true;
diff --git a/Test/og/Program5.bpl b/Test/og/Program5.bpl
index 845bf1a4..09ff8d4e 100644
--- a/Test/og/Program5.bpl
+++ b/Test/og/Program5.bpl
@@ -26,22 +26,22 @@ function {:inline} White(i:int) returns(bool) { i == 1 }
function {:inline} Gray(i:int) returns(bool) { i == 2 }
function {:inline} Black(i:int) returns(bool) { i >= 3 }
-procedure {:yields} {:phase 0,1} AcquireLock({:cnst "tid"} tid: Tid);
+procedure {:yields} {:phase 0,1} AcquireLock({:linear "tid"} tid: Tid);
ensures {:right} |{ A: assert tid != nil;
assume lock == nil;
lock := tid;
return true; }|;
-procedure {:yields} {:phase 0,1} ReleaseLock({:cnst "tid"} tid: Tid);
+procedure {:yields} {:phase 0,1} ReleaseLock({:linear "tid"} tid: Tid);
ensures {:left} |{ A: assert tid != nil;
assert lock == tid;
lock := nil;
return true; }|;
-procedure {:yields} {:phase 0,1} SetColorLocked({:cnst "tid"} tid:Tid, newCol:int);
+procedure {:yields} {:phase 0,1} SetColorLocked({:linear "tid"} tid:Tid, newCol:int);
ensures {:atomic} |{A: assert tid != nil; assert lock == tid; Color := newCol; return true;}|;
-procedure {:yields} {:phase 0,1} GetColorLocked({:cnst "tid"} tid:Tid) returns (col:int);
+procedure {:yields} {:phase 0,1} GetColorLocked({:linear "tid"} tid:Tid) returns (col:int);
ensures {:both} |{A: assert tid != nil; assert lock == tid; col := Color; return true;}|;
procedure {:yields} {:phase 1,2} GetColorNoLock() returns (col:int);
@@ -55,7 +55,7 @@ ensures {:phase 2} Color >= old(Color);
}
-procedure {:yields} {:phase 2,3} TopWriteBarrier({:cnst "tid"} tid:Tid)
+procedure {:yields} {:phase 2,3} TopWriteBarrier({:linear "tid"} tid:Tid)
ensures {:atomic} |{ A: assert tid != nil;
goto B, C;
B: assume White(Color);
@@ -76,7 +76,7 @@ ensures {:atomic} |{ A: assert tid != nil;
yield;
}
-procedure {:yields} {:phase 1,2} MidWriteBarrier({:cnst "tid"} tid:Tid)
+procedure {:yields} {:phase 1,2} MidWriteBarrier({:linear "tid"} tid:Tid)
ensures {:atomic} |{ A: assert tid != nil;
goto B, C;
B: assume White(Color);
diff --git a/Test/og/akash.bpl b/Test/og/akash.bpl
index ce435c51..f3a4235e 100644
--- a/Test/og/akash.bpl
+++ b/Test/og/akash.bpl
@@ -36,7 +36,7 @@ ensures {:atomic} |{A: g := val; return true; }|;
procedure {:yields} {:phase 0,1} SetH(val:int);
ensures {:atomic} |{A: h := val; return true; }|;
-procedure {:yields} {:phase 1} A({:linear "tid"} tid_in: int) returns ({:linear "tid"} tid_out: int)
+procedure {:yields} {:phase 1} A({:linear_in "tid"} tid_in: int) returns ({:linear "tid"} tid_out: int)
{
var {:linear "1"} x: [int]bool;
var {:linear "2"} y: [int]bool;
@@ -67,7 +67,7 @@ procedure {:yields} {:phase 1} A({:linear "tid"} tid_in: int) returns ({:linear
yield;
}
-procedure {:yields} {:phase 1} B({:linear "tid"} tid_in: int, {:linear "1"} x_in: [int]bool)
+procedure {:yields} {:phase 1} B({:linear_in "tid"} tid_in: int, {:linear_in "1"} x_in: [int]bool)
requires {:phase 1} x_in != mapconstbool(false);
{
var {:linear "tid"} tid_out: int;
@@ -86,7 +86,7 @@ requires {:phase 1} x_in != mapconstbool(false);
yield;
}
-procedure {:yields} {:phase 1} C({:linear "tid"} tid_in: int, {:linear "2"} y_in: [int]bool)
+procedure {:yields} {:phase 1} C({:linear_in "tid"} tid_in: int, {:linear_in "2"} y_in: [int]bool)
requires {:phase 1} y_in != mapconstbool(false);
{
var {:linear "tid"} tid_out: int;
diff --git a/Test/og/civl-paper.bpl b/Test/og/civl-paper.bpl
index 48394f92..eadf81e3 100644
--- a/Test/og/civl-paper.bpl
+++ b/Test/og/civl-paper.bpl
@@ -19,27 +19,27 @@ var {:phase 2} {:linear "mem"} g: lmap;
const p: int;
-procedure {:yields} {:phase 1,2} TransferToGlobal({:cnst "tid"} tid: X, {:linear "mem"} l: lmap);
+procedure {:yields} {:phase 1,2} TransferToGlobal({:linear "tid"} tid: X, {:linear_in "mem"} l: lmap);
ensures {:both} |{ A: assert tid != nil && lock == tid; g := l; return true; }|;
requires {:phase 1} InvLock(lock, b);
ensures {:phase 1} InvLock(lock, b);
-procedure {:yields} {:phase 1,2} TransferFromGlobal({:cnst "tid"} tid: X) returns ({:linear "mem"} l: lmap);
+procedure {:yields} {:phase 1,2} TransferFromGlobal({:linear "tid"} tid: X) returns ({:linear "mem"} l: lmap);
ensures {:both} |{ A: assert tid != nil && lock == tid; l := g; return true; }|;
requires {:phase 1} InvLock(lock, b);
ensures {:phase 1} InvLock(lock, b);
-procedure {:yields} {:phase 1} Load({:cnst "mem"} l: lmap, a: int) returns (v: int);
+procedure {:yields} {:phase 1} Load({:linear "mem"} l: lmap, a: int) returns (v: int);
ensures {:both} |{ A: v := map(l)[a]; return true; }|;
requires {:phase 1} InvLock(lock, b);
ensures {:phase 1} InvLock(lock, b);
-procedure {:yields} {:phase 1} Store({:linear "mem"} l_in: lmap, a: int, v: int) returns ({:linear "mem"} l_out: lmap);
+procedure {:yields} {:phase 1} Store({:linear_in "mem"} l_in: lmap, a: int, v: int) returns ({:linear "mem"} l_out: lmap);
ensures {:both} |{ A: assume l_out == cons(dom(l_in), map(l_in)[a := v]); return true; }|;
requires {:phase 1} InvLock(lock, b);
ensures {:phase 1} InvLock(lock, b);
-procedure {:yields} {:phase 2} P({:cnst "tid"} tid: X)
+procedure {:yields} {:phase 2} P({:linear "tid"} tid: X)
requires {:phase 1} InvLock(lock, b);
ensures {:phase 1} InvLock(lock, b);
requires {:phase 2} tid != nil && Inv(g);
@@ -77,7 +77,7 @@ function {:inline} Inv(g: lmap) : bool
var {:phase 1} b: bool;
var {:phase 2} lock: X;
-procedure {:yields} {:phase 1,2} Acquire({:cnst "tid"} tid: X)
+procedure {:yields} {:phase 1,2} Acquire({:linear "tid"} tid: X)
requires {:phase 1} InvLock(lock, b);
ensures {:phase 1} InvLock(lock, b);
ensures {:right} |{ A: assert tid != nil; assume lock == nil; lock := tid; return true; }|;
@@ -102,7 +102,7 @@ ensures {:right} |{ A: assert tid != nil; assume lock == nil; lock := tid; retur
goto L;
}
-procedure {:yields} {:phase 1,2} Release({:cnst "tid"} tid: X)
+procedure {:yields} {:phase 1,2} Release({:linear "tid"} tid: X)
ensures {:left} |{ A: assert lock == tid && tid != nil; lock := nil; return true; }|;
requires {:phase 1} InvLock(lock, b);
ensures {:phase 1} InvLock(lock, b);
diff --git a/Test/og/linear-set.bpl b/Test/og/linear-set.bpl
index de7c53e6..228062a3 100644
--- a/Test/og/linear-set.bpl
+++ b/Test/og/linear-set.bpl
@@ -23,7 +23,7 @@ function {:inline} {:linear "x"} XCollector(xs: [X]bool) : [X]bool
var {:phase 1} x: int;
var {:phase 1} l: [X]bool;
-procedure Split({:linear "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [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();
procedure Allocate() returns ({:linear "tid"} xls: [X]bool);
@@ -38,7 +38,7 @@ procedure {:yields} {:phase 0,1} Unlock();
ensures {:atomic} |{A: l := None(); return true; }|;
-procedure {:yields} {:phase 1} main({:linear "tid"} tidls': [X]bool, {:linear "x"} xls': [X]bool)
+procedure {:yields} {:phase 1} main({:linear_in "tid"} tidls': [X]bool, {:linear_in "x"} xls': [X]bool)
requires {:phase 1} tidls' != None() && xls' == All();
{
var {:linear "tid"} tidls: [X]bool;
@@ -66,7 +66,7 @@ requires {:phase 1} tidls' != None() && xls' == All();
yield;
}
-procedure {:yields} {:phase 1} thread({:linear "tid"} tidls': [X]bool, {:linear "x"} xls': [X]bool)
+procedure {:yields} {:phase 1} thread({:linear_in "tid"} tidls': [X]bool, {:linear_in "x"} xls': [X]bool)
requires {:phase 1} tidls' != None() && xls' != None();
{
var {:linear "x"} xls: [X]bool;
diff --git a/Test/og/linear-set2.bpl b/Test/og/linear-set2.bpl
index 73ffb9ad..11d24605 100644
--- a/Test/og/linear-set2.bpl
+++ b/Test/og/linear-set2.bpl
@@ -24,7 +24,7 @@ var {:phase 1} x: int;
var {:phase 1} l: X;
const nil: X;
-procedure Split({:linear "x"} xls: [X]bool) returns ({:linear "x"} xls1: [X]bool, {:linear "x"} xls2: [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();
procedure Allocate() returns ({:linear "tid"} xls: X);
@@ -39,7 +39,7 @@ ensures {:atomic} |{A: assume l == nil; l := tidls; return true; }|;
procedure {:yields} {:phase 0,1} Unlock();
ensures {:atomic} |{A: l := nil; return true; }|;
-procedure {:yields} {:phase 1} main({:linear "tid"} tidls': X, {:linear "x"} xls': [X]bool)
+procedure {:yields} {:phase 1} main({:linear_in "tid"} tidls': X, {:linear_in "x"} xls': [X]bool)
requires {:phase 1} tidls' != nil && xls' == All();
{
var {:linear "tid"} tidls: X;
@@ -66,7 +66,7 @@ requires {:phase 1} tidls' != nil && xls' == All();
yield;
}
-procedure {:yields} {:phase 1} thread({:linear "tid"} tidls': X, {:linear "x"} xls': [X]bool)
+procedure {:yields} {:phase 1} thread({:linear_in "tid"} tidls': X, {:linear_in "x"} xls': [X]bool)
requires {:phase 1} tidls' != nil && xls' != None();
{
var {:linear "x"} xls: [X]bool;
diff --git a/Test/og/lock-introduced.bpl b/Test/og/lock-introduced.bpl
index d424f9a3..1f576c42 100644
--- a/Test/og/lock-introduced.bpl
+++ b/Test/og/lock-introduced.bpl
@@ -11,7 +11,7 @@ const nil: X;
var {:phase 0,2} b: bool;
var {:phase 1,3} lock: X;
-procedure {:yields} {:phase 3} Customer({:cnst "tid"} tid: X)
+procedure {:yields} {:phase 3} Customer({:linear "tid"} tid: X)
requires {:phase 2} tid != nil;
requires {:phase 2} InvLock(lock, b);
ensures {:phase 2} InvLock(lock, b);
@@ -35,7 +35,7 @@ function {:inline} InvLock(lock: X, b: bool) : bool
lock != nil <==> b
}
-procedure {:yields} {:phase 2,3} Enter({:cnst "tid"} tid: X)
+procedure {:yields} {:phase 2,3} Enter({:linear "tid"} tid: X)
requires {:phase 2} tid != nil;
requires {:phase 2} InvLock(lock, b);
ensures {:phase 2} InvLock(lock, b);
@@ -48,7 +48,7 @@ ensures {:right} |{ A: assume lock == nil && tid != nil; lock := tid; return tru
assert {:phase 2} InvLock(lock, b);
}
-procedure {:yields} {:phase 2,3} Leave({:cnst "tid"} tid:X)
+procedure {:yields} {:phase 2,3} Leave({:linear "tid"} tid:X)
requires {:phase 2} InvLock(lock, b);
ensures {:phase 2} InvLock(lock, b);
ensures {:atomic} |{ A: assert lock == tid && tid != nil; lock := nil; return true; }|;
@@ -60,7 +60,7 @@ ensures {:atomic} |{ A: assert lock == tid && tid != nil; lock := nil; return tr
assert {:phase 2} InvLock(lock, b);
}
-procedure {:yields} {:phase 1,2} LowerEnter({:cnst "tid"} tid: X)
+procedure {:yields} {:phase 1,2} LowerEnter({:linear "tid"} tid: X)
ensures {:atomic} |{ A: assume !b; b := true; lock := tid; return true; }|;
{
var status: bool;
diff --git a/Test/og/multiset.bpl b/Test/og/multiset.bpl
index fc97f9fb..8ee661c6 100644
--- a/Test/og/multiset.bpl
+++ b/Test/og/multiset.bpl
@@ -20,7 +20,7 @@ function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool
axiom (max > 0);
-procedure {:yields} {:phase 0} acquire(i : int, {:linear "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X);
+procedure {:yields} {:phase 0} acquire(i : int, {:linear_in "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X);
ensures {:right} |{ A:
assert 0 <= i && i < max;
assert tidIn != nil && tidIn != done;
@@ -31,7 +31,7 @@ ensures {:right} |{ A:
}|;
-procedure {:yields} {:phase 0} release(i : int, {:linear "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X);
+procedure {:yields} {:phase 0} release(i : int, {:linear_in "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X);
ensures {:left} |{ A:
assert 0 <= i && i < max;
assert lock[i] == tidIn;
@@ -42,7 +42,7 @@ ensures {:left} |{ A:
}|;
-procedure {:yields} {:phase 0,1} getElt(j : int, {:linear "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X, elt_j:int);
+procedure {:yields} {:phase 0,1} getElt(j : int, {:linear_in "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X, elt_j:int);
ensures {:both} |{ A:
assert 0 <= j && j < max;
assert lock[j] == tidIn;
@@ -53,7 +53,7 @@ ensures {:both} |{ A:
}|;
-procedure {:yields} {:phase 0,1} setElt(j : int, x : int, {:linear "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X);
+procedure {:yields} {:phase 0,1} setElt(j : int, x : int, {:linear_in "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X);
ensures {:both} |{ A:
assert x != null;
assert owner[j] == nil;
@@ -67,7 +67,7 @@ ensures {:both} |{ A:
}|;
-procedure {:yields} {:phase 0} setEltToNull(j : int, {:linear "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X);
+procedure {:yields} {:phase 0} setEltToNull(j : int, {:linear_in "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X);
ensures {:left} |{ A:
assert owner[j] == tidIn;
assert 0 <= j && j < max;
@@ -80,7 +80,7 @@ ensures {:left} |{ A:
return true;
}|;
-procedure {:yields} {:phase 0} setValid(j : int, {:linear "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X);
+procedure {:yields} {:phase 0} setValid(j : int, {:linear_in "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X);
ensures {:both} |{ A:
assert 0 <= j && j < max;
assert lock[j] == tidIn;
@@ -92,7 +92,7 @@ ensures {:both} |{ A:
return true;
}|;
-procedure {:yields} {:phase 0} isEltThereAndValid(j : int, x : int, {:linear "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X, fnd:bool);
+procedure {:yields} {:phase 0} isEltThereAndValid(j : int, x : int, {:linear_in "tid"} tidIn: X) returns ({:linear "tid"} tidOut: X, fnd:bool);
ensures {:both} |{ A:
assert 0 <= j && j < max;
assert lock[j] == tidIn;
@@ -102,7 +102,7 @@ ensures {:both} |{ A:
return true;
}|;
-procedure {:yields} {:phase 1} FindSlot(x : int, {:linear "tid"} tidIn: X) returns (r : int, {:linear "tid"} tidOut: X)
+procedure {:yields} {:phase 1} FindSlot(x : int, {:linear_in "tid"} tidIn: X) returns (r : int, {:linear "tid"} tidOut: X)
requires {:phase 1} Inv(valid, elt, owner);
ensures {:phase 1} Inv(valid, elt, owner);
ensures {:right} |{ A: assert tidIn != nil && tidIn != done;
@@ -160,7 +160,7 @@ ensures {:right} |{ A: assert tidIn != nil && tidIn != done;
return;
}
-procedure {:yields} {:phase 2} Insert(x : int, {:linear "tid"} tidIn: X) returns (result : bool, {:linear "tid"} tidOut: X)
+procedure {:yields} {:phase 2} Insert(x : int, {:linear_in "tid"} tidIn: X) returns (result : bool, {:linear "tid"} tidOut: X)
requires {:phase 1} Inv(valid, elt, owner);
requires {:phase 2} Inv(valid, elt, owner);
ensures {:phase 1} Inv(valid, elt, owner);
@@ -207,7 +207,7 @@ ensures {:atomic} |{ var r:int;
procedure {:yields} {:phase 2} InsertPair(x : int,
y : int,
- {:linear "tid"} tidIn: X)
+ {:linear_in "tid"} tidIn: X)
returns (result : bool,
{:linear "tid"} tidOut: X)
requires {:phase 1} Inv(valid, elt, owner);
@@ -286,7 +286,7 @@ ensures {:atomic} |{ var rx:int;
return;
}
-procedure {:yields} {:phase 2} LookUp(x : int, {:linear "tid"} tidIn: X, old_valid:[int]bool, old_elt:[int]int) returns (found : bool, {:linear "tid"} tidOut: X)
+procedure {:yields} {:phase 2} LookUp(x : int, {:linear_in "tid"} tidIn: X, old_valid:[int]bool, old_elt:[int]int) returns (found : bool, {:linear "tid"} tidOut: X)
requires {:phase 1} {:phase 2} old_valid == valid && old_elt == elt;
requires {:phase 1} {:phase 2} Inv(valid, elt, owner);
requires {:phase 1} {:phase 2} (tidIn != nil && tidIn != done);
diff --git a/Test/og/new1.bpl b/Test/og/new1.bpl
index ccddb25e..537a5f4b 100644
--- a/Test/og/new1.bpl
+++ b/Test/og/new1.bpl
@@ -9,11 +9,11 @@ function {:inline} {:linear "Perm"} SetCollectorPerm(x: [int]bool) : [int]bool
x
}
-procedure Allocate_Perm({:linear "Perm"} Permissions: [int]bool) returns ({:linear "Perm"} xls: [int]bool);
+procedure Allocate_Perm({:linear_in "Perm"} Permissions: [int]bool) returns ({:linear "Perm"} xls: [int]bool);
requires Permissions == mapconstbool(true);
ensures xls == mapconstbool(true);
-procedure {:yields} {:phase 1} PB({:linear "Perm"} permVar_in:[int]bool)
+procedure {:yields} {:phase 1} PB({:linear_in "Perm"} permVar_in:[int]bool)
requires {:phase 1} permVar_in[0] && g == 0;
{
var {:linear "Perm"} permVar_out: [int]bool;
@@ -30,7 +30,7 @@ requires {:phase 1} permVar_in[0] && g == 0;
assert {:phase 1} g == 1;
}
-procedure {:yields} {:phase 1} Main({:linear "Perm"} Permissions: [int]bool)
+procedure {:yields} {:phase 1} Main({:linear_in "Perm"} Permissions: [int]bool)
requires {:phase 0,1} Permissions == mapconstbool(true);
{
var {:linear "Perm"} permVar_out: [int]bool;
diff --git a/Test/og/parallel2.bpl b/Test/og/parallel2.bpl
index 8cc1c578..1906d00b 100644
--- a/Test/og/parallel2.bpl
+++ b/Test/og/parallel2.bpl
@@ -23,7 +23,7 @@ procedure {:yields} {:phase 1} main()
par i := u(i) | j := u(j);
}
-procedure {:yields} {:phase 1} t({:linear "tid"} i': int) returns ({:linear "tid"} i: int)
+procedure {:yields} {:phase 1} t({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int)
{
i := i';
@@ -33,7 +33,7 @@ procedure {:yields} {:phase 1} t({:linear "tid"} i': int) returns ({:linear "tid
assert {:phase 1} a[i] == 42;
}
-procedure {:yields} {:phase 1} u({:linear "tid"} i': int) returns ({:linear "tid"} i: int)
+procedure {:yields} {:phase 1} u({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int)
{
i := i';
@@ -43,7 +43,7 @@ procedure {:yields} {:phase 1} u({:linear "tid"} i': int) returns ({:linear "tid
assert {:phase 1} a[i] == 42;
}
-procedure {:yields} {:phase 1} Yield({:cnst "tid"} i: int)
+procedure {:yields} {:phase 1} Yield({:linear "tid"} i: int)
ensures {:phase 1} old(a)[i] == a[i];
{
yield;
diff --git a/Test/og/parallel4.bpl b/Test/og/parallel4.bpl
index 60466d67..f061f8be 100644
--- a/Test/og/parallel4.bpl
+++ b/Test/og/parallel4.bpl
@@ -19,7 +19,7 @@ procedure {:yields} {:phase 1} main()
par i := t(i) | j := t(j);
}
-procedure {:yields} {:phase 1} t({:linear "tid"} i': int) returns ({:linear "tid"} i: int)
+procedure {:yields} {:phase 1} t({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int)
{
i := i';
call Yield();
diff --git a/Test/og/parallel5.bpl b/Test/og/parallel5.bpl
index cfb593a6..751cc666 100644
--- a/Test/og/parallel5.bpl
+++ b/Test/og/parallel5.bpl
@@ -23,7 +23,7 @@ procedure {:yields} {:phase 1} main()
par i := u(i) | j := u(j);
}
-procedure {:yields} {:phase 1} t({:linear "tid"} i': int) returns ({:linear "tid"} i: int)
+procedure {:yields} {:phase 1} t({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int)
{
i := i';
@@ -33,7 +33,7 @@ procedure {:yields} {:phase 1} t({:linear "tid"} i': int) returns ({:linear "tid
assert {:phase 1} a[i] == 42;
}
-procedure {:yields} {:phase 1} u({:linear "tid"} i': int) returns ({:linear "tid"} i: int)
+procedure {:yields} {:phase 1} u({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int)
{
i := i';
@@ -43,7 +43,7 @@ procedure {:yields} {:phase 1} u({:linear "tid"} i': int) returns ({:linear "tid
assert {:phase 1} a[i] == 42;
}
-procedure {:yields} {:phase 1} Yield({:cnst "tid"} i: int)
+procedure {:yields} {:phase 1} Yield({:linear "tid"} i: int)
ensures {:phase 1} old(a)[i] == a[i];
{
yield;
diff --git a/Test/og/perm.bpl b/Test/og/perm.bpl
index b3c3e86d..4df74778 100644
--- a/Test/og/perm.bpl
+++ b/Test/og/perm.bpl
@@ -10,11 +10,11 @@ function {:inline} {:linear "Perm"} SetCollectorPerm(x: [int]bool) : [int]bool
x
}
-procedure Split({:linear "Perm"} xls: [int]bool) returns ({:linear "Perm"} xls1: [int]bool, {:linear "Perm"} xls2: [int]bool);
+procedure Split({:linear_in "Perm"} xls: [int]bool) returns ({:linear "Perm"} xls1: [int]bool, {:linear "Perm"} xls2: [int]bool);
ensures xls == ch_mapunion(xls1, xls2) && xls1 != ch_mapconstbool(false) && xls2 != ch_mapconstbool(false);
-procedure {:yields} {:phase 1} mainE({:linear "Perm"} permVar_in: [int]bool)
+procedure {:yields} {:phase 1} mainE({:linear_in "Perm"} permVar_in: [int]bool)
free requires {:phase 1} permVar_in == ch_mapconstbool(true);
free requires {:phase 1} permVar_in[0];
free requires {:phase 1} x == 0;
@@ -34,7 +34,7 @@ procedure {:yields} {:phase 1} mainE({:linear "Perm"} permVar_in: [int]bool)
yield;
}
-procedure {:yields} {:phase 1} foo({:linear "Perm"} permVar_in: [int]bool)
+procedure {:yields} {:phase 1} foo({:linear_in "Perm"} permVar_in: [int]bool)
free requires {:phase 1} permVar_in != ch_mapconstbool(false);
free requires {:phase 1} permVar_in[1];
requires {:phase 1} x == 0;
diff --git a/Test/og/t1.bpl b/Test/og/t1.bpl
index 02db387c..3730d490 100644
--- a/Test/og/t1.bpl
+++ b/Test/og/t1.bpl
@@ -36,7 +36,7 @@ ensures {:atomic} |{A: g := val; return true; }|;
procedure {:yields} {:phase 0,1} SetH(val:int);
ensures {:atomic} |{A: h := val; return true; }|;
-procedure {:yields} {:phase 1} A({:linear "tid"} tid_in: int) returns ({:linear "tid"} tid_out: int)
+procedure {:yields} {:phase 1} A({:linear_in "tid"} tid_in: int) returns ({:linear "tid"} tid_out: int)
{
var {:linear "1"} x: [int]bool;
var {:linear "2"} y: [int]bool;
@@ -72,7 +72,7 @@ procedure {:yields} {:phase 1} A({:linear "tid"} tid_in: int) returns ({:linear
yield;
}
-procedure {:yields} {:phase 1} B({:linear "tid"} tid_in: int, {:linear "1"} x_in: [int]bool)
+procedure {:yields} {:phase 1} B({:linear_in "tid"} tid_in: int, {:linear_in "1"} x_in: [int]bool)
requires {:phase 1} x_in != mapconstbool(false);
{
var {:linear "tid"} tid_out: int;
@@ -85,7 +85,7 @@ requires {:phase 1} x_in != mapconstbool(false);
yield;
}
-procedure {:yields} {:phase 1} C({:linear "tid"} tid_in: int, {:linear "2"} y_in: [int]bool)
+procedure {:yields} {:phase 1} C({:linear_in "tid"} tid_in: int, {:linear_in "2"} y_in: [int]bool)
requires {:phase 1} y_in != mapconstbool(false);
{
var {:linear "tid"} tid_out: int;
diff --git a/Test/og/ticket.bpl b/Test/og/ticket.bpl
index 02341e91..552a4007 100644
--- a/Test/og/ticket.bpl
+++ b/Test/og/ticket.bpl
@@ -33,10 +33,10 @@ function {:inline} Inv2(tickets: [int]bool, ticket: int, lock: X): (bool)
if (lock == nil) then tickets == RightOpen(ticket) else tickets == RightClosed(ticket)
}
-procedure Allocate({:linear "tid"} xls':[X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X);
+procedure Allocate({:linear_in "tid"} xls':[X]bool) returns ({:linear "tid"} xls: [X]bool, {:linear "tid"} xl: X);
ensures {:phase 1} {:phase 2} xl != nil;
-procedure {:yields} {:phase 3} main({:linear "tid"} xls':[X]bool)
+procedure {:yields} {:phase 3} main({:linear_in "tid"} xls':[X]bool)
requires {:phase 3} xls' == mapconstbool(true);
{
var {:linear "tid"} tid: X;
@@ -59,7 +59,7 @@ requires {:phase 3} xls' == mapconstbool(true);
par Yield1() | Yield2() | Yield();
}
-procedure {:yields} {:phase 3} Customer({:linear "tid"} tid': X)
+procedure {:yields} {:phase 3} Customer({:linear_in "tid"} tid': X)
requires {:phase 1} Inv1(T, t);
requires {:phase 2} tid' != nil && Inv2(T, s, cs);
requires {:phase 3} true;
@@ -80,7 +80,7 @@ requires {:phase 3} true;
par Yield1() | Yield2() | Yield();
}
-procedure {:yields} {:phase 2,3} Enter({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X)
+procedure {:yields} {:phase 2,3} Enter({:linear_in "tid"} tid': X) returns ({:linear "tid"} tid: X)
requires {:phase 1} Inv1(T, t);
ensures {:phase 1} Inv1(T,t);
requires {:phase 2} tid' != nil && Inv2(T, s, cs);
@@ -97,7 +97,7 @@ ensures {:right} |{ A: tid := tid'; havoc t, T; assume tid != nil && cs == nil;
par Yield1() | Yield2();
}
-procedure {:yields} {:phase 1,2} GetTicketAbstract({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X, m: int)
+procedure {:yields} {:phase 1,2} GetTicketAbstract({:linear_in "tid"} tid': X) returns ({:linear "tid"} tid: X, m: int)
requires {:phase 1} Inv1(T, t);
ensures {:phase 1} Inv1(T, t);
ensures {:right} |{ A: tid := tid'; havoc m, t; assume !T[m]; T[m] := true; return true; }|;
@@ -129,15 +129,15 @@ ensures {:phase 1} Inv1(T,t);
assert {:phase 1} Inv1(T,t);
}
-procedure {:yields} {:phase 0,3} Init({:linear "tid"} xls':[X]bool) returns ({:linear "tid"} xls:[X]bool);
+procedure {:yields} {:phase 0,3} Init({:linear_in "tid"} xls':[X]bool) returns ({:linear "tid"} xls:[X]bool);
ensures {:atomic} |{ A: assert xls' == mapconstbool(true); xls := xls'; cs := nil; t := 0; s := 0; T := RightOpen(0); return true; }|;
-procedure {:yields} {:phase 0,1} GetTicket({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X, m: int);
+procedure {:yields} {:phase 0,1} GetTicket({:linear_in "tid"} tid': X) returns ({:linear "tid"} tid: X, m: int);
ensures {:atomic} |{ A: tid := tid'; m := t; t := t + 1; T[m] := true; return true; }|;
-procedure {:yields} {:phase 0,2} WaitAndEnter({:linear "tid"} tid': X, m:int) returns ({:linear "tid"} tid: X);
+procedure {:yields} {:phase 0,2} WaitAndEnter({:linear_in "tid"} tid': X, m:int) returns ({:linear "tid"} tid: X);
ensures {:atomic} |{ A: tid := tid'; assume m <= s; cs := tid; return true; }|;
-procedure {:yields} {:phase 0,3} Leave({:linear "tid"} tid': X) returns ({:linear "tid"} tid: X);
+procedure {:yields} {:phase 0,3} Leave({:linear_in "tid"} tid': X) returns ({:linear "tid"} tid: X);
ensures {:atomic} |{ A: assert cs == tid'; assert tid' != nil; tid := tid'; s := s + 1; cs := nil; return true; }|;
diff --git a/Test/og/treiber-stack.bpl b/Test/og/treiber-stack.bpl
index 8e5f059a..ecaf1e3a 100644
--- a/Test/og/treiber-stack.bpl
+++ b/Test/og/treiber-stack.bpl
@@ -24,13 +24,13 @@ ensures {:right} |{ A: goto B,C;
B: assume dom(Stack)[i]; v := map(Stack)[i]; return true;
C: assume !dom(Stack)[i]; return true; }|;
-procedure {:yields} {:phase 0} Store({:linear "Node"} l_in:lmap, i:Node, v:Node) returns ({:linear "Node"} l_out:lmap);
+procedure {:yields} {:phase 0} Store({:linear_in "Node"} l_in:lmap, i:Node, v:Node) returns ({:linear "Node"} l_out:lmap);
ensures {:both} |{ A: assert dom(l_in)[i]; l_out := Add(l_in, i, v); return true; }|;
procedure {:yields} {:phase 0} MakeEmpty() returns ({:linear "Node"} l_out:lmap);
ensures {:both} |{ A: l_out := EmptyLmap(); return true; }|;
-procedure {:yields} {:phase 0} TransferToStack(oldVal: Node, newVal: Node, {:linear "Node"} l_in:lmap) returns (r: bool, {:linear "Node"} l_out:lmap);
+procedure {:yields} {:phase 0} TransferToStack(oldVal: Node, newVal: Node, {:linear_in "Node"} l_in:lmap) returns (r: bool, {:linear "Node"} l_out:lmap);
ensures {:atomic} |{ A: assert dom(l_in)[newVal];
goto B,C;
B: assume oldVal == TopOfStack; TopOfStack := newVal; l_out := EmptyLmap(); Stack := Add(Stack, newVal, map(l_in)[newVal]); r := true; return true;
@@ -51,7 +51,7 @@ function {:inline} Inv(TopOfStack: Node, Stack: lmap) : (bool)
Subset(Difference(BetweenSet(map(Stack), TopOfStack, null), Singleton(null)), dom(Stack))
}
-procedure {:yields} {:phase 1} push(x: Node, {:linear "Node"} x_lmap: lmap)
+procedure {:yields} {:phase 1} push(x: Node, {:linear_in "Node"} x_lmap: lmap)
requires {:phase 1} dom(x_lmap)[x];
requires {:phase 1} Inv(TopOfStack, Stack);
ensures {:phase 1} Inv(TopOfStack, Stack);
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 14:07:47 +0000