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.

3 files changed, 63 insertions, 63 deletions

diff --git a/Test/datatypes/ex.bpl b/Test/datatypes/ex.bpl
index e7a0e694..753d8801 100644
--- a/Test/datatypes/ex.bpl
+++ b/Test/datatypes/ex.bpl
@@ -1,13 +1,13 @@
-// RUN: %boogie -typeEncoding:m "%s" > "%t"

-// RUN: %diff "%s.expect" "%t"

-type{:datatype} finite_map;

-function{:constructor} finite_map(dom:[int]bool, map:[int]int):finite_map;

-

-type{:datatype} partition;

-function{:constructor} partition(owners:[int]int, vars:[int]finite_map):partition;

-

-procedure P(arr:finite_map)

-  requires dom#finite_map(arr)[0];

-  ensures  dom#finite_map(arr)[0];

-{

-}

+// RUN: %boogie -typeEncoding:m "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+type{:datatype} finite_map;
+function{:constructor} finite_map(dom:[int]bool, map:[int]int):finite_map;
+
+type{:datatype} partition;
+function{:constructor} partition(owners:[int]int, vars:[int]finite_map):partition;
+
+procedure P(arr:finite_map)
+  requires dom#finite_map(arr)[0];
+  ensures  dom#finite_map(arr)[0];
+{
+}
diff --git a/Test/datatypes/t1.bpl b/Test/datatypes/t1.bpl
index f0488639..876d879d 100644
--- a/Test/datatypes/t1.bpl
+++ b/Test/datatypes/t1.bpl
@@ -1,26 +1,26 @@
-// RUN: %boogie -typeEncoding:m "%s" > "%t"

-// RUN: %diff "%s.expect" "%t"

-type TT;

-type {:datatype} Tree;

-function {:constructor} leaf() : Tree;

-function {:constructor} node(value:TT, children:TreeList) : Tree;

-

-type {:datatype} TreeList;

-function {:constructor} cons(car:Tree, cdr:TreeList) : TreeList;

-function {:constructor} nil() : TreeList;

-

-procedure foo() 

-{

-  var a: Tree;

-  var b: TreeList;

-  var x: TT;

-

-  assert value#node(node(x, nil())) == x;

-  assert children#node(node(x, nil())) == nil();

-  

-  assert (cons(leaf(), nil()) != nil());

-

-  assert is#nil(nil());

-

-  assert is#node(leaf());

+// RUN: %boogie -typeEncoding:m "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+type TT;
+type {:datatype} Tree;
+function {:constructor} leaf() : Tree;
+function {:constructor} node(value:TT, children:TreeList) : Tree;
+
+type {:datatype} TreeList;
+function {:constructor} cons(car:Tree, cdr:TreeList) : TreeList;
+function {:constructor} nil() : TreeList;
+
+procedure foo() 
+{
+  var a: Tree;
+  var b: TreeList;
+  var x: TT;
+
+  assert value#node(node(x, nil())) == x;
+  assert children#node(node(x, nil())) == nil();
+  
+  assert (cons(leaf(), nil()) != nil());
+
+  assert is#nil(nil());
+
+  assert is#node(leaf());
 }
\ No newline at end of file
diff --git a/Test/datatypes/t2.bpl b/Test/datatypes/t2.bpl
index 106b8d0c..257fff9c 100644
--- a/Test/datatypes/t2.bpl
+++ b/Test/datatypes/t2.bpl
@@ -1,26 +1,26 @@
-// RUN: %boogie -typeEncoding:m "%s" > "%t"

-// RUN: %diff "%s.expect" "%t"

-type TT;

-type {:datatype} Tree;

-function {:constructor} leaf`0() : Tree;

-function {:constructor} node`2(value:TT, children:TreeList) : Tree;

-

-type {:datatype} TreeList;

-function {:constructor} cons`2(car:Tree, cdr:TreeList) : TreeList;

-function {:constructor} nil`0() : TreeList;

-

-procedure foo() 

-{

-  var a: Tree;

-  var b: TreeList;

-  var x: TT;

-

-  assert value#node`2(node`2(x, nil`0())) == x;

-  assert children#node`2(node`2(x, nil`0())) == nil`0();

-  

-  assert (cons`2(leaf`0(), nil`0()) != nil`0());

-

-  assert is#nil`0(nil`0());

-

-  assert is#node`2(leaf`0());

+// RUN: %boogie -typeEncoding:m "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+type TT;
+type {:datatype} Tree;
+function {:constructor} leaf`0() : Tree;
+function {:constructor} node`2(value:TT, children:TreeList) : Tree;
+
+type {:datatype} TreeList;
+function {:constructor} cons`2(car:Tree, cdr:TreeList) : TreeList;
+function {:constructor} nil`0() : TreeList;
+
+procedure foo() 
+{
+  var a: Tree;
+  var b: TreeList;
+  var x: TT;
+
+  assert value#node`2(node`2(x, nil`0())) == x;
+  assert children#node`2(node`2(x, nil`0())) == nil`0();
+  
+  assert (cons`2(leaf`0(), nil`0()) != nil`0());
+
+  assert is#nil`0(nil`0());
+
+  assert is#node`2(leaf`0());
 }
\ No newline at end of file