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

diff --git a/Test/AbsHoudini/test9.bpl b/Test/AbsHoudini/test9.bpl
index 7d624167..9e7778eb 100644
--- a/Test/AbsHoudini/test9.bpl
+++ b/Test/AbsHoudini/test9.bpl
@@ -1,92 +1,92 @@
-// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] "%s" > "%t"

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

-var v1: int;

-var v2: int;

-var v3: int;

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

-

-procedure push() 

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

-requires {:candidate} b2() || v1 == 1;

-ensures  {:candidate} b3() || v1 == 0;

-ensures {:candidate}  b4() || v1 == 1;

-modifies v1,v2;

-{

-   v2 := v1;

-   v1 := 1;

-}

-

-procedure pop()

-modifies v1,v2;

-requires {:candidate} b5() || v1 == 0;

-requires {:candidate} b6() || v1 == 1;

-ensures  {:candidate} b7() || v1 == 0;

-ensures {:candidate}  b8() || v1 == 1;

-{

-   v1 := v2;

-   havoc v2;

-}

-

-procedure foo() 

-modifies v1,v2;

-requires {:candidate} b9() || v1 == 0;

-requires {:candidate} b10() || v1 == 1;

-ensures  {:candidate} b11() || v1 == 0;

-ensures {:candidate}  b12() || v1 == 1;

-{

-   call push();

-   call pop();

-}

-

-procedure bar()

-modifies v1,v2;

-requires {:candidate} b13() || v1 == 0;

-requires {:candidate} b14() || v1 == 1;

-ensures  {:candidate} b15() || v1 == 0;

-ensures {:candidate}  b16() || v1 == 1;

-{

-   call push();

-   call pop();

-}

-

-procedure main() 

-modifies v1,v2;

-{

-   v1 := 1;

-   call foo();

-   havoc v1;

-   call bar();

-}

-

-// Expected:

-//b1 = true

-//b2 = true

-//b3 = true

-//b4 = false

-//b5 = true

-//b6 = false

-//b7 = true

-//b8 = true

-//b9 = true

-//b10 = false

-//b11 = true

-//b12 = false

-//b13 = true

-//b14 = true

-//b15 = true

-//b16 = true

+// RUN: %boogie -noinfer -contractInfer -printAssignment -inlineDepth:1 -abstractHoudini:IA[ConstantProp] "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+var v1: int;
+var v2: int;
+var v3: int;
+function{:existential true} b1(): bool;
+function{:existential true} b2(): bool;
+function{:existential true} b3(): bool;
+function{:existential true} b4(): bool;
+function{:existential true} b5(): bool;
+function{:existential true} b6(): bool;
+function{:existential true} b7(): bool;
+function{:existential true} b8(): bool;
+function{:existential true} b9(): bool;
+function{:existential true} b10(): bool;
+function{:existential true} b11(): bool;
+function{:existential true} b12(): bool;
+function{:existential true} b13(): bool;
+function{:existential true} b14(): bool;
+function{:existential true} b15(): bool;
+function{:existential true} b16(): bool;
+
+procedure push() 
+requires {:candidate} b1() || v1 == 0;
+requires {:candidate} b2() || v1 == 1;
+ensures  {:candidate} b3() || v1 == 0;
+ensures {:candidate}  b4() || v1 == 1;
+modifies v1,v2;
+{
+   v2 := v1;
+   v1 := 1;
+}
+
+procedure pop()
+modifies v1,v2;
+requires {:candidate} b5() || v1 == 0;
+requires {:candidate} b6() || v1 == 1;
+ensures  {:candidate} b7() || v1 == 0;
+ensures {:candidate}  b8() || v1 == 1;
+{
+   v1 := v2;
+   havoc v2;
+}
+
+procedure foo() 
+modifies v1,v2;
+requires {:candidate} b9() || v1 == 0;
+requires {:candidate} b10() || v1 == 1;
+ensures  {:candidate} b11() || v1 == 0;
+ensures {:candidate}  b12() || v1 == 1;
+{
+   call push();
+   call pop();
+}
+
+procedure bar()
+modifies v1,v2;
+requires {:candidate} b13() || v1 == 0;
+requires {:candidate} b14() || v1 == 1;
+ensures  {:candidate} b15() || v1 == 0;
+ensures {:candidate}  b16() || v1 == 1;
+{
+   call push();
+   call pop();
+}
+
+procedure main() 
+modifies v1,v2;
+{
+   v1 := 1;
+   call foo();
+   havoc v1;
+   call bar();
+}
+
+// Expected:
+//b1 = true
+//b2 = true
+//b3 = true
+//b4 = false
+//b5 = true
+//b6 = false
+//b7 = true
+//b8 = true
+//b9 = true
+//b10 = false
+//b11 = true
+//b12 = false
+//b13 = true
+//b14 = true
+//b15 = true
+//b16 = true