removed some obsolete linear string attributes

shazqadeer · shazqadeer · commit 80470f6d7e13 · 2025-11-08T21:46:11.000-08:00
diff --git a/Test/civl/regression-tests/async-yield-sufficiency.bpl b/Test/civl/regression-tests/async-yield-sufficiency.bpl
@@ -1,16 +1,16 @@
 // RUN: %parallel-boogie "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
-type {:linear "tid"} Tid = int;
+type {:linear} Tid = int;
 var {:layer 0,1} x:int;
 
-yield procedure {:layer 1} P({:linear_in "tid"} tid1:int, {:linear "tid"} tid2:int)
+yield procedure {:layer 1} P({:linear_in} tid1:int, {:linear} tid2:int)
 requires call Yield_P(tid1, tid2);
 {
   async call Q(tid1);
   call write(); // This action invalidates the precondition of the above async call
 }
 
-yield procedure {:layer 1} Q({:linear "tid"} tid1:int)
+yield procedure {:layer 1} Q({:linear} tid1:int)
 requires call Yield_Q(tid1);
 {
   call assertion();
@@ -33,11 +33,11 @@ refines WRITE;
 yield procedure {:layer 0} assertion();
 refines ASSERTION;
 
-yield invariant {:layer 1} Yield_P({:linear "tid"} tid1:int, {:linear "tid"} tid2:int);
+yield invariant {:layer 1} Yield_P({:linear} tid1:int, {:linear} tid2:int);
 preserves tid1 == 1;
 preserves tid2 == 1;
 preserves x == 0;
 
-yield invariant {:layer 1} Yield_Q({:linear "tid"} tid1:int);
+yield invariant {:layer 1} Yield_Q({:linear} tid1:int);
 preserves tid1 == 1;
 preserves x == 0; // This precondition is not valid at the end of procedure P
diff --git a/Test/civl/regression-tests/call-yield-invariant-errors.bpl b/Test/civl/regression-tests/call-yield-invariant-errors.bpl
@@ -1,26 +1,25 @@
 // RUN: %parallel-boogie "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
-type {:linear "lin"} X = int;
 var {:layer 0,1} x:int;
-yield invariant {:layer 1} linear_yield_x({:linear "lin"} n: int);
+yield invariant {:layer 1} linear_yield_x({:linear} n: int);
 preserves x >= n;
 
 yield procedure {:layer 1}
 p2({:linear_in "lin"} b: int);
 
 yield procedure {:layer 1}
-P1({:linear "lin"} x: int, {:linear_in "lin"} y: int)
+P1({:linear} x: int, {:linear_in "lin"} y: int)
 {
   call Q(x) | Q(x);
 }
 
 yield procedure {:layer 1}
-P2({:linear "lin"} x: int, {:linear_in "lin"} y: int)
+P2({:linear} x: int, {:linear_in "lin"} y: int)
 {
   call Q(x) | linear_yield_x(y) | linear_yield_x(y);
   call Q(x) | linear_yield_x(x) | linear_yield_x(y);
 }
 
 yield procedure {:layer 1}
-Q({:linear "lin"} a: int);
+Q({:linear} a: int);
diff --git a/Test/civl/regression-tests/call-yield-invariant-errors.bpl.expect b/Test/civl/regression-tests/call-yield-invariant-errors.bpl.expect
@@ -1,3 +1,3 @@
-call-yield-invariant-errors.bpl(15,2): Error: linear variable can occur only once as an input parameter of a parallel call: x
-call-yield-invariant-errors.bpl(22,2): Error: linear variable cannot be an input parameter to both a yield invariant and a procedure in a parallel call: x
+call-yield-invariant-errors.bpl(14,2): Error: linear variable can occur only once as an input parameter of a parallel call: x
+call-yield-invariant-errors.bpl(21,2): Error: linear variable cannot be an input parameter to both a yield invariant and a procedure in a parallel call: x
 2 type checking errors detected in call-yield-invariant-errors.bpl
diff --git a/Test/civl/regression-tests/funky.bpl b/Test/civl/regression-tests/funky.bpl
@@ -1,6 +1,7 @@
 // RUN: %parallel-boogie "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
-type {:linear} X;
+
+type X;
 const nil: X;
 
 var {:layer 0,3} A: X;
diff --git a/Test/civl/regression-tests/linear/allocator.bpl b/Test/civl/regression-tests/linear/allocator.bpl
@@ -1,15 +1,10 @@
 // RUN: %parallel-boogie "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
-
-
-
-type {:linear "tid"} X = int;
-
-procedure A({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int);
+procedure A({:linear_in} i': int) returns ({:linear} i: int);
   ensures i == i';
 
-procedure B({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int)
+procedure B({:linear_in} i': int) returns ({:linear} i: int)
 {
   i := i';
   call i := A(i);
diff --git a/Test/civl/regression-tests/linear/allocator.bpl.expect b/Test/civl/regression-tests/linear/allocator.bpl.expect
@@ -1,5 +1,5 @@
-allocator.bpl(16,3): Error: this assertion could not be proved
+allocator.bpl(11,3): Error: this assertion could not be proved
 Execution trace:
-    allocator.bpl(14,5): anon0
+    allocator.bpl(9,5): anon0
 
 Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/civl/regression-tests/linear/bug.bpl b/Test/civl/regression-tests/linear/bug.bpl
@@ -1,9 +1,7 @@
 // RUN: %parallel-boogie "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
-type {:linear ""} X = int;
-
-var {:linear ""} g:int;
+var {:linear} g:int;
 
 procedure A()
 {
diff --git a/Test/civl/regression-tests/linear/bug.bpl.expect b/Test/civl/regression-tests/linear/bug.bpl.expect
@@ -1,5 +1,5 @@
-bug.bpl(15,3): Error: this assertion could not be proved
+bug.bpl(13,3): Error: this assertion could not be proved
 Execution trace:
-    bug.bpl(14,3): anon0
+    bug.bpl(12,3): anon0
 
 Boogie program verifier finished with 1 verified, 1 error
diff --git a/Test/civl/regression-tests/linear/f1.bpl b/Test/civl/regression-tests/linear/f1.bpl
@@ -1,6 +1,6 @@
-// RUN: %parallel-boogie "%s" > "%t"
+// RUN: %parallel-boogie -lib:base "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
-type {:linear "1"} X = int;
+
 const {:existential true} b0: bool;
 const {:existential true} b1: bool;
 const {:existential true} b2: bool;
@@ -21,11 +21,11 @@ axiom(!b6);
 axiom(!b7);
 axiom(b8);
 
-procedure main({:linear_in "1"} x_in: [int]bool)
+procedure main({:linear_in} x_in: [int]bool)
   requires b0 ==> x_in == MapConst(true);
   requires b1 ==> x_in != MapConst(false);
 {
-   var {:linear "1"} x: [int] bool;
+   var {:linear} x: [int] bool;
    x := x_in;
 
    call foo(x);
@@ -35,11 +35,11 @@ procedure main({:linear_in "1"} x_in: [int]bool)
    assert b8 ==> x == MapConst(false);
 }
 
-procedure foo({:linear_in "1"} x_in: [int]bool)
+procedure foo({:linear_in} x_in: [int]bool)
   requires b2 ==> x_in == MapConst(true);
   requires b3 ==> x_in != MapConst(false);
 {
-   var {:linear "1"} x: [int] bool;
+   var {:linear} x: [int] bool;
    x := x_in;
 
    assert b4 ==> x == MapConst(true);
diff --git a/Test/civl/regression-tests/linear/f2.bpl b/Test/civl/regression-tests/linear/f2.bpl
@@ -1,23 +1,16 @@
-// RUN: %parallel-boogie "%s" > "%t"
+// RUN: %parallel-boogie -lib:base "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
-
-
-
-
-
-type {:linear "1"} X = int;
-
-procedure Split({:linear_in "1"} xls: [int]bool) returns ({:linear "1"} xls1: [int]bool, {:linear "1"} xls2: [int]bool);
+procedure Split({:linear_in} xls: [int]bool) returns ({:linear} xls1: [int]bool, {:linear} xls2: [int]bool);
 ensures xls == MapOr(xls1, xls2) && xls1 != MapConst(false) && xls2 != MapConst(false);
 
-procedure Allocate() returns ({:linear "1"} x: [int]bool);
+procedure Allocate() returns ({:linear} x: [int]bool);
 
 procedure main()
 {
-   var {:linear "1"} x: [int] bool;
-   var {:linear "1"} x1: [int] bool;
-   var {:linear "1"} x2: [int] bool;
+   var {:linear} x: [int] bool;
+   var {:linear} x1: [int] bool;
+   var {:linear} x2: [int] bool;
 
    call x := Allocate();
    assume x == MapConst(true);
diff --git a/Test/civl/regression-tests/linear/f2.bpl.expect b/Test/civl/regression-tests/linear/f2.bpl.expect
@@ -1,5 +1,5 @@
-f2.bpl(26,4): Error: this assertion could not be proved
+f2.bpl(19,4): Error: this assertion could not be proved
 Execution trace:
-    f2.bpl(22,4): anon0
+    f2.bpl(15,4): anon0
 
 Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/civl/regression-tests/parallel4.bpl b/Test/civl/regression-tests/parallel4.bpl
@@ -1,25 +1,20 @@
 // RUN: %parallel-boogie "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
-
-
-
-type {:linear "tid"} X = int;
-
 var {:layer 0,1} a:int;
 
-yield procedure {:layer 1} Allocate() returns ({:linear "tid"} tid: int);
+yield procedure {:layer 1} Allocate() returns ({:linear} tid: int);
 
 yield procedure {:layer 1} main()
 {
-  var {:linear "tid"} i: int;
-  var {:linear "tid"} j: int;
+  var {:linear} i: int;
+  var {:linear} j: int;
   call i := Allocate();
   call j := Allocate();
   call i := t(i) | j := t(j);
 }
 
-yield procedure {:layer 1} t({:linear_in "tid"} i': int) returns ({:linear "tid"} i: int)
+yield procedure {:layer 1} t({:linear_in} i': int) returns ({:linear} i: int)
 {
   i := i';
   call Yield();
diff --git a/Test/civl/regression-tests/parallel4.bpl.expect b/Test/civl/regression-tests/parallel4.bpl.expect
@@ -1,6 +1,6 @@
-parallel4.bpl(26,3): Error: this assertion could not be proved
+parallel4.bpl(21,3): Error: this assertion could not be proved
 Execution trace:
-    parallel4.bpl(24,5): anon0
-    parallel4.bpl(24,5): anon0_0
+    parallel4.bpl(19,5): anon0
+    parallel4.bpl(19,5): anon0_0
 
 Boogie program verifier finished with 3 verified, 1 error
diff --git a/Test/civl/regression-tests/signature-mismatch.bpl b/Test/civl/regression-tests/signature-mismatch.bpl
@@ -1,6 +1,6 @@
 // RUN: %parallel-boogie "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
-type {:linear "lin"} X = int;
+type {:linear} X = int;
 var {:layer 0,1} x:int;
 var {:layer 0,1} y:bool;
 ////////////////////////////////////////////////////////////////////////////////
@@ -29,7 +29,7 @@ refines atomic_write_x_2;
 
 ////////////////////////////////////////////////////////////////////////////////
 
-atomic action {:layer 1,1} atomic_write_x_3 ({:linear "lin"} x':int)
+atomic action {:layer 1,1} atomic_write_x_3 ({:linear} x':int)
 modifies x;
 { x := x'; }
 
diff --git a/Test/civl/regression-tests/yield-requires-ensures-errors-4.bpl b/Test/civl/regression-tests/yield-requires-ensures-errors-4.bpl
@@ -1,15 +1,15 @@
 // RUN: %parallel-boogie "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
-type {:linear "lin"} X = int;
+type {:linear} X = int;
 
 var {:layer 0,1} x:int;
 
-yield invariant {:layer 1} linear_yield_x({:linear "lin"} n: int);
+yield invariant {:layer 1} linear_yield_x({:linear} n: int);
 preserves x >= n;
 
 yield procedure {:layer 1}
-p3({:linear "lin"} a: int, {:linear_in "lin"} b: int, {:linear_out "lin"} c: int);
+p3({:linear} a: int, {:linear_in "lin"} b: int, {:linear_out "lin"} c: int);
 requires call linear_yield_x(a);
 ensures call linear_yield_x(a);
 requires call linear_yield_x(c);
diff --git a/Test/civl/regression-tests/yield-requires-ensures-errors.bpl b/Test/civl/regression-tests/yield-requires-ensures-errors.bpl
@@ -1,7 +1,7 @@
 // RUN: %parallel-boogie "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
-type {:linear "lin"} X = int;
+type {:linear} X = int;
 
 var {:layer 0,1} x:int;
 
diff --git a/Test/civl/samples/bluetooth.bpl b/Test/civl/samples/bluetooth.bpl
@@ -108,9 +108,8 @@ pure action B({:linear_in} usersInDriver: Set Perm, {:linear_out} l: Set Perm)
 }
 
 // stopper code
-type {:linear "stopper"} X = int;
 
-yield procedure {:layer 2} Stopper({:linear "stopper"} i: One int)
+yield procedure {:layer 2} Stopper({:linear} i: One int)
 refines AtomicSetStoppingFlag;
 preserves call Inv2();
 preserves call Inv1();
@@ -119,7 +118,7 @@ preserves call Inv1();
     call WaitAndStop();
 }
 
-yield procedure {:layer 1} Close({:linear "stopper"} i: One int)
+yield procedure {:layer 1} Close({:linear} i: One int)
 refines AtomicSetStoppingFlag;
 preserves call Inv1();
 {
@@ -160,7 +159,7 @@ atomic action {:layer 1} AtomicCheckAssert()
 yield procedure {:layer 0} CheckAssert();
 refines AtomicCheckAssert;
 
-right action {:layer 1,3} AtomicSetStoppingFlag({:linear "stopper"} i: One int)
+right action {:layer 1,3} AtomicSetStoppingFlag({:linear} i: One int)
 modifies stoppingFlag;
 {
     // The first assertion ensures that there is at most one stopper.
@@ -169,7 +168,7 @@ modifies stoppingFlag;
     assert !stoppingFlag;
     stoppingFlag := true;
 }
-yield procedure {:layer 0} SetStoppingFlag({:linear "stopper"} i: One int);
+yield procedure {:layer 0} SetStoppingFlag({:linear} i: One int);
 refines AtomicSetStoppingFlag;
 
 atomic action {:layer 1} AtomicDeleteReference()
diff --git a/Test/civl/samples/purity-issta.bpl b/Test/civl/samples/purity-issta.bpl
@@ -1,6 +1,7 @@
 // RUN: %parallel-boogie "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
-type {:linear} X;
+
+type X;
 const nil: X;
 
 const max: int;

Original file line number	Diff line number	Diff line change
`@@ -1,9 +1,7 @@`
`1`	`1`	`// RUN: %parallel-boogie "%s" > "%t"`
`2`	`2`	`// RUN: %diff "%s.expect" "%t"`
`3`	`3`
`4`		`-type {:linear ""} X = int;`
`5`		`-`
`6`		`-var {:linear ""} g:int;`
	`4`	`+var {:linear} g:int;`
`7`	`5`
`8`	`6`	`procedure A()`
`9`	`7`	`{`