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

diff --git a/Test/AbsHoudini/test10.bpl b/Test/AbsHoudini/test10.bpl
index cb2fe89a..4acc862d 100644
--- a/Test/AbsHoudini/test10.bpl
+++ b/Test/AbsHoudini/test10.bpl
@@ -1,52 +1,52 @@
-// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] "%s" > "%t"

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

-var sdv_7: int;

-var sdv_21: int;

-function {:existential true} b1(): bool;

-function{:existential true}  b2(): bool;

-function{:existential true}  b3(): bool;

-function{:existential true}  b4(): bool;

-

-procedure push(a:int)

-modifies sdv_7, sdv_21;

-{

-   sdv_21 := sdv_7;

-   sdv_7 := a;

-}

-

-procedure pop()

-modifies sdv_7, sdv_21;

-{

-   sdv_7 := sdv_21;

-   havoc sdv_21;

-}

-

-procedure foo()

-modifies sdv_7, sdv_21;

-requires {:candidate} b1() || (sdv_7 == 0);

-ensures{:candidate}  b2() || (sdv_7 == old(sdv_7));

-{

-   call push(2);

-   call pop();

-   call bar();

-}

-

-procedure bar()

-requires{:candidate} b3() || (sdv_7 == 0);

-ensures{:candidate}  b4() || (sdv_7 == old(sdv_7));

-modifies sdv_7, sdv_21;

-{

-   call push(1);

-   call pop();

-}

-

-procedure main()

-modifies sdv_7, sdv_21;

-{

-   sdv_7 := 0;

-   call foo();

-}

-

-// Expected: All false

-

-

+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+var sdv_7: int;
+var sdv_21: int;
+function {:existential true} b1(): bool;
+function{:existential true}  b2(): bool;
+function{:existential true}  b3(): bool;
+function{:existential true}  b4(): bool;
+
+procedure push(a:int)
+modifies sdv_7, sdv_21;
+{
+   sdv_21 := sdv_7;
+   sdv_7 := a;
+}
+
+procedure pop()
+modifies sdv_7, sdv_21;
+{
+   sdv_7 := sdv_21;
+   havoc sdv_21;
+}
+
+procedure foo()
+modifies sdv_7, sdv_21;
+requires {:candidate} b1() || (sdv_7 == 0);
+ensures{:candidate}  b2() || (sdv_7 == old(sdv_7));
+{
+   call push(2);
+   call pop();
+   call bar();
+}
+
+procedure bar()
+requires{:candidate} b3() || (sdv_7 == 0);
+ensures{:candidate}  b4() || (sdv_7 == old(sdv_7));
+modifies sdv_7, sdv_21;
+{
+   call push(1);
+   call pop();
+}
+
+procedure main()
+modifies sdv_7, sdv_21;
+{
+   sdv_7 := 0;
+   call foo();
+}
+
+// Expected: All false
+
+