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, 99 insertions, 99 deletions

diff --git a/Test/test1/Frame1.bpl b/Test/test1/Frame1.bpl
index 2ec70270..5e637660 100644
--- a/Test/test1/Frame1.bpl
+++ b/Test/test1/Frame1.bpl
@@ -1,99 +1,99 @@
-// RUN: %boogie -noVerify "%s" > "%t"

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

-var g0: int;

-var g1: int;

-

-var h0: [ref, name]int;

-var h1: [ref, name]int;

-

-const X: name;

-

-procedure P(a: ref, hh: [ref, name]int) returns (b: int, hout: [ref, name]any);

-  modifies h1, g0;

-

-implementation P(a: ref, hh: [ref, name]int)

-               returns (b: int, hout: [ref, name]any) {

-  start:

-    g0 := 5;

-    g1 := 6;  // error: g1 is not in modifies clause

-    a := null;  // error: in-parameters are not mutable 

-    b := 12;

-    goto next;

-  next:

-    havoc g0;

-    havoc g1;  // error: g1 is not in modifies clause

-    havoc a;  // error: in-parameters are not mutable

-    havoc b;

-    goto more;

-  more:

-    hh[a,X] := 101;  // error: in-parameter (hh) is not mutable

-    h0[a,X] := 102;  // error: h0 is not in modifies clause

-    h1[a,X] := 103;

-    hh := h0;  // error: in-parameter is not mutable

-    h0 := h1;  // error: h0 is not in modifies clause

-    h1 := hh;

-    havoc hh;  // error: in-parameter is not mutable

-    havoc h0;  // error: h0 is not in modifies clause

-    havoc h1;

-    return;

-}

-

-procedure PX();

-  modifies h1, g0;

-

-procedure PY()

-  modifies h1, g0;

-{

-  start:

-    call PX();

-    call PY();

-    return;

-}

-

-procedure PZ()

-  modifies h1;

-{

-  start:

-    call PX();  // error: PX has larger frame than PZ

-    return;

-}

-

-procedure Q() returns (x: int, y: int, h: [ref, name]int)

-{

-  start:

-    return;

-}

-

-procedure QCallerBad()

-{

-  start:

-    call g0, g1, h0 := Q();

-    return;

-}

-

-procedure QCallerGood()

-  modifies g0, h0;

-{

-  var t: int;

-

-  start:

-    call t, g0, h0 := Q();

-    return;

-}

-

-procedure MismatchedTypes(x: int);

-

-implementation MismatchedTypes(x: bool)  // error

-{

-  start:

-    return;

-}

-implementation MismatchedTypes(y: bool)  // error (this time with a different name for the formal)

-{

-  start:

-    return;

-}

-

-

-type ref, name, any;

-const null : ref;

+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+var g0: int;
+var g1: int;
+
+var h0: [ref, name]int;
+var h1: [ref, name]int;
+
+const X: name;
+
+procedure P(a: ref, hh: [ref, name]int) returns (b: int, hout: [ref, name]any);
+  modifies h1, g0;
+
+implementation P(a: ref, hh: [ref, name]int)
+               returns (b: int, hout: [ref, name]any) {
+  start:
+    g0 := 5;
+    g1 := 6;  // error: g1 is not in modifies clause
+    a := null;  // error: in-parameters are not mutable 
+    b := 12;
+    goto next;
+  next:
+    havoc g0;
+    havoc g1;  // error: g1 is not in modifies clause
+    havoc a;  // error: in-parameters are not mutable
+    havoc b;
+    goto more;
+  more:
+    hh[a,X] := 101;  // error: in-parameter (hh) is not mutable
+    h0[a,X] := 102;  // error: h0 is not in modifies clause
+    h1[a,X] := 103;
+    hh := h0;  // error: in-parameter is not mutable
+    h0 := h1;  // error: h0 is not in modifies clause
+    h1 := hh;
+    havoc hh;  // error: in-parameter is not mutable
+    havoc h0;  // error: h0 is not in modifies clause
+    havoc h1;
+    return;
+}
+
+procedure PX();
+  modifies h1, g0;
+
+procedure PY()
+  modifies h1, g0;
+{
+  start:
+    call PX();
+    call PY();
+    return;
+}
+
+procedure PZ()
+  modifies h1;
+{
+  start:
+    call PX();  // error: PX has larger frame than PZ
+    return;
+}
+
+procedure Q() returns (x: int, y: int, h: [ref, name]int)
+{
+  start:
+    return;
+}
+
+procedure QCallerBad()
+{
+  start:
+    call g0, g1, h0 := Q();
+    return;
+}
+
+procedure QCallerGood()
+  modifies g0, h0;
+{
+  var t: int;
+
+  start:
+    call t, g0, h0 := Q();
+    return;
+}
+
+procedure MismatchedTypes(x: int);
+
+implementation MismatchedTypes(x: bool)  // error
+{
+  start:
+    return;
+}
+implementation MismatchedTypes(y: bool)  // error (this time with a different name for the formal)
+{
+  start:
+    return;
+}
+
+
+type ref, name, any;
+const null : ref;