Initial set of files.

1 files changed, 371 insertions, 0 deletions

diff --git a/Test/test0/ModifiedBag.bpl b/Test/test0/ModifiedBag.bpl
new file mode 100644
index 00000000..09edbd12
--- /dev/null
+++ b/Test/test0/ModifiedBag.bpl
@@ -0,0 +1,371 @@
+// ----------- BEGIN PRELUDE

+type real;

+

+type elements;

+

+type name;

+

+const $CALL: name;

+

+const $REQ: name;

+

+const $ENS: name;

+

+const $PACK: name;

+

+const $UNPACK: name;

+

+const $HEAD: name;

+

+const $THROW: name;

+

+var $RefHeap: [ref, name]ref;

+

+var $IntHeap: [ref, name]int;

+

+var $RealHeap: [ref, name]real;

+

+var $BoolHeap: [ref, name]bool;

+

+var $ArrayHeap: [ref, name]elements;

+

+const $allocated: name;

+

+const $elements: name;

+

+function $ArrayLength(ref) returns (int);

+

+function $RefArrayGet(elements, int) returns (ref);

+

+function $RefArraySet(elements, int, ref) returns (elements);

+

+function $IntArrayGet(elements, int) returns (value: int);

+

+function $IntArraySet(elements, int, value: int) returns (elements);

+

+function $RealArrayGet(elements, int) returns (value: real);

+

+function $RealArraySet(elements, int, value: real) returns (elements);

+

+function $BoolArrayGet(elements, int) returns (value: bool);

+

+function $BoolArraySet(elements, int, value: bool) returns (elements);

+

+function $ArrayArrayGet(elements, int) returns (value: elements);

+

+function $ArrayArraySet(elements, int, value: elements) returns (elements);

+

+axiom (forall A: elements, i: int, x: ref :: $RefArrayGet($RefArraySet(A, i, x), i) == x);

+

+axiom (forall A: elements, i: int, j: int, x: ref :: i != j ==> $RefArrayGet($RefArraySet(A, i, x), j) == $RefArrayGet(A, j));

+

+axiom (forall A: elements, i: int, x: int :: $IntArrayGet($IntArraySet(A, i, x), i) == x);

+

+axiom (forall A: elements, i: int, j: int, x: int :: i != j ==> $IntArrayGet($IntArraySet(A, i, x), j) == $IntArrayGet(A, j));

+

+axiom (forall A: elements, i: int, x: real :: $RealArrayGet($RealArraySet(A, i, x), i) == x);

+

+axiom (forall A: elements, i: int, j: int, x: real :: i != j ==> $RealArrayGet($RealArraySet(A, i, x), j) == $RealArrayGet(A, j));

+

+axiom (forall A: elements, i: int, x: bool :: $BoolArrayGet($BoolArraySet(A, i, x), i) == x);

+

+axiom (forall A: elements, i: int, j: int, x: bool :: i != j ==> $BoolArrayGet($BoolArraySet(A, i, x), j) == $BoolArrayGet(A, j));

+

+axiom (forall A: elements, i: int, x: elements :: $ArrayArrayGet($ArrayArraySet(A, i, x), i) == x);

+

+axiom (forall A: elements, i: int, j: int, x: elements :: i != j ==> $ArrayArrayGet($ArrayArraySet(A, i, x), j) == $ArrayArrayGet(A, j));

+

+axiom (forall a: ref :: 0 <= $ArrayLength(a));

+

+function $typeof(ref) returns (name);

+

+function $BoolIs(bool, name) returns (bool);

+

+function $RealIs(real, name) returns (bool);

+

+function $IntIs(int, name) returns (bool);

+

+const System.Int16: name;

+

+const System.Int32: name;

+

+const System.Int64: name;

+

+const System.Int16.MinValue: int;

+

+const System.Int16.MaxValue: int;

+

+const System.Int32.MinValue: int;

+

+const System.Int32.MaxValue: int;

+

+const System.Int64.MinValue: int;

+

+const System.Int64.MaxValue: int;

+

+axiom System.Int64.MinValue < System.Int32.MinValue;

+

+axiom System.Int32.MinValue < System.Int16.MinValue;

+

+axiom System.Int16.MinValue < System.Int16.MaxValue;

+

+axiom System.Int16.MaxValue < System.Int32.MaxValue;

+

+axiom System.Int32.MaxValue < System.Int64.MaxValue;

+

+axiom (forall i: int :: $IntIs(i, System.Int16) <==> System.Int16.MinValue <= i && i <= System.Int16.MaxValue);

+

+axiom (forall i: int :: $IntIs(i, System.Int32) <==> System.Int32.MinValue <= i && i <= System.Int32.MaxValue);

+

+axiom (forall i: int :: $IntIs(i, System.Int64) <==> System.Int64.MinValue <= i && i <= System.Int64.MaxValue);

+

+function $RefIs(ref, name) returns (bool);

+

+axiom (forall o: ref, T: name :: $RefIs(o, T) <==> o == null || $typeof(o) <: T);

+

+axiom (forall o: ref, T: name :: $RefIs(o, $NotNull(T)) <==> o != null && $RefIs(o, T));

+

+axiom (forall a: ref, T: name, i: int, $ArrayHeap: [ref, name]elements :: $RefIs(a, $IntArray(T)) && a != null ==> $IntIs($IntArrayGet($ArrayHeap[a, $elements], i), T));

+

+axiom (forall a: ref, T: name, i: int, $ArrayHeap: [ref, name]elements  :: $RefIs(a, $RealArray(T)) && a != null ==> $RealIs($RealArrayGet($ArrayHeap[a, $elements], i), T));

+

+axiom (forall a: ref, T: name, i: int, $ArrayHeap: [ref, name]elements  :: $RefIs(a, $BoolArray(T)) && a != null ==> $BoolIs($BoolArrayGet($ArrayHeap[a, $elements], i), T));

+

+axiom (forall a: ref, T: name, i: int, $ArrayHeap: [ref, name]elements  :: $RefIs(a, $RefArray(T)) && a != null ==> $RefIs($RefArrayGet($ArrayHeap[a, $elements], i), T));

+

+function $NotNull(name) returns (name);

+

+function $IntArray(name) returns (name);

+

+function $BoolArray(name) returns (name);

+

+function $RealArray(name) returns (name);

+

+function $RefArray(name) returns (name);

+// ----------- END PRELUDE

+const Bag.a: name;

+

+const Bag.n: name;

+

+const Bag: name;

+

+

+

+

+

+procedure Bag..ctor$(this: ref, initialElements$in: ref);

+

+

+

+

+

+

+procedure System.Object..ctor(this: ref);

+

+

+

+procedure System.Array.CopyTo$System.Array$System.Int32(this: ref, array$in: ref, index$in: int);

+

+

+

+procedure Bag..ctor$$System.Int32$System.Int32(this: ref, initialElements$in: ref, start$in: int, howMany$in: int);

+  requires 0 <= howMany$in;

+  requires start$in + howMany$in <= $ArrayLength(initialElements$in);

+  modifies $IntHeap, $RefHeap;

+

+

+

+implementation Bag..ctor$$System.Int32$System.Int32(this: ref, initialElements$in: ref, start$in: int, howMany$in: int)

+{

+  var initialElements: ref, start: int, howMany: int, stack0i: int, stack0o: ref, stack1i: int, stack2i: int;

+

+  entry:

+    assume $RefIs(this, $NotNull(Bag));

+    initialElements := initialElements$in;

+    assume $RefIs(initialElements, $NotNull($IntArray(System.Int32)));

+    start := start$in;

+    assume $IntIs(start, System.Int32);

+    howMany := howMany$in;

+    assume $IntIs(howMany, System.Int32);

+    goto block165;

+

+  block165:

+    call System.Object..ctor(this);

+    $IntHeap[this, Bag.n] := howMany;

+    stack0i := howMany;

+    havoc stack0o;

+    assume $BoolHeap[stack0o, $allocated] == true && $ArrayLength(stack0o) == stack0i;

+    $RefHeap[this, Bag.a] := stack0o;

+    stack0o := $RefHeap[this, Bag.a];

+    stack1i := 0;

+    stack2i := start + howMany;

+    call System.Array.Copy$System.Array$System.Int32$System.Array$System.Int32$System.Int32(initialElements, start, stack0o, stack1i, stack2i);

+    assert this != null;

+    assert 0 <= $IntHeap[this, Bag.n] && $IntHeap[this, Bag.n] <= $ArrayLength($RefHeap[this, Bag.a]);

+    return;

+}

+

+

+

+procedure System.Array.Copy$System.Array$System.Int32$System.Array$System.Int32$System.Int32(sourceArray$in: ref, sourceIndex$in: int, destinationArray$in: ref, destinationIndex$in: int, length$in: int);

+

+

+

+procedure Bag.Add$System.Int32(this: ref, x$in: int);

+  modifies $ArrayHeap, $IntHeap;

+

+

+

+implementation Bag.Add$System.Int32(this: ref, x$in: int)

+{

+  var x: int, stack0i: int, stack1o: ref, stack1i: int, stack0b: bool, stack0o: ref, stack2i: int, b: ref;

+

+  entry:

+    assume $RefIs(this, $NotNull(Bag));

+    x := x$in;

+    assume $IntIs(x, System.Int32);

+    assert this != null;

+    assume 0 <= $IntHeap[this, Bag.n] && $IntHeap[this, Bag.n] <= $ArrayLength($RefHeap[this, Bag.a]);

+    goto block205;

+

+  block205:

+    stack0i := $IntHeap[this, Bag.n];

+    stack1o := $RefHeap[this, Bag.a];

+    stack1i := $ArrayLength(stack1o);

+    stack1i := stack1i;

+    stack0b := stack0i != stack1i;

+    goto trueblock208, falseblock206;

+

+  trueblock208:

+    assume stack0b == true;

+assume false;

+//    goto block208;

+return;

+

+  falseblock206:

+    assume stack0b == false;

+    goto block206;

+

+  block206:

+//    assert label-([$PACK@0:3:4425:0], $IntHeap[this, Bag.n] <= 2 * $ArrayLength($RefHeap[this, Bag.a]));

+    stack0i := 2;

+    stack1o := $RefHeap[this, Bag.a];

+    stack1i := $ArrayLength(stack1o);

+    stack1i := stack1i;

+    stack0i := stack0i * stack1i;

+    stack0i := stack0i;

+    assert $IntHeap[this, Bag.n] <= stack0i;

+//    havoc b;

+//    assume $BoolHeap[b, $allocated] == true && $ArrayLength(b) == stack0i;

+//    assert label-([$PACK@0:3:4427:0], $IntHeap[this, Bag.n] <= $ArrayLength(b));

+//    stack0o := $RefHeap[this, Bag.a];

+//    stack1i := 0;

+//    call [$CALL@0:7:39:0] System.Array.CopyTo$System.Array$System.Int32(stack0o, b, stack1i);

+//    $RefHeap[this, Bag.a] := b;

+//    assert label-([$PACK@0:3:4428:0], $IntHeap[this, Bag.n] <= $ArrayLength($RefHeap[this, Bag.a]));

+//    goto block208;

+    return;

+

+  block208:

+    stack0o := $RefHeap[this, Bag.a];

+    stack1i := $IntHeap[this, Bag.n];

+    $ArrayHeap[stack0o, $elements] := $IntArraySet($ArrayHeap[stack0o, $elements], stack1i, x);

+    stack0o := this;

+    stack1o := stack0o;

+    stack1i := $IntHeap[stack1o, Bag.n];

+    stack2i := 1;

+    stack1i := stack1i + stack2i;

+    $IntHeap[stack0o, Bag.n] := stack1i;

+    assert this != null;

+    assert 0 <= $IntHeap[this, Bag.n];

+    assert $IntHeap[this, Bag.n] <= $ArrayLength($RefHeap[this, Bag.a]);

+    return;

+

+}

+

+

+

+procedure Bag.ExtractMin(this: ref) returns ($result: int);

+  modifies $IntHeap, $ArrayHeap;

+

+

+

+implementation Bag.ExtractMin(this: ref) returns ($result: int)

+{

+  var m: int, mindex: int, i: int, stack0i: int, stack0b: bool, stack0o: ref, stack1o: ref, stack1i: int, stack2i: int, CS$00000003$00000000: int;

+

+  entry:

+    assume $RefIs(this, $NotNull(Bag));

+    assert this != null;

+    assume 0 <= $IntHeap[this, Bag.n] && $IntHeap[this, Bag.n] <= $ArrayLength($RefHeap[this, Bag.a]);

+    goto block282;

+

+  block282:

+    m := 2147483647;

+    mindex := 0;

+    i := 1;

+    goto block286;

+

+  block285:

+    stack0i := 1;

+    stack0i := i + stack0i;

+    i := stack0i;

+    goto block286;

+

+  block286:

+    stack0i := $IntHeap[this, Bag.n];

+    stack0b := i <= stack0i;

+    goto trueblock283, falseblock287;

+

+  trueblock283:

+    assume stack0b == true;

+    goto block283;

+

+  falseblock287:

+    assume stack0b == false;

+    goto block287;

+

+  block283:

+    stack0o := $RefHeap[this, Bag.a];

+    stack0i := $IntArrayGet($ArrayHeap[stack0o, $elements], i);

+    stack0b := stack0i >= m;

+    goto trueblock285, falseblock284;

+

+  block287:

+    stack0o := this;

+    stack1o := stack0o;

+    stack1i := $IntHeap[stack1o, Bag.n];

+    stack2i := 1;

+    stack1i := stack1i - stack2i;

+    $IntHeap[stack0o, Bag.n] := stack1i;

+    stack0o := $RefHeap[this, Bag.a];

+    stack1o := $RefHeap[this, Bag.a];

+    stack2i := $IntHeap[this, Bag.n];

+    stack1i := $IntArrayGet($ArrayHeap[stack1o, $elements], stack2i);

+    $ArrayHeap[stack0o, $elements] := $IntArraySet($ArrayHeap[stack0o, $elements], mindex, stack1i);

+    CS$00000003$00000000 := m;

+    goto block289;

+

+  trueblock285:

+    assume stack0b == true;

+    goto block285;

+

+  falseblock284:

+    assume stack0b == false;

+    goto block284;

+

+  block284:

+    mindex := i;

+    stack0o := $RefHeap[this, Bag.a];

+    m := $IntArrayGet($ArrayHeap[stack0o, $elements], i);

+    goto block285;

+

+  block289:

+    $result := CS$00000003$00000000;

+    assert this != null;

+    assert 0 <= $IntHeap[this, Bag.n] && $IntHeap[this, Bag.n] <= $ArrayLength($RefHeap[this, Bag.a]);

+    return;

+}

+

+type ref;

+const null : ref;