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.

2 files changed, 405 insertions, 405 deletions

diff --git a/Test/aitest0/Intervals.bpl b/Test/aitest0/Intervals.bpl
index 565b6823..fddce05a 100644
--- a/Test/aitest0/Intervals.bpl
+++ b/Test/aitest0/Intervals.bpl
@@ -1,334 +1,334 @@
-// RUN: %boogie -infer:j "%s" > "%t"

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

-const N: int;

-axiom 0 <= N;

-

-procedure P(K: int)

-  requires 0 <= K;

-{

-  var b: bool, x, k: int;

-

-  if (!b) {

-    b := !b;

-  }

-  x := if b then 13 else 10;

-  k := K;

-  while (k != 0) {

-    x := x + k;

-    k := k - 1;

-  }

-  assert 13 <= x;

-}

-

-procedure Thresholds0()

-{

-  var i: int;

-  i := 0;

-  while (i < 200)

-  {

-    i := i + 1;

-  }

-  assert i == 200;

-}

-

-procedure Thresholds1()

-{

-  var i: int;

-  i := 0;

-  while (i <= 199)

-  {

-    i := i + 1;

-  }

-  assert i == 200;

-}

-

-procedure Thresholds2()

-{

-  var i: int;

-  i := 100;

-  while (0 < i)

-  {

-    i := i - 1;

-  }

-  assert i == 0;

-}

-

-procedure Thresholds3()

-{

-  var i: int;

-  i := 0;

-  while (i < 200)

-  {

-    i := i + 1;

-  }

-  assert i == 199;  // error

-}

-

-procedure Thresholds4()

-{

-  var i: int;

-  i := 0;

-  while (i + 3 < 203)

-  {

-    i := i + 1;

-  }

-  assert i * 2 == 400;  // error: this would hold in an execution, but /infer:j is too weak to infer invariant i<=200

-}

-

-procedure UnaryNegation0() returns (x: int)  // this was once buggy

-{

-  x := -1;

-  loop_head:

-    x := x;

-    goto loop_head, after_loop;

-  after_loop:

-  assert x == -1;

-}

-procedure UnaryNegation1() returns (x: int)  // this was once buggy

-{

-  x := -1;

-  loop_head:

-    x := x;

-    goto loop_head, after_loop;

-  after_loop:

-  assert x == 1;  // error

-}

-

-// --------------------------- test {:identity} annotation --------------------

-

-function {:identity} MyId(x: int): int;

-function MyStealthyId(x: int): int;  // this one messes up the abstract interpretation

-function {:identity false} {:identity}/*the last attribute rules*/ MyPolyId<T>(x: T): T;

-function {:identity /*this is a lie*/} MyBogusId(x: int): int { -x }

-function {:identity /*ignored, since the function takes more than one argument*/} MultipleArgs(x: int, y: int): int;

-function {:identity /*ignored, since the return type is not equal to the argument type*/} BoolToInt(b: bool): int;

-function {:identity true/*in some contexts, the type of this function makes sense as an identity*/} SometimesId0<T>(x: T): int;

-function {:identity true/*in some contexts, the type of this function makes sense as an identity*/} SometimesId1<T>(x: int): T;

-function {:identity true/*in some contexts, the type of this function makes sense as an identity*/} SometimesId2<T,U>(x: T): U;

-

-

-procedure Id0(n: int)

-{

-  var i: int;

-  i := 0;

-  while (i < n)

-  {

-    i := i + 1;

-  }

-  assert 0 <= i;

-}

-

-procedure Id1(n: int)

-{

-  var i: int;

-  i := MyId(0);

-  while (i < n)

-  {

-    i := i + MyId(1);

-  }

-  assert 0 <= i;

-}

-

-procedure Id2(n: int)

-{

-  var i: int;

-  i := MyStealthyId(0);

-  while (i < n)

-  {

-    i := i + 1;

-  }

-  assert 0 <= i;  // error: abstract interpreter does not figure this one out

-}

-

-procedure Id3(n: int)

-{

-  var i: int;

-  i := 0;

-  while (i < n)

-  {

-    i := i + MyStealthyId(1);

-  }

-  assert 0 <= i;  // error: abstract interpreter does not figure this one out

-}

-

-procedure Id4(n: int)

-{

-  var i: int;

-  i := MyPolyId(0);

-  while (i < n)

-  {

-    i := i + MyPolyId(1);

-  }

-  assert 0 <= i;

-}

-

-procedure Id5(n: int)

-{

-  var i: int;

-  var b: bool;

-  i, b := 0, false;

-  while (i < n)

-  {

-    i, b := i + 1, false;

-  }

-  assert !b;

-}

-

-procedure Id6(n: int)

-{

-  var i: int;

-  var b: bool;

-  i, b := 0, MyPolyId(false);

-  while (i < n)

-  {

-    i, b := i + 1, false;

-  }

-  assert !b;

-}

-

-procedure Id7(n: int)

-{

-  var i, k, y, z: int;

-  i, k := 0, 0;

-  while (i < n)

-  {

-    i := i + 1;

-    y, z := MyBogusId(5), -5;

-    k := k + z;

-    if (*) {

-      assert y == z;  // fine

-    }

-  }

-  assert 0 <= k;  // error: this does not hold -- k may very well be negative

-}

-

-procedure Id8(n: int)

-{

-  var i, k: int;

-  i, k := 0, 0;

-  while (i < n)

-  {

-    i := i + 1;

-    k := k + MyBogusId(5);

-  }

-  assert 0 <= k;  // since we lied about MyBogusId being an {:identity} function, the abstract interpreter gives us this bogus invariant

-}

-

-procedure Id9(n: int)

-  requires 0 < n;

-{

-  var i, k: int;

-  i, k := 0, 0;

-  while (i < n)

-    invariant i <= n && -k == 5*i;

-  {

-    i := i + 1;

-    k := k + MyBogusId(5);

-  }

-  assert -k == 5*n;

-  assert false;  // this just shows the effect of MyBogusId even more; there is no complaint about this assert

-}

-

-procedure Id10(n: int)

-{

-  var i: int;

-  i := 0;

-  while (i < n)

-  {

-    i := i + MultipleArgs(19, 23);

-  }

-  assert 0 <= i;  // error: no information is known about i

-}

-

-procedure Id11(n: int)

-{

-  var i, k: int;

-  i, k := 0, 0;

-  while (i < n)

-  {

-    i := i + 1;

-    k := k + BoolToInt(false);  // this should not be treated as an identity function, since it goes from one type to another

-  }

-  assert 0 <= k;  // error: no information is known about k

-}

-

-procedure Id12(n: int)

-{

-  var i: int;

-  i := 0;

-  while (i < n)

-  {

-    i := i + SometimesId0(false);

-  }

-  assert 0 <= i;  // error: no information is known about i

-}

-

-procedure Id13(n: int)

-{

-  var i: int;

-  i := 0;

-  while (i < n)

-  {

-    i := i + SometimesId0(1);

-  }

-  assert 0 <= i;

-}

-

-procedure Id14(n: int)

-{

-  var i: int;

-  i := 0;

-  while (i < n)

-  {

-    i := i + SometimesId0(-1);

-  }

-  assert 0 <= i;  // error: this does not hold

-}

-

-procedure Id15(n: int)

-{

-  var i: int;

-  i := 0;

-  while (i < n)

-  {

-    i := i + SometimesId1(1);

-  }

-  assert 0 <= i;  // fine: SometimesId1 claims to be an identity and the use of it is int->int

-}

-

-procedure Id16(n: int)

-{

-  var i: int;

-  i := 0;

-  while (i < n)

-  {

-    i := i + SometimesId2(false);

-  }

-  assert 0 <= i;  // error: no information is known about i

-}

-

-procedure Id17(n: int)

-{

-  var i: int;

-  i := 0;

-  while (i < n)

-  {

-    i := i + SometimesId2(1);

-  }

-  assert 0 <= i;  // fine: SometimesId2 claims to be an identity and the use of it is int->int

-}

-

-// real numbers

-

-procedure W0(N: real)

-{

-  var i, bf0: real;

-  i := 0.0;

-  while (i < N) {

-    bf0 := N - i;

-    i := i + 1.0;

-    // check termination:

-    assert 0.0 <= bf0;

-    assert N - i <= bf0 - 1.0;

-  }

-}

+// RUN: %boogie -infer:j "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+const N: int;
+axiom 0 <= N;
+
+procedure P(K: int)
+  requires 0 <= K;
+{
+  var b: bool, x, k: int;
+
+  if (!b) {
+    b := !b;
+  }
+  x := if b then 13 else 10;
+  k := K;
+  while (k != 0) {
+    x := x + k;
+    k := k - 1;
+  }
+  assert 13 <= x;
+}
+
+procedure Thresholds0()
+{
+  var i: int;
+  i := 0;
+  while (i < 200)
+  {
+    i := i + 1;
+  }
+  assert i == 200;
+}
+
+procedure Thresholds1()
+{
+  var i: int;
+  i := 0;
+  while (i <= 199)
+  {
+    i := i + 1;
+  }
+  assert i == 200;
+}
+
+procedure Thresholds2()
+{
+  var i: int;
+  i := 100;
+  while (0 < i)
+  {
+    i := i - 1;
+  }
+  assert i == 0;
+}
+
+procedure Thresholds3()
+{
+  var i: int;
+  i := 0;
+  while (i < 200)
+  {
+    i := i + 1;
+  }
+  assert i == 199;  // error
+}
+
+procedure Thresholds4()
+{
+  var i: int;
+  i := 0;
+  while (i + 3 < 203)
+  {
+    i := i + 1;
+  }
+  assert i * 2 == 400;  // error: this would hold in an execution, but /infer:j is too weak to infer invariant i<=200
+}
+
+procedure UnaryNegation0() returns (x: int)  // this was once buggy
+{
+  x := -1;
+  loop_head:
+    x := x;
+    goto loop_head, after_loop;
+  after_loop:
+  assert x == -1;
+}
+procedure UnaryNegation1() returns (x: int)  // this was once buggy
+{
+  x := -1;
+  loop_head:
+    x := x;
+    goto loop_head, after_loop;
+  after_loop:
+  assert x == 1;  // error
+}
+
+// --------------------------- test {:identity} annotation --------------------
+
+function {:identity} MyId(x: int): int;
+function MyStealthyId(x: int): int;  // this one messes up the abstract interpretation
+function {:identity false} {:identity}/*the last attribute rules*/ MyPolyId<T>(x: T): T;
+function {:identity /*this is a lie*/} MyBogusId(x: int): int { -x }
+function {:identity /*ignored, since the function takes more than one argument*/} MultipleArgs(x: int, y: int): int;
+function {:identity /*ignored, since the return type is not equal to the argument type*/} BoolToInt(b: bool): int;
+function {:identity true/*in some contexts, the type of this function makes sense as an identity*/} SometimesId0<T>(x: T): int;
+function {:identity true/*in some contexts, the type of this function makes sense as an identity*/} SometimesId1<T>(x: int): T;
+function {:identity true/*in some contexts, the type of this function makes sense as an identity*/} SometimesId2<T,U>(x: T): U;
+
+
+procedure Id0(n: int)
+{
+  var i: int;
+  i := 0;
+  while (i < n)
+  {
+    i := i + 1;
+  }
+  assert 0 <= i;
+}
+
+procedure Id1(n: int)
+{
+  var i: int;
+  i := MyId(0);
+  while (i < n)
+  {
+    i := i + MyId(1);
+  }
+  assert 0 <= i;
+}
+
+procedure Id2(n: int)
+{
+  var i: int;
+  i := MyStealthyId(0);
+  while (i < n)
+  {
+    i := i + 1;
+  }
+  assert 0 <= i;  // error: abstract interpreter does not figure this one out
+}
+
+procedure Id3(n: int)
+{
+  var i: int;
+  i := 0;
+  while (i < n)
+  {
+    i := i + MyStealthyId(1);
+  }
+  assert 0 <= i;  // error: abstract interpreter does not figure this one out
+}
+
+procedure Id4(n: int)
+{
+  var i: int;
+  i := MyPolyId(0);
+  while (i < n)
+  {
+    i := i + MyPolyId(1);
+  }
+  assert 0 <= i;
+}
+
+procedure Id5(n: int)
+{
+  var i: int;
+  var b: bool;
+  i, b := 0, false;
+  while (i < n)
+  {
+    i, b := i + 1, false;
+  }
+  assert !b;
+}
+
+procedure Id6(n: int)
+{
+  var i: int;
+  var b: bool;
+  i, b := 0, MyPolyId(false);
+  while (i < n)
+  {
+    i, b := i + 1, false;
+  }
+  assert !b;
+}
+
+procedure Id7(n: int)
+{
+  var i, k, y, z: int;
+  i, k := 0, 0;
+  while (i < n)
+  {
+    i := i + 1;
+    y, z := MyBogusId(5), -5;
+    k := k + z;
+    if (*) {
+      assert y == z;  // fine
+    }
+  }
+  assert 0 <= k;  // error: this does not hold -- k may very well be negative
+}
+
+procedure Id8(n: int)
+{
+  var i, k: int;
+  i, k := 0, 0;
+  while (i < n)
+  {
+    i := i + 1;
+    k := k + MyBogusId(5);
+  }
+  assert 0 <= k;  // since we lied about MyBogusId being an {:identity} function, the abstract interpreter gives us this bogus invariant
+}
+
+procedure Id9(n: int)
+  requires 0 < n;
+{
+  var i, k: int;
+  i, k := 0, 0;
+  while (i < n)
+    invariant i <= n && -k == 5*i;
+  {
+    i := i + 1;
+    k := k + MyBogusId(5);
+  }
+  assert -k == 5*n;
+  assert false;  // this just shows the effect of MyBogusId even more; there is no complaint about this assert
+}
+
+procedure Id10(n: int)
+{
+  var i: int;
+  i := 0;
+  while (i < n)
+  {
+    i := i + MultipleArgs(19, 23);
+  }
+  assert 0 <= i;  // error: no information is known about i
+}
+
+procedure Id11(n: int)
+{
+  var i, k: int;
+  i, k := 0, 0;
+  while (i < n)
+  {
+    i := i + 1;
+    k := k + BoolToInt(false);  // this should not be treated as an identity function, since it goes from one type to another
+  }
+  assert 0 <= k;  // error: no information is known about k
+}
+
+procedure Id12(n: int)
+{
+  var i: int;
+  i := 0;
+  while (i < n)
+  {
+    i := i + SometimesId0(false);
+  }
+  assert 0 <= i;  // error: no information is known about i
+}
+
+procedure Id13(n: int)
+{
+  var i: int;
+  i := 0;
+  while (i < n)
+  {
+    i := i + SometimesId0(1);
+  }
+  assert 0 <= i;
+}
+
+procedure Id14(n: int)
+{
+  var i: int;
+  i := 0;
+  while (i < n)
+  {
+    i := i + SometimesId0(-1);
+  }
+  assert 0 <= i;  // error: this does not hold
+}
+
+procedure Id15(n: int)
+{
+  var i: int;
+  i := 0;
+  while (i < n)
+  {
+    i := i + SometimesId1(1);
+  }
+  assert 0 <= i;  // fine: SometimesId1 claims to be an identity and the use of it is int->int
+}
+
+procedure Id16(n: int)
+{
+  var i: int;
+  i := 0;
+  while (i < n)
+  {
+    i := i + SometimesId2(false);
+  }
+  assert 0 <= i;  // error: no information is known about i
+}
+
+procedure Id17(n: int)
+{
+  var i: int;
+  i := 0;
+  while (i < n)
+  {
+    i := i + SometimesId2(1);
+  }
+  assert 0 <= i;  // fine: SometimesId2 claims to be an identity and the use of it is int->int
+}
+
+// real numbers
+
+procedure W0(N: real)
+{
+  var i, bf0: real;
+  i := 0.0;
+  while (i < N) {
+    bf0 := N - i;
+    i := i + 1.0;
+    // check termination:
+    assert 0.0 <= bf0;
+    assert N - i <= bf0 - 1.0;
+  }
+}
diff --git a/Test/aitest0/constants.bpl b/Test/aitest0/constants.bpl
index a3b82df7..d2075e26 100644
--- a/Test/aitest0/constants.bpl
+++ b/Test/aitest0/constants.bpl
@@ -1,71 +1,71 @@
-// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify "%s" > "%t"

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

-// Test the constant propagation AI

-

-var GlobalFlag : bool;

-

-const A, B, C:int;		// Consts

-

-procedure Join (b : bool)

-  modifies GlobalFlag;

-{  

-  var x, y, z:int;

-  

-  start:

-    GlobalFlag := true;

-    x := 3;

-    y := 4;

-    z := x + y;

-    goto Then, Else; // if (b)

- 

-  Then:

-    assume b == true;

-    x := x + 1;

-    goto join;

-

-  Else:

-    assume b == false;

-    y := 4;

-    goto join;

-    

-  join:

-    assert y == 4;

-    assert z == 7;

-    assert GlobalFlag == true;

-    return;

-}    

-

-

-procedure Loop ()

-{

-  var c, i: int;

-

-  start:

-    c := 0; i := 0;

-    goto test;

- 

-  test:

-    // if (i < 10);

-    goto Then, Else;

-

-  Then:

-    assume (i < 10);

-    i := i + 1;

-    goto test;

-

-  Else:

-    return;

-}

-

-procedure Evaluate () 

-{

- var i : int;

-

- start:

- i := 5;

- i := 3 * i + 1;

- i := 3 * (i + 1);

- i := 1 + 3 * i;

- i := (i + 1) * 3;

- return;

-}

+// RUN: %boogie -infer:j -instrumentInfer:e -printInstrumented -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+// Test the constant propagation AI
+
+var GlobalFlag : bool;
+
+const A, B, C:int;		// Consts
+
+procedure Join (b : bool)
+  modifies GlobalFlag;
+{  
+  var x, y, z:int;
+  
+  start:
+    GlobalFlag := true;
+    x := 3;
+    y := 4;
+    z := x + y;
+    goto Then, Else; // if (b)
+ 
+  Then:
+    assume b == true;
+    x := x + 1;
+    goto join;
+
+  Else:
+    assume b == false;
+    y := 4;
+    goto join;
+    
+  join:
+    assert y == 4;
+    assert z == 7;
+    assert GlobalFlag == true;
+    return;
+}    
+
+
+procedure Loop ()
+{
+  var c, i: int;
+
+  start:
+    c := 0; i := 0;
+    goto test;
+ 
+  test:
+    // if (i < 10);
+    goto Then, Else;
+
+  Then:
+    assume (i < 10);
+    i := i + 1;
+    goto test;
+
+  Else:
+    return;
+}
+
+procedure Evaluate () 
+{
+ var i : int;
+
+ start:
+ i := 5;
+ i := 3 * i + 1;
+ i := 3 * (i + 1);
+ i := 1 + 3 * i;
+ i := (i + 1) * 3;
+ return;
+}