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.

1 files changed, 45 insertions, 45 deletions

diff --git a/Test/test21/FunAxioms.bpl b/Test/test21/FunAxioms.bpl
index 5964b4e8..2baa2169 100644
--- a/Test/test21/FunAxioms.bpl
+++ b/Test/test21/FunAxioms.bpl
@@ -1,46 +1,46 @@
-// 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;

-

-function MP<a,b>(x:a, y:b) returns (Pair a b);

-function Left<a,b>(Pair a b) returns (a);

-function Right<a,b>(Pair a b) returns (b);

-

-axiom (forall<a,b> x:a, y:b :: Left(MP(x,y)) == x);

-axiom (forall<a,b> x:a, y:b :: Right(MP(x,y)) == y);

-

-type A, B;

-

-procedure P() returns () {

-

-  var x:A, y:B, z:A, p : Pair A B;

-

-  assert Left(MP(x,y)) == x;

-  assert Right(MP(x,y)) == y;

-  assert Right(MP(x,MP(x,y))) == MP(x,y);

-  assert Left(MP(x,MP(x,y))) == x;

-  assert Right(Right(MP(x,MP(x,y)))) == y;

-

-  p := MP(x, y);

-

-  p := MP(Left(p), y);

-

-  assert Left(p) == x && Right(p) == y;

-

-  assert Left(p) == z;            // should not be provable

-

-}

-

-procedure Q() returns () {

-

-  assert Left(MP(1,3)) == 1;

-  assert Right(MP(1,3)) == 3;

-  assert Right(MP(1,true)) == true;

-

+// 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;
+
+function MP<a,b>(x:a, y:b) returns (Pair a b);
+function Left<a,b>(Pair a b) returns (a);
+function Right<a,b>(Pair a b) returns (b);
+
+axiom (forall<a,b> x:a, y:b :: Left(MP(x,y)) == x);
+axiom (forall<a,b> x:a, y:b :: Right(MP(x,y)) == y);
+
+type A, B;
+
+procedure P() returns () {
+
+  var x:A, y:B, z:A, p : Pair A B;
+
+  assert Left(MP(x,y)) == x;
+  assert Right(MP(x,y)) == y;
+  assert Right(MP(x,MP(x,y))) == MP(x,y);
+  assert Left(MP(x,MP(x,y))) == x;
+  assert Right(Right(MP(x,MP(x,y)))) == y;
+
+  p := MP(x, y);
+
+  p := MP(Left(p), y);
+
+  assert Left(p) == x && Right(p) == y;
+
+  assert Left(p) == z;            // should not be provable
+
+}
+
+procedure Q() returns () {
+
+  assert Left(MP(1,3)) == 1;
+  assert Right(MP(1,3)) == 3;
+  assert Right(MP(1,true)) == true;
+
 }
\ No newline at end of file