From 5c9156cb9422477f0fc1cd34d50753a6f7de09dc Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 7 May 2014 21:20:35 +0100 Subject: Enabled "linear type checking" lit tests. --- Test/linear/Answer | 44 ++++++++++++++++++++-------------------- Test/linear/allocator.bpl | 2 ++ Test/linear/allocator.bpl.expect | 5 +++++ Test/linear/bug.bpl | 2 ++ Test/linear/bug.bpl.expect | 5 +++++ Test/linear/f1.bpl | 2 ++ Test/linear/f1.bpl.expect | 5 +++++ Test/linear/f2.bpl | 2 ++ Test/linear/f2.bpl.expect | 5 +++++ Test/linear/f3.bpl | 2 ++ Test/linear/f3.bpl.expect | 2 ++ Test/linear/list.bpl | 2 ++ Test/linear/list.bpl.expect | 2 ++ Test/linear/typecheck.bpl | 2 ++ Test/linear/typecheck.bpl.expect | 16 +++++++++++++++ 15 files changed, 76 insertions(+), 22 deletions(-) create mode 100644 Test/linear/allocator.bpl.expect create mode 100644 Test/linear/bug.bpl.expect create mode 100644 Test/linear/f1.bpl.expect create mode 100644 Test/linear/f2.bpl.expect create mode 100644 Test/linear/f3.bpl.expect create mode 100644 Test/linear/list.bpl.expect create mode 100644 Test/linear/typecheck.bpl.expect (limited to 'Test/linear') 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 -- cgit v1.2.3