diff options
| -rw-r--r-- | Test/textbook/BQueue.bpl | 2 | ||||
| -rw-r--r-- | Test/textbook/BQueue.bpl.expect | 2 | ||||
| -rw-r--r-- | Test/textbook/Bubble.bpl | 2 | ||||
| -rw-r--r-- | Test/textbook/Bubble.bpl.expect | 2 | ||||
| -rw-r--r-- | Test/textbook/DivMod.bpl | 2 | ||||
| -rw-r--r-- | Test/textbook/DivMod.bpl.expect | 2 | ||||
| -rw-r--r-- | Test/textbook/DutchFlag.bpl | 2 | ||||
| -rw-r--r-- | Test/textbook/DutchFlag.bpl.expect | 2 | ||||
| -rw-r--r-- | Test/textbook/Find.bpl | 2 | ||||
| -rw-r--r-- | Test/textbook/Find.bpl.expect | 2 | ||||
| -rw-r--r-- | Test/textbook/McCarthy-91.bpl | 2 | ||||
| -rw-r--r-- | Test/textbook/McCarthy-91.bpl.expect | 2 | ||||
| -rw-r--r-- | Test/textbook/TuringFactorial.bpl | 2 | ||||
| -rw-r--r-- | Test/textbook/TuringFactorial.bpl.expect | 2 |
14 files changed, 28 insertions, 0 deletions
diff --git a/Test/textbook/BQueue.bpl b/Test/textbook/BQueue.bpl index 77f1efb3..1c52a0e8 100644 --- a/Test/textbook/BQueue.bpl +++ b/Test/textbook/BQueue.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie %s > %t
+// RUN: %diff %s.expect %t
// BQueue.bpl
// A queue program specified in the style of dynamic frames.
// Rustan Leino, Michal Moskal, and Wolfram Schulte, 2007.
diff --git a/Test/textbook/BQueue.bpl.expect b/Test/textbook/BQueue.bpl.expect new file mode 100644 index 00000000..76a9a2bf --- /dev/null +++ b/Test/textbook/BQueue.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 8 verified, 0 errors diff --git a/Test/textbook/Bubble.bpl b/Test/textbook/Bubble.bpl index 80ecc9a0..937ab7e5 100644 --- a/Test/textbook/Bubble.bpl +++ b/Test/textbook/Bubble.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie %s > %t
+// RUN: %diff %s.expect %t
// Bubble Sort, where the specification says the output is a permutation of
// the input.
diff --git a/Test/textbook/Bubble.bpl.expect b/Test/textbook/Bubble.bpl.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/textbook/Bubble.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/textbook/DivMod.bpl b/Test/textbook/DivMod.bpl index 4a551b6e..de218604 100644 --- a/Test/textbook/DivMod.bpl +++ b/Test/textbook/DivMod.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie %s > %t
+// RUN: %diff %s.expect %t
// This file contains two definitions of integer div/mod (truncated division, as is
// used in C, C#, Java, and several other languages, and Euclidean division, which
// has mathematical appeal and is used by SMT Lib) and proves the correct
diff --git a/Test/textbook/DivMod.bpl.expect b/Test/textbook/DivMod.bpl.expect new file mode 100644 index 00000000..41374b00 --- /dev/null +++ b/Test/textbook/DivMod.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 2 verified, 0 errors diff --git a/Test/textbook/DutchFlag.bpl b/Test/textbook/DutchFlag.bpl index 03fd2317..64743303 100644 --- a/Test/textbook/DutchFlag.bpl +++ b/Test/textbook/DutchFlag.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie %s > %t
+// RUN: %diff %s.expect %t
// The partition step of Quick Sort picks a 'pivot' element from a specified subsection
// of a given integer array. It then partially sorts the elements of the array so that
// elements smaller than the pivot end up to the left of the pivot and elements larger
diff --git a/Test/textbook/DutchFlag.bpl.expect b/Test/textbook/DutchFlag.bpl.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/textbook/DutchFlag.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/textbook/Find.bpl b/Test/textbook/Find.bpl index effedf92..2b149baf 100644 --- a/Test/textbook/Find.bpl +++ b/Test/textbook/Find.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie %s > %t
+// RUN: %diff %s.expect %t
// Declare a constant 'K' and a function 'f' and postulate that 'K' is
// in the image of 'f'
const K: int;
diff --git a/Test/textbook/Find.bpl.expect b/Test/textbook/Find.bpl.expect new file mode 100644 index 00000000..41374b00 --- /dev/null +++ b/Test/textbook/Find.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 2 verified, 0 errors diff --git a/Test/textbook/McCarthy-91.bpl b/Test/textbook/McCarthy-91.bpl index 899a7ff1..895c8e8c 100644 --- a/Test/textbook/McCarthy-91.bpl +++ b/Test/textbook/McCarthy-91.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie %s > %t
+// RUN: %diff %s.expect %t
// McCarthy 91 function
procedure F(n: int) returns (r: int)
ensures 100 < n ==> r == n - 10;
diff --git a/Test/textbook/McCarthy-91.bpl.expect b/Test/textbook/McCarthy-91.bpl.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/textbook/McCarthy-91.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors diff --git a/Test/textbook/TuringFactorial.bpl b/Test/textbook/TuringFactorial.bpl index 37a3cb46..d0c40e84 100644 --- a/Test/textbook/TuringFactorial.bpl +++ b/Test/textbook/TuringFactorial.bpl @@ -1,3 +1,5 @@ +// RUN: %boogie %s > %t
+// RUN: %diff %s.expect %t
// A Boogie version of Turing's additive factorial program, from "Checking a large routine"
// published in the "Report of a Conference of High Speed Automatic Calculating Machines",
// pp. 67-69, 1949.
diff --git a/Test/textbook/TuringFactorial.bpl.expect b/Test/textbook/TuringFactorial.bpl.expect new file mode 100644 index 00000000..37fad75c --- /dev/null +++ b/Test/textbook/TuringFactorial.bpl.expect @@ -0,0 +1,2 @@ + +Boogie program verifier finished with 1 verified, 0 errors |