From 02aca9ffab2d5a63e89f83d5eadb7133132c3b0a Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 27 May 2014 20:53:49 +0100 Subject: Fix lit test suite when running Boogie under a path that contains spaces. --- Test/test21/BooleanQuantification.bpl | 12 ++++++------ Test/test21/BooleanQuantification2.bpl | 12 ++++++------ Test/test21/Boxing.bpl | 12 ++++++------ Test/test21/Casts.bpl | 12 ++++++------ Test/test21/Coercions2.bpl | 12 ++++++------ Test/test21/Colors.bpl | 12 ++++++------ Test/test21/DisjointDomains.bpl | 12 ++++++------ Test/test21/DisjointDomains2.bpl | 12 ++++++------ Test/test21/EmptyList.bpl | 12 ++++++------ Test/test21/EmptySetBug.bpl | 12 ++++++------ Test/test21/Flattening.bpl | 12 ++++++------ Test/test21/FunAxioms.bpl | 12 ++++++------ Test/test21/FunAxioms2.bpl | 12 ++++++------ Test/test21/HeapAbstraction.bpl | 12 ++++++------ Test/test21/HeapAxiom.bpl | 12 ++++++------ Test/test21/InterestingExamples0.bpl | 12 ++++++------ Test/test21/InterestingExamples1.bpl | 12 ++++++------ Test/test21/InterestingExamples2.bpl | 12 ++++++------ Test/test21/InterestingExamples3.bpl | 12 ++++++------ Test/test21/InterestingExamples4.bpl | 12 ++++++------ Test/test21/InterestingExamples5.bpl | 12 ++++++------ Test/test21/Keywords.bpl | 12 ++++++------ Test/test21/LargeLiterals0.bpl | 12 ++++++------ Test/test21/LetSorting.bpl | 12 ++++++------ Test/test21/MapAxiomsConsistency.bpl | 12 ++++++------ Test/test21/MapOutputTypeParams.bpl | 12 ++++++------ Test/test21/Maps0.bpl | 12 ++++++------ Test/test21/Maps1.bpl | 12 ++++++------ Test/test21/Maps2.bpl | 12 ++++++------ Test/test21/NameClash.bpl | 12 ++++++------ Test/test21/Orderings.bpl | 12 ++++++------ Test/test21/Orderings2.bpl | 12 ++++++------ Test/test21/Orderings3.bpl | 12 ++++++------ Test/test21/Orderings4.bpl | 12 ++++++------ Test/test21/ParallelAssignment.bpl | 12 ++++++------ Test/test21/PolyList.bpl | 12 ++++++------ Test/test21/Real.bpl | 12 ++++++------ Test/test21/Triggers0.bpl | 12 ++++++------ Test/test21/Triggers1.bpl | 12 ++++++------ Test/test21/test3_AddMethod_conv.bpl | 12 ++++++------ 40 files changed, 240 insertions(+), 240 deletions(-) (limited to 'Test/test21') diff --git a/Test/test21/BooleanQuantification.bpl b/Test/test21/BooleanQuantification.bpl index 527ab174..1493269b 100644 --- a/Test/test21/BooleanQuantification.bpl +++ b/Test/test21/BooleanQuantification.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t -// RUN: %diff %s.n.expect %t -// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t -// RUN: %diff %s.p.expect %t -// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t -// RUN: %diff %s.a.expect %t +// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" +// RUN: %diff "%s.n.expect" "%t" +// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" +// RUN: %diff "%s.p.expect" "%t" +// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" +// RUN: %diff "%s.a.expect" "%t" diff --git a/Test/test21/BooleanQuantification2.bpl b/Test/test21/BooleanQuantification2.bpl index 73234024..22dfd217 100644 --- a/Test/test21/BooleanQuantification2.bpl +++ b/Test/test21/BooleanQuantification2.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t -// RUN: %diff %s.n.expect %t -// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t -// RUN: %diff %s.p.expect %t -// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t -// RUN: %diff %s.a.expect %t +// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" +// RUN: %diff "%s.n.expect" "%t" +// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" +// RUN: %diff "%s.p.expect" "%t" +// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" +// RUN: %diff "%s.a.expect" "%t" axiom (forall x:bool :: x || !x); diff --git a/Test/test21/Boxing.bpl b/Test/test21/Boxing.bpl index 00e3013e..0112b6cf 100644 --- a/Test/test21/Boxing.bpl +++ b/Test/test21/Boxing.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t -// RUN: %diff %s.n.expect %t -// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t -// RUN: %diff %s.p.expect %t -// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t -// RUN: %diff %s.a.expect %t +// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" +// RUN: %diff "%s.n.expect" "%t" +// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" +// RUN: %diff "%s.p.expect" "%t" +// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" +// RUN: %diff "%s.a.expect" "%t" type Box; diff --git a/Test/test21/Casts.bpl b/Test/test21/Casts.bpl index 1320cff2..739185ea 100644 --- a/Test/test21/Casts.bpl +++ b/Test/test21/Casts.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t -// RUN: %diff %s.n.expect %t -// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t -// RUN: %diff %s.p.expect %t -// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t -// RUN: %diff %s.a.expect %t +// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" +// RUN: %diff "%s.n.expect" "%t" +// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" +// RUN: %diff "%s.p.expect" "%t" +// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" +// RUN: %diff "%s.a.expect" "%t" procedure P() returns () { diff --git a/Test/test21/Coercions2.bpl b/Test/test21/Coercions2.bpl index 849376f5..e9a78574 100644 --- a/Test/test21/Coercions2.bpl +++ b/Test/test21/Coercions2.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t -// RUN: %diff %s.n.expect %t -// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t -// RUN: %diff %s.p.expect %t -// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t -// RUN: %diff %s.a.expect %t +// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" +// RUN: %diff "%s.n.expect" "%t" +// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" +// RUN: %diff "%s.p.expect" "%t" +// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" +// RUN: %diff "%s.a.expect" "%t" type Box, C; diff --git a/Test/test21/Colors.bpl b/Test/test21/Colors.bpl index 7e63c9ff..f0e12672 100644 --- a/Test/test21/Colors.bpl +++ b/Test/test21/Colors.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t -// RUN: %diff %s.n.expect %t -// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t -// RUN: %diff %s.p.expect %t -// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t -// RUN: %diff %s.a.expect %t +// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" +// RUN: %diff "%s.n.expect" "%t" +// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" +// RUN: %diff "%s.p.expect" "%t" +// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" +// RUN: %diff "%s.a.expect" "%t" type Color; diff --git a/Test/test21/DisjointDomains.bpl b/Test/test21/DisjointDomains.bpl index 303d0e4f..30d8a6f7 100644 --- a/Test/test21/DisjointDomains.bpl +++ b/Test/test21/DisjointDomains.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t -// RUN: %diff %s.n.expect %t -// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t -// RUN: %diff %s.p.expect %t -// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t -// RUN: %diff %s.a.expect %t +// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" +// RUN: %diff "%s.n.expect" "%t" +// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" +// RUN: %diff "%s.p.expect" "%t" +// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" +// RUN: %diff "%s.a.expect" "%t" type C _; function f(C a) returns (int); diff --git a/Test/test21/DisjointDomains2.bpl b/Test/test21/DisjointDomains2.bpl index 8677d9dc..ae25a20e 100644 --- a/Test/test21/DisjointDomains2.bpl +++ b/Test/test21/DisjointDomains2.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t -// RUN: %diff %s.n.expect %t -// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t -// RUN: %diff %s.p.expect %t -// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t -// RUN: %diff %s.a.expect %t +// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" +// RUN: %diff "%s.n.expect" "%t" +// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" +// RUN: %diff "%s.p.expect" "%t" +// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" +// RUN: %diff "%s.a.expect" "%t" type C _; function f(C a) returns (int); diff --git a/Test/test21/EmptyList.bpl b/Test/test21/EmptyList.bpl index 28362b73..450cd064 100644 --- a/Test/test21/EmptyList.bpl +++ b/Test/test21/EmptyList.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t -// RUN: %diff %s.n.expect %t -// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t -// RUN: %diff %s.p.expect %t -// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t -// RUN: %diff %s.a.expect %t +// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" +// RUN: %diff "%s.n.expect" "%t" +// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" +// RUN: %diff "%s.p.expect" "%t" +// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" +// RUN: %diff "%s.a.expect" "%t" type List _; diff --git a/Test/test21/EmptySetBug.bpl b/Test/test21/EmptySetBug.bpl index 06a42652..e3feb16c 100644 --- a/Test/test21/EmptySetBug.bpl +++ b/Test/test21/EmptySetBug.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t -// RUN: %diff %s.n.expect %t -// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t -// RUN: %diff %s.p.expect %t -// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t -// RUN: %diff %s.a.expect %t +// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" +// RUN: %diff "%s.n.expect" "%t" +// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" +// RUN: %diff "%s.p.expect" "%t" +// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" +// RUN: %diff "%s.a.expect" "%t" type ref; const null: ref; diff --git a/Test/test21/Flattening.bpl b/Test/test21/Flattening.bpl index 4ef7e5c8..ddebd9ab 100644 --- a/Test/test21/Flattening.bpl +++ b/Test/test21/Flattening.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t -// RUN: %diff %s.n.expect %t -// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t -// RUN: %diff %s.p.expect %t -// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t -// RUN: %diff %s.a.expect %t +// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" +// RUN: %diff "%s.n.expect" "%t" +// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" +// RUN: %diff "%s.p.expect" "%t" +// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" +// RUN: %diff "%s.a.expect" "%t" function g(int) returns (int); diff --git a/Test/test21/FunAxioms.bpl b/Test/test21/FunAxioms.bpl index c51024ad..5964b4e8 100644 --- a/Test/test21/FunAxioms.bpl +++ b/Test/test21/FunAxioms.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t -// RUN: %diff %s.n.expect %t -// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t -// RUN: %diff %s.p.expect %t -// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t -// RUN: %diff %s.a.expect %t +// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" +// RUN: %diff "%s.n.expect" "%t" +// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" +// RUN: %diff "%s.p.expect" "%t" +// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" +// RUN: %diff "%s.a.expect" "%t" type Pair a b; diff --git a/Test/test21/FunAxioms2.bpl b/Test/test21/FunAxioms2.bpl index 3b9bccf2..6e087baf 100644 --- a/Test/test21/FunAxioms2.bpl +++ b/Test/test21/FunAxioms2.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t -// RUN: %diff %s.n.expect %t -// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t -// RUN: %diff %s.p.expect %t -// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t -// RUN: %diff %s.a.expect %t +// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" +// RUN: %diff "%s.n.expect" "%t" +// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" +// RUN: %diff "%s.p.expect" "%t" +// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" +// RUN: %diff "%s.a.expect" "%t" type T; diff --git a/Test/test21/HeapAbstraction.bpl b/Test/test21/HeapAbstraction.bpl index 6f88189c..0fb2f007 100644 --- a/Test/test21/HeapAbstraction.bpl +++ b/Test/test21/HeapAbstraction.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t -// RUN: %diff %s.n.expect %t -// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t -// RUN: %diff %s.p.expect %t -// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t -// RUN: %diff %s.a.expect %t +// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" +// RUN: %diff "%s.n.expect" "%t" +// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" +// RUN: %diff "%s.p.expect" "%t" +// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" +// RUN: %diff "%s.a.expect" "%t" type Field a, Heap = [ref, Field a]a; diff --git a/Test/test21/HeapAxiom.bpl b/Test/test21/HeapAxiom.bpl index adb3f632..691c97f9 100644 --- a/Test/test21/HeapAxiom.bpl +++ b/Test/test21/HeapAxiom.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t -// RUN: %diff %s.n.expect %t -// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t -// RUN: %diff %s.p.expect %t -// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t -// RUN: %diff %s.a.expect %t +// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" +// RUN: %diff "%s.n.expect" "%t" +// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" +// RUN: %diff "%s.p.expect" "%t" +// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" +// RUN: %diff "%s.a.expect" "%t" type Field a, Heap = [ref, Field a]a; diff --git a/Test/test21/InterestingExamples0.bpl b/Test/test21/InterestingExamples0.bpl index d3021553..08ed61d4 100644 --- a/Test/test21/InterestingExamples0.bpl +++ b/Test/test21/InterestingExamples0.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t -// RUN: %diff %s.n.expect %t -// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t -// RUN: %diff %s.p.expect %t -// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t -// RUN: %diff %s.a.expect %t +// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" +// RUN: %diff "%s.n.expect" "%t" +// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" +// RUN: %diff "%s.p.expect" "%t" +// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" +// RUN: %diff "%s.a.expect" "%t" procedure P() returns () { var a : [t]int; diff --git a/Test/test21/InterestingExamples1.bpl b/Test/test21/InterestingExamples1.bpl index a530c625..247e2c5b 100644 --- a/Test/test21/InterestingExamples1.bpl +++ b/Test/test21/InterestingExamples1.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t -// RUN: %diff %s.n.expect %t -// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t -// RUN: %diff %s.p.expect %t -// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t -// RUN: %diff %s.a.expect %t +// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" +// RUN: %diff "%s.n.expect" "%t" +// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" +// RUN: %diff "%s.p.expect" "%t" +// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" +// RUN: %diff "%s.a.expect" "%t" type Set = [a] bool; type Field a; diff --git a/Test/test21/InterestingExamples2.bpl b/Test/test21/InterestingExamples2.bpl index fd17b122..6fc8d259 100644 --- a/Test/test21/InterestingExamples2.bpl +++ b/Test/test21/InterestingExamples2.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t -// RUN: %diff %s.n.expect %t -// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t -// RUN: %diff %s.p.expect %t -// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t -// RUN: %diff %s.a.expect %t +// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" +// RUN: %diff "%s.n.expect" "%t" +// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" +// RUN: %diff "%s.p.expect" "%t" +// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" +// RUN: %diff "%s.a.expect" "%t" procedure P() returns () { diff --git a/Test/test21/InterestingExamples3.bpl b/Test/test21/InterestingExamples3.bpl index 3acca9a1..24e89b2b 100644 --- a/Test/test21/InterestingExamples3.bpl +++ b/Test/test21/InterestingExamples3.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t -// RUN: %diff %s.n.expect %t -// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t -// RUN: %diff %s.p.expect %t -// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t -// RUN: %diff %s.a.expect %t +// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" +// RUN: %diff "%s.n.expect" "%t" +// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" +// RUN: %diff "%s.p.expect" "%t" +// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" +// RUN: %diff "%s.a.expect" "%t" procedure P() returns () { diff --git a/Test/test21/InterestingExamples4.bpl b/Test/test21/InterestingExamples4.bpl index db2e9682..941c9020 100644 --- a/Test/test21/InterestingExamples4.bpl +++ b/Test/test21/InterestingExamples4.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t -// RUN: %diff %s.n.expect %t -// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t -// RUN: %diff %s.p.expect %t -// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t -// RUN: %diff %s.a.expect %t +// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" +// RUN: %diff "%s.n.expect" "%t" +// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" +// RUN: %diff "%s.p.expect" "%t" +// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" +// RUN: %diff "%s.a.expect" "%t" // a property that should hold according to the Boogie semantics // (but no automatic theorem prover will be able to prove it) diff --git a/Test/test21/InterestingExamples5.bpl b/Test/test21/InterestingExamples5.bpl index be388839..3f4e4f34 100644 --- a/Test/test21/InterestingExamples5.bpl +++ b/Test/test21/InterestingExamples5.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t -// RUN: %diff %s.n.expect %t -// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t -// RUN: %diff %s.p.expect %t -// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t -// RUN: %diff %s.a.expect %t +// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" +// RUN: %diff "%s.n.expect" "%t" +// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" +// RUN: %diff "%s.p.expect" "%t" +// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" +// RUN: %diff "%s.a.expect" "%t" type C a; diff --git a/Test/test21/Keywords.bpl b/Test/test21/Keywords.bpl index 9af526e4..3be91fa8 100644 --- a/Test/test21/Keywords.bpl +++ b/Test/test21/Keywords.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t -// RUN: %diff %s.n.expect %t -// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t -// RUN: %diff %s.p.expect %t -// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t -// RUN: %diff %s.a.expect %t +// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" +// RUN: %diff "%s.n.expect" "%t" +// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" +// RUN: %diff "%s.p.expect" "%t" +// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" +// RUN: %diff "%s.a.expect" "%t" function NOT(x:int) returns(int); diff --git a/Test/test21/LargeLiterals0.bpl b/Test/test21/LargeLiterals0.bpl index 203e9bc5..57877f9d 100644 --- a/Test/test21/LargeLiterals0.bpl +++ b/Test/test21/LargeLiterals0.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t -// RUN: %diff %s.n.expect %t -// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t -// RUN: %diff %s.p.expect %t -// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t -// RUN: %diff %s.a.expect %t +// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" +// RUN: %diff "%s.n.expect" "%t" +// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" +// RUN: %diff "%s.p.expect" "%t" +// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" +// RUN: %diff "%s.a.expect" "%t" var x : int; diff --git a/Test/test21/LetSorting.bpl b/Test/test21/LetSorting.bpl index 38e77396..c58c6242 100644 --- a/Test/test21/LetSorting.bpl +++ b/Test/test21/LetSorting.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t -// RUN: %diff %s.n.expect %t -// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t -// RUN: %diff %s.p.expect %t -// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t -// RUN: %diff %s.a.expect %t +// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" +// RUN: %diff "%s.n.expect" "%t" +// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" +// RUN: %diff "%s.p.expect" "%t" +// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" +// RUN: %diff "%s.a.expect" "%t" procedure Array0() returns (z: int) diff --git a/Test/test21/MapAxiomsConsistency.bpl b/Test/test21/MapAxiomsConsistency.bpl index 66e7a142..4c8302a4 100644 --- a/Test/test21/MapAxiomsConsistency.bpl +++ b/Test/test21/MapAxiomsConsistency.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t -// RUN: %diff %s.n.expect %t -// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t -// RUN: %diff %s.p.expect %t -// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t -// RUN: %diff %s.a.expect %t +// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" +// RUN: %diff "%s.n.expect" "%t" +// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" +// RUN: %diff "%s.p.expect" "%t" +// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" +// RUN: %diff "%s.a.expect" "%t" // Dafny program verifier version 0.92, Copyright (c) 2003-2008, Microsoft. // Command Line Options: /trace /typeEncoding:arguments /print:test.bpl test.dfy diff --git a/Test/test21/MapOutputTypeParams.bpl b/Test/test21/MapOutputTypeParams.bpl index 4e83e6f1..c9304d34 100644 --- a/Test/test21/MapOutputTypeParams.bpl +++ b/Test/test21/MapOutputTypeParams.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t -// RUN: %diff %s.n.expect %t -// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t -// RUN: %diff %s.p.expect %t -// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t -// RUN: %diff %s.a.expect %t +// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" +// RUN: %diff "%s.n.expect" "%t" +// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" +// RUN: %diff "%s.p.expect" "%t" +// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" +// RUN: %diff "%s.a.expect" "%t" diff --git a/Test/test21/Maps0.bpl b/Test/test21/Maps0.bpl index ba3a0f98..125730ef 100644 --- a/Test/test21/Maps0.bpl +++ b/Test/test21/Maps0.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t -// RUN: %diff %s.n.expect %t -// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t -// RUN: %diff %s.p.expect %t -// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t -// RUN: %diff %s.a.expect %t +// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" +// RUN: %diff "%s.n.expect" "%t" +// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" +// RUN: %diff "%s.p.expect" "%t" +// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" +// RUN: %diff "%s.a.expect" "%t" const a : [int] bool; diff --git a/Test/test21/Maps1.bpl b/Test/test21/Maps1.bpl index 417521eb..024cd50f 100644 --- a/Test/test21/Maps1.bpl +++ b/Test/test21/Maps1.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t -// RUN: %diff %s.n.expect %t -// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t -// RUN: %diff %s.p.expect %t -// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t -// RUN: %diff %s.a.expect %t +// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" +// RUN: %diff "%s.n.expect" "%t" +// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" +// RUN: %diff "%s.p.expect" "%t" +// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" +// RUN: %diff "%s.a.expect" "%t" // different map type classes with the same arity diff --git a/Test/test21/Maps2.bpl b/Test/test21/Maps2.bpl index ea020afd..0b7980c7 100644 --- a/Test/test21/Maps2.bpl +++ b/Test/test21/Maps2.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t -// RUN: %diff %s.n.expect %t -// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t -// RUN: %diff %s.p.expect %t -// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t -// RUN: %diff %s.a.expect %t +// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" +// RUN: %diff "%s.n.expect" "%t" +// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" +// RUN: %diff "%s.p.expect" "%t" +// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" +// RUN: %diff "%s.a.expect" "%t" // XFAIL: * type T; diff --git a/Test/test21/NameClash.bpl b/Test/test21/NameClash.bpl index 9b6fefa8..d31a6e01 100644 --- a/Test/test21/NameClash.bpl +++ b/Test/test21/NameClash.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t -// RUN: %diff %s.n.expect %t -// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t -// RUN: %diff %s.p.expect %t -// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t -// RUN: %diff %s.a.expect %t +// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" +// RUN: %diff "%s.n.expect" "%t" +// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" +// RUN: %diff "%s.p.expect" "%t" +// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" +// RUN: %diff "%s.a.expect" "%t" function f(int) returns (int); diff --git a/Test/test21/Orderings.bpl b/Test/test21/Orderings.bpl index 6a048224..39361461 100644 --- a/Test/test21/Orderings.bpl +++ b/Test/test21/Orderings.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t -// RUN: %diff %s.n.expect %t -// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t -// RUN: %diff %s.p.expect %t -// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t -// RUN: %diff %s.a.expect %t +// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" +// RUN: %diff "%s.n.expect" "%t" +// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" +// RUN: %diff "%s.p.expect" "%t" +// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" +// RUN: %diff "%s.a.expect" "%t" const a, b:int; diff --git a/Test/test21/Orderings2.bpl b/Test/test21/Orderings2.bpl index fe01184c..01d3be15 100644 --- a/Test/test21/Orderings2.bpl +++ b/Test/test21/Orderings2.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t -// RUN: %diff %s.n.expect %t -// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t -// RUN: %diff %s.p.expect %t -// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t -// RUN: %diff %s.a.expect %t +// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" +// RUN: %diff "%s.n.expect" "%t" +// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" +// RUN: %diff "%s.p.expect" "%t" +// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" +// RUN: %diff "%s.a.expect" "%t" const b:int; diff --git a/Test/test21/Orderings3.bpl b/Test/test21/Orderings3.bpl index a842be12..3036d8e6 100644 --- a/Test/test21/Orderings3.bpl +++ b/Test/test21/Orderings3.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t -// RUN: %diff %s.n.expect %t -// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t -// RUN: %diff %s.p.expect %t -// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t -// RUN: %diff %s.a.expect %t +// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" +// RUN: %diff "%s.n.expect" "%t" +// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" +// RUN: %diff "%s.p.expect" "%t" +// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" +// RUN: %diff "%s.a.expect" "%t" // Example from the Boogie 2 language report diff --git a/Test/test21/Orderings4.bpl b/Test/test21/Orderings4.bpl index 62f7b7fa..00da92dc 100644 --- a/Test/test21/Orderings4.bpl +++ b/Test/test21/Orderings4.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t -// RUN: %diff %s.n.expect %t -// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t -// RUN: %diff %s.p.expect %t -// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t -// RUN: %diff %s.a.expect %t +// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" +// RUN: %diff "%s.n.expect" "%t" +// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" +// RUN: %diff "%s.p.expect" "%t" +// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" +// RUN: %diff "%s.a.expect" "%t" type Wicket; diff --git a/Test/test21/ParallelAssignment.bpl b/Test/test21/ParallelAssignment.bpl index 6bd414e9..6f7c7639 100644 --- a/Test/test21/ParallelAssignment.bpl +++ b/Test/test21/ParallelAssignment.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t -// RUN: %diff %s.n.expect %t -// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t -// RUN: %diff %s.p.expect %t -// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t -// RUN: %diff %s.a.expect %t +// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" +// RUN: %diff "%s.n.expect" "%t" +// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" +// RUN: %diff "%s.p.expect" "%t" +// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" +// RUN: %diff "%s.a.expect" "%t" // Examples from the Boogie2 language report type C, D; diff --git a/Test/test21/PolyList.bpl b/Test/test21/PolyList.bpl index c68c637e..08fcd637 100644 --- a/Test/test21/PolyList.bpl +++ b/Test/test21/PolyList.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t -// RUN: %diff %s.n.expect %t -// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t -// RUN: %diff %s.p.expect %t -// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t -// RUN: %diff %s.a.expect %t +// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" +// RUN: %diff "%s.n.expect" "%t" +// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" +// RUN: %diff "%s.p.expect" "%t" +// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" +// RUN: %diff "%s.a.expect" "%t" diff --git a/Test/test21/Real.bpl b/Test/test21/Real.bpl index 42b1f889..eb140f77 100644 --- a/Test/test21/Real.bpl +++ b/Test/test21/Real.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t -// RUN: %diff %s.n.expect %t -// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t -// RUN: %diff %s.p.expect %t -// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t -// RUN: %diff %s.a.expect %t +// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" +// RUN: %diff "%s.n.expect" "%t" +// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" +// RUN: %diff "%s.p.expect" "%t" +// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" +// RUN: %diff "%s.a.expect" "%t" axiom (forall r: real :: r == 0.0 || r / r == 1.0); procedure P(a: real, b: real) returns () { diff --git a/Test/test21/Triggers0.bpl b/Test/test21/Triggers0.bpl index f58b168f..c3ff14d5 100644 --- a/Test/test21/Triggers0.bpl +++ b/Test/test21/Triggers0.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t -// RUN: %diff %s.n.expect %t -// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t -// RUN: %diff %s.p.expect %t -// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t -// RUN: %diff %s.a.expect %t +// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" +// RUN: %diff "%s.n.expect" "%t" +// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" +// RUN: %diff "%s.p.expect" "%t" +// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" +// RUN: %diff "%s.a.expect" "%t" const ar : [int]bool; diff --git a/Test/test21/Triggers1.bpl b/Test/test21/Triggers1.bpl index 63a780f5..a4199040 100644 --- a/Test/test21/Triggers1.bpl +++ b/Test/test21/Triggers1.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t -// RUN: %diff %s.n.expect %t -// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t -// RUN: %diff %s.p.expect %t -// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t -// RUN: %diff %s.a.expect %t +// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" +// RUN: %diff "%s.n.expect" "%t" +// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" +// RUN: %diff "%s.p.expect" "%t" +// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" +// RUN: %diff "%s.a.expect" "%t" diff --git a/Test/test21/test3_AddMethod_conv.bpl b/Test/test21/test3_AddMethod_conv.bpl index d0abb5c3..89c34c45 100644 --- a/Test/test21/test3_AddMethod_conv.bpl +++ b/Test/test21/test3_AddMethod_conv.bpl @@ -1,9 +1,9 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n %s > %t -// RUN: %diff %s.n.expect %t -// RUN: %boogie -typeEncoding:p -logPrefix:0p %s > %t -// RUN: %diff %s.p.expect %t -// RUN: %boogie -typeEncoding:a -logPrefix:0a %s > %t -// RUN: %diff %s.a.expect %t +// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" +// RUN: %diff "%s.n.expect" "%t" +// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" +// RUN: %diff "%s.p.expect" "%t" +// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" +// RUN: %diff "%s.a.expect" "%t" // XFAIL: * // Spec# program verifier version 0.90, Copyright (c) 2003-2008, Microsoft. // Command Line Options: /print:debug.txt AddMethod.dll -- cgit v1.2.3