Enabled "linear type checking" lit tests.

15 files changed, 76 insertions, 22 deletions

diff --git a/Test/linear/Answer b/Test/linear/Answer
index ff1246e6..4b8794a6 100644
--- a/Test/linear/Answer
+++ b/Test/linear/Answer
@@ -1,20 +1,20 @@
 

 -------------------- typecheck.bpl --------------------

-typecheck.bpl(31,9): Error: Only simple assignment allowed on linear variable b

-typecheck.bpl(33,6): Error: Only variable can be assigned to linear variable a

-typecheck.bpl(35,6): Error: Only linear variable can be assigned to linear variable a

-typecheck.bpl(39,6): Error: Linear variable of domain D2 cannot be assigned to linear variable of domain D

-typecheck.bpl(45,9): Error: Linear variable x can occur only once in the right-hand-side of an assignment

-typecheck.bpl(49,4): Error: Linear variable a can occur only once as an input parameter

-typecheck.bpl(51,4): Error: Only variable can be passed to linear parameter b

-typecheck.bpl(53,4): Error: The domains of formal and actual parameters must be the same

+typecheck.bpl(33,9): Error: Only simple assignment allowed on linear variable b

+typecheck.bpl(35,6): Error: Only variable can be assigned to linear variable a

+typecheck.bpl(37,6): Error: Only linear variable can be assigned to linear variable a

+typecheck.bpl(41,6): Error: Linear variable of domain D2 cannot be assigned to linear variable of domain D

+typecheck.bpl(47,9): Error: Linear variable x can occur only once in the right-hand-side of an assignment

+typecheck.bpl(51,4): Error: Linear variable a can occur only once as an input parameter

+typecheck.bpl(53,4): Error: Only variable can be passed to linear parameter b

 typecheck.bpl(55,4): Error: The domains of formal and actual parameters must be the same

-typecheck.bpl(57,4): Error: Only a linear argument can be passed to linear parameter a

-typecheck.bpl(62,4): Error: Linear variable a can occur only once as an input parameter of a parallel call

-typecheck.bpl(69,0): Error: Output variable d must be available at a return

-typecheck.bpl(78,0): Error: Global variable g must be available at a return

-typecheck.bpl(83,7): Error: unavailable source for a linear read

-typecheck.bpl(84,0): Error: Output variable r must be available at a return

+typecheck.bpl(57,4): Error: The domains of formal and actual parameters must be the same

+typecheck.bpl(59,4): Error: Only a linear argument can be passed to linear parameter a

+typecheck.bpl(64,4): Error: Linear variable a can occur only once as an input parameter of a parallel call

+typecheck.bpl(71,0): Error: Output variable d must be available at a return

+typecheck.bpl(80,0): Error: Global variable g must be available at a return

+typecheck.bpl(85,7): Error: unavailable source for a linear read

+typecheck.bpl(86,0): Error: Output variable r must be available at a return

 15 type checking errors detected in typecheck.bpl

 

 -------------------- list.bpl --------------------

@@ -22,23 +22,23 @@ typecheck.bpl(84,0): Error: Output variable r must be available at a return
 Boogie program verifier finished with 2 verified, 0 errors

 

 -------------------- allocator.bpl --------------------

-allocator.bpl(8,3): Error BP5001: This assertion might not hold.

+allocator.bpl(10,3): Error BP5001: This assertion might not hold.

 Execution trace:

-    allocator.bpl(6,5): anon0

+    allocator.bpl(8,5): anon0

 

 Boogie program verifier finished with 0 verified, 1 error

 

 -------------------- f1.bpl --------------------

-f1.bpl(33,4): Error BP5001: This assertion might not hold.

+f1.bpl(35,4): Error BP5001: This assertion might not hold.

 Execution trace:

-    f1.bpl(27,6): anon0

+    f1.bpl(29,6): anon0

 

 Boogie program verifier finished with 1 verified, 1 error

 

 -------------------- f2.bpl --------------------

-f2.bpl(19,4): Error BP5001: This assertion might not hold.

+f2.bpl(21,4): Error BP5001: This assertion might not hold.

 Execution trace:

-    f2.bpl(15,4): anon0

+    f2.bpl(17,4): anon0

 

 Boogie program verifier finished with 0 verified, 1 error

 

@@ -47,8 +47,8 @@ Boogie program verifier finished with 0 verified, 1 error
 Boogie program verifier finished with 2 verified, 0 errors

 

 -------------------- bug.bpl --------------------

-bug.bpl(13,3): Error BP5001: This assertion might not hold.

+bug.bpl(15,3): Error BP5001: This assertion might not hold.

 Execution trace:

-    bug.bpl(12,3): anon0

+    bug.bpl(14,3): anon0

 

 Boogie program verifier finished with 1 verified, 1 error

diff --git a/Test/linear/allocator.bpl b/Test/linear/allocator.bpl
index d723cbed..ae8f517d 100644
--- a/Test/linear/allocator.bpl
+++ b/Test/linear/allocator.bpl
@@ -1,3 +1,5 @@
+// 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);

   ensures i == i';

 

diff --git a/Test/linear/allocator.bpl.expect b/Test/linear/allocator.bpl.expect
new file mode 100644
index 00000000..22071642
--- /dev/null
+++ b/Test/linear/allocator.bpl.expect
@@ -0,0 +1,5 @@
+allocator.bpl(10,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    allocator.bpl(8,5): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/linear/bug.bpl b/Test/linear/bug.bpl
index b7a6a238..a619968e 100644
--- a/Test/linear/bug.bpl
+++ b/Test/linear/bug.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory -doModSetAnalysis %s > %t

+// RUN: %diff %s.expect %t

 function {:builtin "MapConst"} MapConstBool(bool) : [int]bool;

 function {:inline} {:linear ""} LinearIntDistinctness(x:int) : [int]bool { MapConstBool(false)[x := true] }

 

diff --git a/Test/linear/bug.bpl.expect b/Test/linear/bug.bpl.expect
new file mode 100644
index 00000000..3a8b1429
--- /dev/null
+++ b/Test/linear/bug.bpl.expect
@@ -0,0 +1,5 @@
+bug.bpl(15,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    bug.bpl(14,3): anon0
+
+Boogie program verifier finished with 1 verified, 1 error
diff --git a/Test/linear/f1.bpl b/Test/linear/f1.bpl
index 1f451daf..513b67fa 100644
--- a/Test/linear/f1.bpl
+++ b/Test/linear/f1.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory -doModSetAnalysis %s > %t

+// RUN: %diff %s.expect %t

 function {:builtin "MapConst"} mapconstbool(bool) : [int]bool;

 const {:existential true} b0: bool;

 const {:existential true} b1: bool;

diff --git a/Test/linear/f1.bpl.expect b/Test/linear/f1.bpl.expect
new file mode 100644
index 00000000..3a280fe7
--- /dev/null
+++ b/Test/linear/f1.bpl.expect
@@ -0,0 +1,5 @@
+f1.bpl(35,4): Error BP5001: This assertion might not hold.
+Execution trace:
+    f1.bpl(29,6): anon0
+
+Boogie program verifier finished with 1 verified, 1 error
diff --git a/Test/linear/f2.bpl b/Test/linear/f2.bpl
index 82871466..9517e349 100644
--- a/Test/linear/f2.bpl
+++ b/Test/linear/f2.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory -doModSetAnalysis %s > %t

+// RUN: %diff %s.expect %t

 function {:builtin "MapConst"} mapconstbool(bool) : [int]bool;

 function {:builtin "MapOr"} mapunion([int]bool, [int]bool) : [int]bool;

 

diff --git a/Test/linear/f2.bpl.expect b/Test/linear/f2.bpl.expect
new file mode 100644
index 00000000..a28b7038
--- /dev/null
+++ b/Test/linear/f2.bpl.expect
@@ -0,0 +1,5 @@
+f2.bpl(21,4): Error BP5001: This assertion might not hold.
+Execution trace:
+    f2.bpl(17,4): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/linear/f3.bpl b/Test/linear/f3.bpl
index a375338c..1f29cc86 100644
--- a/Test/linear/f3.bpl
+++ b/Test/linear/f3.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory -doModSetAnalysis %s > %t

+// RUN: %diff %s.expect %t

 procedure A() {}

 

 procedure B({:linear ""} tid:int) returns({:linear ""} tid':int)

diff --git a/Test/linear/f3.bpl.expect b/Test/linear/f3.bpl.expect
new file mode 100644
index 00000000..41374b00
--- /dev/null
+++ b/Test/linear/f3.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 2 verified, 0 errors
diff --git a/Test/linear/list.bpl b/Test/linear/list.bpl
index b0caa9e1..d11f9d5c 100644
--- a/Test/linear/list.bpl
+++ b/Test/linear/list.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory -doModSetAnalysis %s > %t

+// RUN: %diff %s.expect %t

 type X;

 function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;

 function {:builtin "MapOr"} MapOr([X]bool, [X]bool) : [X]bool;

diff --git a/Test/linear/list.bpl.expect b/Test/linear/list.bpl.expect
new file mode 100644
index 00000000..41374b00
--- /dev/null
+++ b/Test/linear/list.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 2 verified, 0 errors
diff --git a/Test/linear/typecheck.bpl b/Test/linear/typecheck.bpl
index c8510909..72067494 100644
--- a/Test/linear/typecheck.bpl
+++ b/Test/linear/typecheck.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory  %s > %t

+// RUN: %diff %s.expect %t

 type X;

 

 procedure A()

diff --git a/Test/linear/typecheck.bpl.expect b/Test/linear/typecheck.bpl.expect
new file mode 100644
index 00000000..dddbd163
--- /dev/null
+++ b/Test/linear/typecheck.bpl.expect
@@ -0,0 +1,16 @@
+typecheck.bpl(33,9): Error: Only simple assignment allowed on linear variable b
+typecheck.bpl(35,6): Error: Only variable can be assigned to linear variable a
+typecheck.bpl(37,6): Error: Only linear variable can be assigned to linear variable a
+typecheck.bpl(41,6): Error: Linear variable of domain D2 cannot be assigned to linear variable of domain D
+typecheck.bpl(47,9): Error: Linear variable x can occur only once in the right-hand-side of an assignment
+typecheck.bpl(51,4): Error: Linear variable a can occur only once as an input parameter
+typecheck.bpl(53,4): Error: Only variable can be passed to linear parameter b
+typecheck.bpl(55,4): Error: The domains of formal and actual parameters must be the same
+typecheck.bpl(57,4): Error: The domains of formal and actual parameters must be the same
+typecheck.bpl(59,4): Error: Only a linear argument can be passed to linear parameter a
+typecheck.bpl(64,4): Error: Linear variable a can occur only once as an input parameter of a parallel call
+typecheck.bpl(71,0): Error: Output variable d must be available at a return
+typecheck.bpl(80,0): Error: Global variable g must be available at a return
+typecheck.bpl(85,7): Error: unavailable source for a linear read
+typecheck.bpl(86,0): Error: Output variable r must be available at a return
+15 type checking errors detected in typecheck.bpl