From 962f8d5252b3f5ec4d19e0cd2a430934bd55cc6d Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sun, 28 Jun 2015 01:44:30 +0100 Subject: Normalise line endings using a .gitattributes file. Unfortunately this required that this commit globally modify most files. If you want to use git blame to see the real author of a line use the ``-w`` flag so that whitespace changes are ignored. --- Test/bitvectors/arrays.bpl | 84 +++++++++++++++++++++++----------------------- Test/bitvectors/bv0.bpl | 30 ++++++++--------- Test/bitvectors/bv1.bpl | 38 ++++++++++----------- Test/bitvectors/bv10.bpl | 24 ++++++------- Test/bitvectors/bv2.bpl | 26 +++++++------- Test/bitvectors/bv3.bpl | 10 +++--- Test/bitvectors/bv4.bpl | 50 +++++++++++++-------------- Test/bitvectors/bv5.bpl | 26 +++++++------- Test/bitvectors/bv6.bpl | 22 ++++++------ Test/bitvectors/bv7.bpl | 22 ++++++------ Test/bitvectors/bv8.bpl | 50 +++++++++++++-------------- Test/bitvectors/bv9.bpl | 50 +++++++++++++-------------- 12 files changed, 216 insertions(+), 216 deletions(-) (limited to 'Test/bitvectors') diff --git a/Test/bitvectors/arrays.bpl b/Test/bitvectors/arrays.bpl index dae54e63..c6368fbe 100644 --- a/Test/bitvectors/arrays.bpl +++ b/Test/bitvectors/arrays.bpl @@ -1,43 +1,43 @@ -// RUN: %boogie -proverWarnings:1 "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -const unique f1 : Field int; -const unique f2 : Field bv32; -const unique f3 : Field bool; - -const unique r1 : ref; -const unique r2 : ref; - -var H : [ref,Field x]x; - -procedure foo() - modifies H; -{ - var i : int; - var b : bv32; - var c : bool; - - H[r1, f1] := 3; - H[r1, f2] := 77bv32; - H[r1, f3] := true; - i := H[r1,f1]; - b := H[r1,f2]; - c := H[r1,f3]; - assert i == 3; - assert b == 77bv32; - assert H[r1,f3]; -} - -var B : [bv32]bv32; - -procedure bar() - modifies B; -{ - var b : bv32; - - B[42bv32] := 77bv32; - b := B[42bv32]; - assert b == 77bv32; -} - - +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +const unique f1 : Field int; +const unique f2 : Field bv32; +const unique f3 : Field bool; + +const unique r1 : ref; +const unique r2 : ref; + +var H : [ref,Field x]x; + +procedure foo() + modifies H; +{ + var i : int; + var b : bv32; + var c : bool; + + H[r1, f1] := 3; + H[r1, f2] := 77bv32; + H[r1, f3] := true; + i := H[r1,f1]; + b := H[r1,f2]; + c := H[r1,f3]; + assert i == 3; + assert b == 77bv32; + assert H[r1,f3]; +} + +var B : [bv32]bv32; + +procedure bar() + modifies B; +{ + var b : bv32; + + B[42bv32] := 77bv32; + b := B[42bv32]; + assert b == 77bv32; +} + + type Field a, ref; \ No newline at end of file diff --git a/Test/bitvectors/bv0.bpl b/Test/bitvectors/bv0.bpl index 8c330eda..d5a34bf5 100644 --- a/Test/bitvectors/bv0.bpl +++ b/Test/bitvectors/bv0.bpl @@ -1,15 +1,15 @@ -// RUN: %boogie -proverWarnings:1 "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -procedure foo2(x : bv32) returns(r : bv32) -{ - block1: - r := 17bv31; // Error - r := 17; // Error - r := x[1:0]; // Error - r := x[0:1]; // Error - r := x[55:54]; // Error - r := x[33:32]; // Error - r := 17bv10 ++ 17bv42 ++ 13bv22; // Error - return; -} - +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure foo2(x : bv32) returns(r : bv32) +{ + block1: + r := 17bv31; // Error + r := 17; // Error + r := x[1:0]; // Error + r := x[0:1]; // Error + r := x[55:54]; // Error + r := x[33:32]; // Error + r := 17bv10 ++ 17bv42 ++ 13bv22; // Error + return; +} + diff --git a/Test/bitvectors/bv1.bpl b/Test/bitvectors/bv1.bpl index 2edc5037..7a86bff7 100644 --- a/Test/bitvectors/bv1.bpl +++ b/Test/bitvectors/bv1.bpl @@ -1,19 +1,19 @@ -// RUN: %boogie -proverWarnings:1 "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -procedure foo(x : bv32) returns(r : bv32) -{ - var q : bv64; - - block1: - r := 17bv32; - assert r == r; - assert r[32:0] == r[32:0]; - assert 0bv2 ++ r[12:0] == 0bv2 ++ r[12:0]; - r := 17bv10 ++ 17bv22; - // r := 17; - q := 420000000000bv64; - q := 8444249301319680000bv64; - q := 16444249301319680000bv64; - return; -} - +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure foo(x : bv32) returns(r : bv32) +{ + var q : bv64; + + block1: + r := 17bv32; + assert r == r; + assert r[32:0] == r[32:0]; + assert 0bv2 ++ r[12:0] == 0bv2 ++ r[12:0]; + r := 17bv10 ++ 17bv22; + // r := 17; + q := 420000000000bv64; + q := 8444249301319680000bv64; + q := 16444249301319680000bv64; + return; +} + diff --git a/Test/bitvectors/bv10.bpl b/Test/bitvectors/bv10.bpl index cacf9f7a..6ba4ad7a 100644 --- a/Test/bitvectors/bv10.bpl +++ b/Test/bitvectors/bv10.bpl @@ -1,12 +1,12 @@ -// RUN: %boogie "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -var x: bv32; - -procedure main() -modifies x; -{ - - x := 0bv32; - assume x == 1bv32; - assert false; -} +// RUN: %boogie "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +var x: bv32; + +procedure main() +modifies x; +{ + + x := 0bv32; + assume x == 1bv32; + assert false; +} diff --git a/Test/bitvectors/bv2.bpl b/Test/bitvectors/bv2.bpl index 45fdf7e4..8e2c1dad 100644 --- a/Test/bitvectors/bv2.bpl +++ b/Test/bitvectors/bv2.bpl @@ -1,13 +1,13 @@ -// RUN: %boogie -proverWarnings:1 "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -procedure foo2(x : bv32) returns(r : bv32) -{ - block1: - r := x[-1:1]; // Error -// r := x[x:1]; // Error - r := x[1:x]; // Error - r := x[1+1:3]; // Error - return; -} - - +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure foo2(x : bv32) returns(r : bv32) +{ + block1: + r := x[-1:1]; // Error +// r := x[x:1]; // Error + r := x[1:x]; // Error + r := x[1+1:3]; // Error + return; +} + + diff --git a/Test/bitvectors/bv3.bpl b/Test/bitvectors/bv3.bpl index 5a2ce47f..5b21ca59 100644 --- a/Test/bitvectors/bv3.bpl +++ b/Test/bitvectors/bv3.bpl @@ -1,5 +1,5 @@ -// RUN: %boogie -proverWarnings:1 "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -type bv; -type bv16; - +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +type bv; +type bv16; + diff --git a/Test/bitvectors/bv4.bpl b/Test/bitvectors/bv4.bpl index 29c8130a..1e7b6e31 100644 --- a/Test/bitvectors/bv4.bpl +++ b/Test/bitvectors/bv4.bpl @@ -1,25 +1,25 @@ -// RUN: %boogie -proverWarnings:1 "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -function a() returns(bv32); -axiom a() == a(); - -axiom 0bv5 != 1bv5; - - -// ------------------------- -type $x; -function g() returns($x); -type Field x; -var $gmem : [ref, Field x] x; -const unique f : Field $x; - -procedure qq() - modifies $gmem; -{ - $gmem[null, f] := g(); -} - - -type ref; -const null : ref; +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +function a() returns(bv32); +axiom a() == a(); + +axiom 0bv5 != 1bv5; + + +// ------------------------- +type $x; +function g() returns($x); +type Field x; +var $gmem : [ref, Field x] x; +const unique f : Field $x; + +procedure qq() + modifies $gmem; +{ + $gmem[null, f] := g(); +} + + +type ref; +const null : ref; diff --git a/Test/bitvectors/bv5.bpl b/Test/bitvectors/bv5.bpl index 73dff1ad..048bc315 100644 --- a/Test/bitvectors/bv5.bpl +++ b/Test/bitvectors/bv5.bpl @@ -1,13 +1,13 @@ -// RUN: %boogie "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -procedure P() returns () { - var m : [a]int; - - m[23bv5] := 17; - m[21bv5] := 19; - m[21bv6] := -3; - - assert m[23bv5] == 17; - assert m[21bv6] == 3; // should not be provable -} +// RUN: %boogie "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +procedure P() returns () { + var m : [a]int; + + m[23bv5] := 17; + m[21bv5] := 19; + m[21bv6] := -3; + + assert m[23bv5] == 17; + assert m[21bv6] == 3; // should not be provable +} diff --git a/Test/bitvectors/bv6.bpl b/Test/bitvectors/bv6.bpl index d0654b6f..7ff4777f 100644 --- a/Test/bitvectors/bv6.bpl +++ b/Test/bitvectors/bv6.bpl @@ -1,11 +1,11 @@ -// RUN: %boogie "%s" > "%t" -// RUN: %diff "%s.expect" "%t" - -procedure Q() returns () { - var x : bv32, y : bv16; - - x := y ++ y; - assert x[16:0] == y; - assert x == x[16:0] ++ y; - assert x[17:1] == y; // should not be verifiable -} +// RUN: %boogie "%s" > "%t" +// RUN: %diff "%s.expect" "%t" + +procedure Q() returns () { + var x : bv32, y : bv16; + + x := y ++ y; + assert x[16:0] == y; + assert x == x[16:0] ++ y; + assert x[17:1] == y; // should not be verifiable +} diff --git a/Test/bitvectors/bv7.bpl b/Test/bitvectors/bv7.bpl index a60f9547..5d32dda4 100644 --- a/Test/bitvectors/bv7.bpl +++ b/Test/bitvectors/bv7.bpl @@ -1,11 +1,11 @@ -// RUN: %boogie -proverWarnings:1 "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -procedure foo2(x : bv32) returns(r : bv32) -{ - block1: - r := x[x:1]; // Error - r := x[(1:13)]; // Error - return; -} - - +// RUN: %boogie -proverWarnings:1 "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure foo2(x : bv32) returns(r : bv32) +{ + block1: + r := x[x:1]; // Error + r := x[(1:13)]; // Error + return; +} + + diff --git a/Test/bitvectors/bv8.bpl b/Test/bitvectors/bv8.bpl index ee572998..557eb4e8 100644 --- a/Test/bitvectors/bv8.bpl +++ b/Test/bitvectors/bv8.bpl @@ -1,25 +1,25 @@ -// RUN: %boogie "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -// This file includes some tests for which Boogie once generated bad Z3 input - -procedure foo() -{ - var r: bv3; - var s: bv6; - var u: bv15; - var t: bv24; - - t := t[8: 0] ++ t[10: 0] ++ t[24: 18]; - t := (r ++ s) ++ u; - t := t[16: 0] ++ t[8: 0]; -} - -procedure bar() -{ - var a: bv64; - var b: bv32; - var c: bv8; - - c := a[8:0]; - c := b[8:0]; -} +// RUN: %boogie "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +// This file includes some tests for which Boogie once generated bad Z3 input + +procedure foo() +{ + var r: bv3; + var s: bv6; + var u: bv15; + var t: bv24; + + t := t[8: 0] ++ t[10: 0] ++ t[24: 18]; + t := (r ++ s) ++ u; + t := t[16: 0] ++ t[8: 0]; +} + +procedure bar() +{ + var a: bv64; + var b: bv32; + var c: bv8; + + c := a[8:0]; + c := b[8:0]; +} diff --git a/Test/bitvectors/bv9.bpl b/Test/bitvectors/bv9.bpl index 19a147ad..11c5156b 100644 --- a/Test/bitvectors/bv9.bpl +++ b/Test/bitvectors/bv9.bpl @@ -1,25 +1,25 @@ -// RUN: %boogie -proverOpt:OPTIMIZE_FOR_BV=true "%s" > "%t" -// RUN: %diff "%s.expect" "%t" -procedure foo(); - -implementation foo() -{ - assert (forall Q#a$1^15.32#tc1: bv64, Q#b$1^15.32#tc1: bv64, Q#c$1^15.32#tc1: bv64 :: true && true && true ==> ($bv_bvadd64(Q#a$1^15.32#tc1, Q#b$1^15.32#tc1) == Q#c$1^15.32#tc1 || $bv_bvadd64($bv_bvadd64(Q#a$1^15.32#tc1, Q#b$1^15.32#tc1), 1bv64) == Q#c$1^15.32#tc1) && (if Q#c$1^15.32#tc1 == $bv_bvadd64(Q#a$1^15.32#tc1, Q#b$1^15.32#tc1) then $bv_bvugt64(Q#a$1^15.32#tc1, $bv_bvsub64(18446744073709551615bv64, Q#b$1^15.32#tc1)) else $bv_bvuge64(Q#a$1^15.32#tc1, $bv_bvsub64(18446744073709551615bv64, Q#b$1^15.32#tc1))) ==> $bv_bvlshr64($bv_bvxor64($bv_bvor64(Q#a$1^15.32#tc1, Q#b$1^15.32#tc1), $bv_bvand64($bv_bvxor64(Q#a$1^15.32#tc1, Q#b$1^15.32#tc1), Q#c$1^15.32#tc1)), 0bv32 ++ 63bv32) == 1bv64); -} - -function {:bvbuiltin "bvlshr"} $bv_bvlshr64(p1: bv64, p2: bv64) : bv64; - -function {:bvbuiltin "bvand"} $bv_bvand64(p1: bv64, p2: bv64) : bv64; - -function {:bvbuiltin "bvor"} $bv_bvor64(p1: bv64, p2: bv64) : bv64; - -function {:bvbuiltin "bvxor"} $bv_bvxor64(p1: bv64, p2: bv64) : bv64; - -function {:bvbuiltin "bvuge"} $bv_bvuge64(p1: bv64, p2: bv64) : bool; - -function {:bvbuiltin "bvugt"} $bv_bvugt64(p1: bv64, p2: bv64) : bool; - -function {:bvbuiltin "bvsub"} $bv_bvsub64(p1: bv64, p2: bv64) : bv64; - -function {:bvbuiltin "bvadd"} $bv_bvadd64(p1: bv64, p2: bv64) : bv64; - +// RUN: %boogie -proverOpt:OPTIMIZE_FOR_BV=true "%s" > "%t" +// RUN: %diff "%s.expect" "%t" +procedure foo(); + +implementation foo() +{ + assert (forall Q#a$1^15.32#tc1: bv64, Q#b$1^15.32#tc1: bv64, Q#c$1^15.32#tc1: bv64 :: true && true && true ==> ($bv_bvadd64(Q#a$1^15.32#tc1, Q#b$1^15.32#tc1) == Q#c$1^15.32#tc1 || $bv_bvadd64($bv_bvadd64(Q#a$1^15.32#tc1, Q#b$1^15.32#tc1), 1bv64) == Q#c$1^15.32#tc1) && (if Q#c$1^15.32#tc1 == $bv_bvadd64(Q#a$1^15.32#tc1, Q#b$1^15.32#tc1) then $bv_bvugt64(Q#a$1^15.32#tc1, $bv_bvsub64(18446744073709551615bv64, Q#b$1^15.32#tc1)) else $bv_bvuge64(Q#a$1^15.32#tc1, $bv_bvsub64(18446744073709551615bv64, Q#b$1^15.32#tc1))) ==> $bv_bvlshr64($bv_bvxor64($bv_bvor64(Q#a$1^15.32#tc1, Q#b$1^15.32#tc1), $bv_bvand64($bv_bvxor64(Q#a$1^15.32#tc1, Q#b$1^15.32#tc1), Q#c$1^15.32#tc1)), 0bv32 ++ 63bv32) == 1bv64); +} + +function {:bvbuiltin "bvlshr"} $bv_bvlshr64(p1: bv64, p2: bv64) : bv64; + +function {:bvbuiltin "bvand"} $bv_bvand64(p1: bv64, p2: bv64) : bv64; + +function {:bvbuiltin "bvor"} $bv_bvor64(p1: bv64, p2: bv64) : bv64; + +function {:bvbuiltin "bvxor"} $bv_bvxor64(p1: bv64, p2: bv64) : bv64; + +function {:bvbuiltin "bvuge"} $bv_bvuge64(p1: bv64, p2: bv64) : bool; + +function {:bvbuiltin "bvugt"} $bv_bvugt64(p1: bv64, p2: bv64) : bool; + +function {:bvbuiltin "bvsub"} $bv_bvsub64(p1: bv64, p2: bv64) : bv64; + +function {:bvbuiltin "bvadd"} $bv_bvadd64(p1: bv64, p2: bv64) : bv64; + -- cgit v1.2.3