diff options
48 files changed, 150 insertions, 21 deletions
diff --git a/Test/og/Answer b/Test/og/Answer index b82acad4..4b1bceae 100644 --- a/Test/og/Answer +++ b/Test/og/Answer @@ -1,25 +1,25 @@ -------------------- foo.bpl --------------------
-foo.bpl(28,3): Error: Non-interference check failed
+foo.bpl(30,3): Error: Non-interference check failed
Execution trace:
- foo.bpl(5,3): anon0
- foo.bpl(5,3): anon0$1
- foo.bpl(12,3): inline$Incr_1$0$this_A
+ foo.bpl(7,3): anon0
+ foo.bpl(7,3): anon0$1
+ foo.bpl(14,3): inline$Incr_1$0$this_A
(0,0): inline$Impl_YieldChecker_PC_1$1$L0
Boogie program verifier finished with 9 verified, 1 error
-------------------- bar.bpl --------------------
-bar.bpl(26,3): Error: Non-interference check failed
+bar.bpl(28,3): Error: Non-interference check failed
Execution trace:
- bar.bpl(5,3): anon0
- bar.bpl(5,3): anon0$1
- bar.bpl(12,3): inline$Incr_1$0$this_A
+ bar.bpl(7,3): anon0
+ bar.bpl(7,3): anon0$1
+ bar.bpl(14,3): inline$Incr_1$0$this_A
(0,0): inline$Impl_YieldChecker_PC_1$1$L0
-bar.bpl(26,3): Error: Non-interference check failed
+bar.bpl(28,3): Error: Non-interference check failed
Execution trace:
- bar.bpl(36,3): anon0
- bar.bpl(36,3): anon0$1
+ bar.bpl(38,3): anon0
+ bar.bpl(38,3): anon0$1
(0,0): inline$Impl_YieldChecker_PC_1$1$L0
Boogie program verifier finished with 8 verified, 2 errors
@@ -29,11 +29,11 @@ Boogie program verifier finished with 8 verified, 2 errors Boogie program verifier finished with 3 verified, 0 errors
-------------------- parallel1.bpl --------------------
-parallel1.bpl(28,3): Error: Non-interference check failed
+parallel1.bpl(30,3): Error: Non-interference check failed
Execution trace:
- parallel1.bpl(5,3): anon0
- parallel1.bpl(5,3): anon0$1
- parallel1.bpl(12,3): inline$Incr_1$0$this_A
+ parallel1.bpl(7,3): anon0
+ parallel1.bpl(7,3): anon0$1
+ parallel1.bpl(14,3): inline$Incr_1$0$this_A
(0,0): inline$Impl_YieldChecker_PC_1$1$L0
Boogie program verifier finished with 7 verified, 1 error
@@ -55,10 +55,10 @@ Boogie program verifier finished with 6 verified, 0 errors Boogie program verifier finished with 8 verified, 0 errors
-------------------- parallel4.bpl --------------------
-parallel4.bpl(24,3): Error BP5001: This assertion might not hold.
+parallel4.bpl(26,3): Error BP5001: This assertion might not hold.
Execution trace:
(0,0): og_init
- parallel4.bpl(22,5): anon0$1
+ parallel4.bpl(24,5): anon0$1
Boogie program verifier finished with 5 verified, 1 error
@@ -71,13 +71,13 @@ Boogie program verifier finished with 8 verified, 0 errors Boogie program verifier finished with 6 verified, 0 errors
-------------------- t1.bpl --------------------
-t1.bpl(58,5): Error: Non-interference check failed
+t1.bpl(60,5): Error: Non-interference check failed
Execution trace:
(0,0): og_init
- t1.bpl(78,13): anon0
- t1.bpl(78,13): anon0$1
+ t1.bpl(80,13): anon0
+ t1.bpl(80,13): anon0$1
(0,0): inline$SetG_1$0$Entry
- t1.bpl(78,13): anon0$2
+ t1.bpl(80,13): anon0$2
(0,0): inline$Impl_YieldChecker_A_1$1$L2
Boogie program verifier finished with 5 verified, 1 error
diff --git a/Test/og/DeviceCache.bpl b/Test/og/DeviceCache.bpl index 23f36ae5..59723dc8 100644 --- a/Test/og/DeviceCache.bpl +++ b/Test/og/DeviceCache.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
+// RUN: %diff %s.expect %t
type X;
function {:builtin "MapConst"} mapconstbool(bool): [X]bool;
const nil: X;
diff --git a/Test/og/DeviceCache.bpl.expect b/Test/og/DeviceCache.bpl.expect new file mode 100644 index 00000000..11d204a8 --- /dev/null +++ b/Test/og/DeviceCache.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 35 verified, 0 errors diff --git a/Test/og/DeviceCacheSimplified.bpl b/Test/og/DeviceCacheSimplified.bpl index 28e8b662..3365e565 100644 --- a/Test/og/DeviceCacheSimplified.bpl +++ b/Test/og/DeviceCacheSimplified.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
+// RUN: %diff %s.expect %t
type X;
function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;
diff --git a/Test/og/DeviceCacheWithBuffer.bpl b/Test/og/DeviceCacheWithBuffer.bpl index f1da0ecf..a5252b87 100644 --- a/Test/og/DeviceCacheWithBuffer.bpl +++ b/Test/og/DeviceCacheWithBuffer.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
+// RUN: %diff %s.expect %t
type X;
function {:builtin "MapConst"} mapconstbool(bool): [X]bool;
const nil: X;
diff --git a/Test/og/FlanaganQadeer.bpl b/Test/og/FlanaganQadeer.bpl index 2fddf217..4c664ec4 100644 --- a/Test/og/FlanaganQadeer.bpl +++ b/Test/og/FlanaganQadeer.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
+// RUN: %diff %s.expect %t
type X;
const nil: X;
var {:phase 1} l: X;
diff --git a/Test/og/FlanaganQadeer.bpl.expect b/Test/og/FlanaganQadeer.bpl.expect new file mode 100644 index 00000000..9823d44a --- /dev/null +++ b/Test/og/FlanaganQadeer.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 6 verified, 0 errors diff --git a/Test/og/akash.bpl b/Test/og/akash.bpl index 90ccfebe..37bba956 100644 --- a/Test/og/akash.bpl +++ b/Test/og/akash.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
+// RUN: %diff %s.expect %t
function {:builtin "MapConst"} mapconstbool(bool) : [int]bool;
function {:builtin "MapConst"} MapConstBool(bool) : [int]bool;
diff --git a/Test/og/akash.bpl.expect b/Test/og/akash.bpl.expect new file mode 100644 index 00000000..9823d44a --- /dev/null +++ b/Test/og/akash.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 6 verified, 0 errors diff --git a/Test/og/async.bpl b/Test/og/async.bpl index 4ca43d30..88307ba1 100644 --- a/Test/og/async.bpl +++ b/Test/og/async.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
+// RUN: %diff %s.expect %t
var {:phase 1} x: int;
var {:phase 1} y: int;
diff --git a/Test/og/bar.bpl b/Test/og/bar.bpl index 22751d29..26a4eb46 100644 --- a/Test/og/bar.bpl +++ b/Test/og/bar.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer %s > %t
+// RUN: %diff %s.expect %t
var {:phase 1} g:int;
procedure {:yields} {:phase 1} PB()
diff --git a/Test/og/bar.bpl.expect b/Test/og/bar.bpl.expect new file mode 100644 index 00000000..d59bd019 --- /dev/null +++ b/Test/og/bar.bpl.expect @@ -0,0 +1,13 @@ +bar.bpl(28,3): Error: Non-interference check failed +Execution trace: + bar.bpl(7,3): anon0 + bar.bpl(7,3): anon0$1 + bar.bpl(14,3): inline$Incr_1$0$this_A + (0,0): inline$Impl_YieldChecker_PC_1$1$L0 +bar.bpl(28,3): Error: Non-interference check failed +Execution trace: + bar.bpl(38,3): anon0 + bar.bpl(38,3): anon0$1 + (0,0): inline$Impl_YieldChecker_PC_1$1$L0 + +Boogie program verifier finished with 8 verified, 2 errors diff --git a/Test/og/civl-paper.bpl b/Test/og/civl-paper.bpl index 378bb8b5..9d82e229 100644 --- a/Test/og/civl-paper.bpl +++ b/Test/og/civl-paper.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
+// RUN: %diff %s.expect %t
type X;
const nil: X;
diff --git a/Test/og/civl-paper.bpl.expect b/Test/og/civl-paper.bpl.expect new file mode 100644 index 00000000..812c54cc --- /dev/null +++ b/Test/og/civl-paper.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 28 verified, 0 errors diff --git a/Test/og/foo.bpl b/Test/og/foo.bpl index 400f5a4e..ba05d666 100644 --- a/Test/og/foo.bpl +++ b/Test/og/foo.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer %s > %t
+// RUN: %diff %s.expect %t
var {:phase 1} g:int;
procedure {:yields} {:phase 1} PB()
diff --git a/Test/og/foo.bpl.expect b/Test/og/foo.bpl.expect new file mode 100644 index 00000000..b386f3f6 --- /dev/null +++ b/Test/og/foo.bpl.expect @@ -0,0 +1,8 @@ +foo.bpl(30,3): Error: Non-interference check failed +Execution trace: + foo.bpl(7,3): anon0 + foo.bpl(7,3): anon0$1 + foo.bpl(14,3): inline$Incr_1$0$this_A + (0,0): inline$Impl_YieldChecker_PC_1$1$L0 + +Boogie program verifier finished with 9 verified, 1 error diff --git a/Test/og/houd1.bpl b/Test/og/houd1.bpl index aff53a48..03d52e54 100644 --- a/Test/og/houd1.bpl +++ b/Test/og/houd1.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
+// RUN: %diff %s.expect %t
const {:existential true} b0: bool;
const {:existential true} b1: bool;
const {:existential true} b2: bool;
diff --git a/Test/og/linear-set.bpl b/Test/og/linear-set.bpl index 9effc04d..f6a4de75 100644 --- a/Test/og/linear-set.bpl +++ b/Test/og/linear-set.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
+// RUN: %diff %s.expect %t
type X;
function {:builtin "MapConst"} MapConstInt(int) : [X]int;
function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;
diff --git a/Test/og/linear-set.bpl.expect b/Test/og/linear-set.bpl.expect new file mode 100644 index 00000000..00ddb38b --- /dev/null +++ b/Test/og/linear-set.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 4 verified, 0 errors diff --git a/Test/og/linear-set2.bpl b/Test/og/linear-set2.bpl index 36a8f9c7..dff4936c 100644 --- a/Test/og/linear-set2.bpl +++ b/Test/og/linear-set2.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
+// RUN: %diff %s.expect %t
type X;
function {:builtin "MapConst"} MapConstInt(int) : [X]int;
function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;
diff --git a/Test/og/linear-set2.bpl.expect b/Test/og/linear-set2.bpl.expect new file mode 100644 index 00000000..00ddb38b --- /dev/null +++ b/Test/og/linear-set2.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 4 verified, 0 errors diff --git a/Test/og/lock-introduced.bpl b/Test/og/lock-introduced.bpl index 928b3d00..f0825c14 100644 --- a/Test/og/lock-introduced.bpl +++ b/Test/og/lock-introduced.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
+// RUN: %diff %s.expect %t
function {:builtin "MapConst"} MapConstBool(bool) : [X]bool;
function {:inline} {:linear "tid"} TidCollector(x: X) : [X]bool
{
diff --git a/Test/og/lock.bpl b/Test/og/lock.bpl index 8357d36d..044cde1e 100644 --- a/Test/og/lock.bpl +++ b/Test/og/lock.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
+// RUN: %diff %s.expect %t
var {:phase 2} b: bool;
procedure {:yields} {:phase 2} main()
diff --git a/Test/og/lock.bpl.expect b/Test/og/lock.bpl.expect new file mode 100644 index 00000000..76a9a2bf --- /dev/null +++ b/Test/og/lock.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 8 verified, 0 errors diff --git a/Test/og/lock2.bpl b/Test/og/lock2.bpl index 9f5e0be8..2d1c53df 100644 --- a/Test/og/lock2.bpl +++ b/Test/og/lock2.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
+// RUN: %diff %s.expect %t
var {:phase 2} b: int;
procedure {:yields} {:phase 2} main()
diff --git a/Test/og/lock2.bpl.expect b/Test/og/lock2.bpl.expect new file mode 100644 index 00000000..76a9a2bf --- /dev/null +++ b/Test/og/lock2.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 8 verified, 0 errors diff --git a/Test/og/multiset.bpl b/Test/og/multiset.bpl index 459cb470..f0a2fd5b 100644 --- a/Test/og/multiset.bpl +++ b/Test/og/multiset.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
+// RUN: %diff %s.expect %t
type X;
const unique null : int;
diff --git a/Test/og/multiset.bpl.expect b/Test/og/multiset.bpl.expect new file mode 100644 index 00000000..63682bb4 --- /dev/null +++ b/Test/og/multiset.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 85 verified, 0 errors diff --git a/Test/og/new1.bpl b/Test/og/new1.bpl index 6854e29c..a691c087 100644 --- a/Test/og/new1.bpl +++ b/Test/og/new1.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
+// RUN: %diff %s.expect %t
function {:builtin "MapConst"} mapconstbool(x:bool): [int]bool;
var {:phase 1} g:int;
diff --git a/Test/og/new1.bpl.expect b/Test/og/new1.bpl.expect new file mode 100644 index 00000000..00ddb38b --- /dev/null +++ b/Test/og/new1.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 4 verified, 0 errors diff --git a/Test/og/one.bpl b/Test/og/one.bpl index 1da2f116..190a024a 100644 --- a/Test/og/one.bpl +++ b/Test/og/one.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer %s > %t
+// RUN: %diff %s.expect %t
var {:phase 1} x:int;
procedure {:yields} {:phase 0,1} Set(v: int);
diff --git a/Test/og/one.bpl.expect b/Test/og/one.bpl.expect new file mode 100644 index 00000000..a9949f2e --- /dev/null +++ b/Test/og/one.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 3 verified, 0 errors diff --git a/Test/og/parallel1.bpl b/Test/og/parallel1.bpl index 427dc72d..90846b6c 100644 --- a/Test/og/parallel1.bpl +++ b/Test/og/parallel1.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer %s > %t
+// RUN: %diff %s.expect %t
var {:phase 1} g:int;
procedure {:yields} {:phase 1} PB()
diff --git a/Test/og/parallel1.bpl.expect b/Test/og/parallel1.bpl.expect new file mode 100644 index 00000000..5fc0cbf6 --- /dev/null +++ b/Test/og/parallel1.bpl.expect @@ -0,0 +1,8 @@ +parallel1.bpl(30,3): Error: Non-interference check failed +Execution trace: + parallel1.bpl(7,3): anon0 + parallel1.bpl(7,3): anon0$1 + parallel1.bpl(14,3): inline$Incr_1$0$this_A + (0,0): inline$Impl_YieldChecker_PC_1$1$L0 + +Boogie program verifier finished with 7 verified, 1 error diff --git a/Test/og/parallel2.bpl b/Test/og/parallel2.bpl index 1bce7c8a..52c2e913 100644 --- a/Test/og/parallel2.bpl +++ b/Test/og/parallel2.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
+// RUN: %diff %s.expect %t
var {:phase 1} a:[int]int;
function {:builtin "MapConst"} MapConstBool(bool) : [int]bool;
diff --git a/Test/og/parallel2.bpl.expect b/Test/og/parallel2.bpl.expect new file mode 100644 index 00000000..76a9a2bf --- /dev/null +++ b/Test/og/parallel2.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 8 verified, 0 errors diff --git a/Test/og/parallel4.bpl b/Test/og/parallel4.bpl index 2a2feb2d..4bffcf94 100644 --- a/Test/og/parallel4.bpl +++ b/Test/og/parallel4.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
+// RUN: %diff %s.expect %t
var {:phase 1} a:int;
procedure Allocate() returns ({:linear "tid"} xls: int);
diff --git a/Test/og/parallel4.bpl.expect b/Test/og/parallel4.bpl.expect new file mode 100644 index 00000000..7c696364 --- /dev/null +++ b/Test/og/parallel4.bpl.expect @@ -0,0 +1,6 @@ +parallel4.bpl(26,3): Error BP5001: This assertion might not hold. +Execution trace: + (0,0): og_init + parallel4.bpl(24,5): anon0$1 + +Boogie program verifier finished with 5 verified, 1 error diff --git a/Test/og/parallel5.bpl b/Test/og/parallel5.bpl index a73af06e..5f0b30bf 100644 --- a/Test/og/parallel5.bpl +++ b/Test/og/parallel5.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
+// RUN: %diff %s.expect %t
var {:phase 1} a:[int]int;
procedure Allocate() returns ({:linear "tid"} xls: int);
diff --git a/Test/og/parallel5.bpl.expect b/Test/og/parallel5.bpl.expect new file mode 100644 index 00000000..76a9a2bf --- /dev/null +++ b/Test/og/parallel5.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 8 verified, 0 errors diff --git a/Test/og/perm.bpl b/Test/og/perm.bpl index 6d07ca75..3f5adedd 100644 --- a/Test/og/perm.bpl +++ b/Test/og/perm.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
+// RUN: %diff %s.expect %t
var {:phase 1} x: int;
function {:builtin "MapConst"} ch_mapconstbool(x: bool) : [int]bool;
diff --git a/Test/og/perm.bpl.expect b/Test/og/perm.bpl.expect new file mode 100644 index 00000000..00ddb38b --- /dev/null +++ b/Test/og/perm.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 4 verified, 0 errors diff --git a/Test/og/t1.bpl b/Test/og/t1.bpl index c7e30dd9..c4964c0e 100644 --- a/Test/og/t1.bpl +++ b/Test/og/t1.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
+// RUN: %diff %s.expect %t
function {:builtin "MapConst"} mapconstbool(bool) : [int]bool;
function {:builtin "MapConst"} MapConstBool(bool) : [int]bool;
diff --git a/Test/og/t1.bpl.expect b/Test/og/t1.bpl.expect new file mode 100644 index 00000000..9f9e44b1 --- /dev/null +++ b/Test/og/t1.bpl.expect @@ -0,0 +1,10 @@ +t1.bpl(60,5): Error: Non-interference check failed +Execution trace: + (0,0): og_init + t1.bpl(80,13): anon0 + t1.bpl(80,13): anon0$1 + (0,0): inline$SetG_1$0$Entry + t1.bpl(80,13): anon0$2 + (0,0): inline$Impl_YieldChecker_A_1$1$L2 + +Boogie program verifier finished with 5 verified, 1 error diff --git a/Test/og/termination.bpl b/Test/og/termination.bpl index 80109bf4..a7969e7c 100644 --- a/Test/og/termination.bpl +++ b/Test/og/termination.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
+// RUN: %diff %s.expect %t
procedure {:yields} X();
ensures {:atomic 0} |{ A: return true; }|;
diff --git a/Test/og/ticket.bpl b/Test/og/ticket.bpl index fb347935..3ee7485b 100644 --- a/Test/og/ticket.bpl +++ b/Test/og/ticket.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
+// RUN: %diff %s.expect %t
function RightOpen(n: int) : [int]bool;
function RightClosed(n: int) : [int]bool;
axiom (forall x: int, y: int :: RightOpen(x)[y] <==> y < x);
diff --git a/Test/og/ticket.bpl.expect b/Test/og/ticket.bpl.expect new file mode 100644 index 00000000..812c54cc --- /dev/null +++ b/Test/og/ticket.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 28 verified, 0 errors diff --git a/Test/og/treiber-stack.bpl b/Test/og/treiber-stack.bpl index 6e87d8f3..e082c4ca 100644 --- a/Test/og/treiber-stack.bpl +++ b/Test/og/treiber-stack.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory %s > %t
+// RUN: %diff %s.expect %t
type Node;
type lmap;
function {:linear "Node"} dom(lmap): [Node]bool;
|