From d652155ae013f36a1ee17653a8e458baad2d9c2c Mon Sep 17 00:00:00 2001 From: Checkmate50 Date: Mon, 6 Jun 2016 23:14:18 -0600 Subject: Merging complete. Everything looks good *crosses fingers* --- Test/test21/test3_AddMethod_conv.bpl | 3654 +++++++++++++++++----------------- 1 file changed, 1827 insertions(+), 1827 deletions(-) (limited to 'Test/test21/test3_AddMethod_conv.bpl') diff --git a/Test/test21/test3_AddMethod_conv.bpl b/Test/test21/test3_AddMethod_conv.bpl index 89c34c45..beb848f0 100644 --- a/Test/test21/test3_AddMethod_conv.bpl +++ b/Test/test21/test3_AddMethod_conv.bpl @@ -1,1827 +1,1827 @@ -// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" -// RUN: %diff "%s.n.expect" "%t" -// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" -// RUN: %diff "%s.p.expect" "%t" -// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" -// RUN: %diff "%s.a.expect" "%t" -// XFAIL: * -// Spec# program verifier version 0.90, Copyright (c) 2003-2008, Microsoft. -// Command Line Options: /print:debug.txt AddMethod.dll - -type real; - -type elements; - -type struct; - -type name; -type any; - -type exposeVersionType; - -type Field a; -type Heap = [ref,Field x]x; - -var $Heap: Heap where IsHeap($Heap); - -type ActivityType; - -var $ActivityIndicator: ActivityType; - -function IsHeap(h: Heap) returns (bool); - -const unique $allocated: Field bool; - -const unique $elements: Field elements; - -function DeclType222(Field a) returns (name); - -axiom DeclType222($elements) == System.Object; - -const unique $inv: Field name; - -const unique $localinv: Field name; - -const unique $exposeVersion: Field exposeVersionType; - -axiom DeclType222($exposeVersion) == System.Object; - -const unique $sharingMode: Field any; - -const unique $SharingMode_Unshared: any; - -const unique $SharingMode_LockProtected: any; - -const unique $ownerRef: Field ref; - -const unique $ownerFrame: Field name; - -const unique $PeerGroupPlaceholder: name; - -function ClassRepr(class: name) returns (ref); - -function ClassReprInv(ref) returns (name); - -axiom (forall c: name :: { ClassRepr(c) } ClassReprInv(ClassRepr(c)) == c); - -axiom (forall T: name :: !($typeof(ClassRepr(T)) <: System.Object)); - -axiom (forall T: name :: ClassRepr(T) != null); - -axiom (forall T: name, h: Heap :: { h[ClassRepr(T), $ownerFrame] } IsHeap(h) ==> h[ClassRepr(T), $ownerFrame] == $PeerGroupPlaceholder); - -function IncludeInMainFrameCondition(f: Field a) returns (bool); - -axiom IncludeInMainFrameCondition($allocated); - -axiom IncludeInMainFrameCondition($elements); - -axiom !IncludeInMainFrameCondition($inv); - -axiom !IncludeInMainFrameCondition($localinv); - -axiom IncludeInMainFrameCondition($ownerRef); - -axiom IncludeInMainFrameCondition($ownerFrame); - -axiom IncludeInMainFrameCondition($exposeVersion); - -axiom !IncludeInMainFrameCondition($FirstConsistentOwner); - -function IsStaticField(f: Field a) returns (bool); - -axiom !IsStaticField($allocated); - -axiom !IsStaticField($elements); - -axiom !IsStaticField($inv); - -axiom !IsStaticField($localinv); - -axiom !IsStaticField($exposeVersion); - -function $IncludedInModifiesStar(f: Field a) returns (bool); - -axiom !$IncludedInModifiesStar($ownerRef); - -axiom !$IncludedInModifiesStar($ownerFrame); - -axiom $IncludedInModifiesStar($exposeVersion); - -axiom $IncludedInModifiesStar($elements); - -function ValueArrayGet(elements, int) returns (any); - -function ValueArraySet(elements, int, any) returns (elements); - -function IntArrayGet(elements, int) returns (int); - -function IntArraySet(elements, int, int) returns (elements); - -function RefArrayGet(elements, int) returns (ref); - -function RefArraySet(elements, int, ref) returns (elements); - -axiom (forall A: elements, i: int, x: any :: ValueArrayGet(ValueArraySet(A, i, x), i) == x); - -axiom (forall A: elements, i: int, j: int, x: any :: i != j ==> ValueArrayGet(ValueArraySet(A, i, x), j) == ValueArrayGet(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: 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)); - -function ArrayIndex(arr: ref, dim: int, indexAtDim: int, remainingIndexContribution: int) returns (int); - -function ArrayIndexInvX(arrayIndex: int) returns (indexAtDim: int); - -function ArrayIndexInvY(arrayIndex: int) returns (remainingIndexContribution: int); - -axiom (forall a: ref, d: int, x: int, y: int :: { ArrayIndex(a, d, x, y) } ArrayIndexInvX(ArrayIndex(a, d, x, y)) == x); - -axiom (forall a: ref, d: int, x: int, y: int :: { ArrayIndex(a, d, x, y) } ArrayIndexInvY(ArrayIndex(a, d, x, y)) == y); - -axiom (forall a: ref, i: int, heap: Heap :: { IntArrayGet(heap[a, $elements], i) } IsHeap(heap) ==> InRange(IntArrayGet(heap[a, $elements], i), $ElementType($typeof(a)))); - -axiom (forall a: ref, i: int, heap: Heap :: { $typeof(RefArrayGet(heap[a, $elements], i)) } IsHeap(heap) && RefArrayGet(heap[a, $elements], i) != null ==> $typeof(RefArrayGet(heap[a, $elements], i)) <: $ElementType($typeof(a))); - -axiom (forall a: ref, T: name, i: int, r: int, heap: Heap :: { $typeof(a) <: NonNullRefArray(T, r), RefArrayGet(heap[a, $elements], i) } IsHeap(heap) && $typeof(a) <: NonNullRefArray(T, r) ==> RefArrayGet(heap[a, $elements], i) != null); - -function $Rank(ref) returns (int); - -axiom (forall a: ref :: 1 <= $Rank(a)); - -axiom (forall a: ref, T: name, r: int :: { $typeof(a) <: RefArray(T, r) } a != null && $typeof(a) <: RefArray(T, r) ==> $Rank(a) == r); - -axiom (forall a: ref, T: name, r: int :: { $typeof(a) <: NonNullRefArray(T, r) } a != null && $typeof(a) <: NonNullRefArray(T, r) ==> $Rank(a) == r); - -axiom (forall a: ref, T: name, r: int :: { $typeof(a) <: ValueArray(T, r) } a != null && $typeof(a) <: ValueArray(T, r) ==> $Rank(a) == r); - -axiom (forall a: ref, T: name, r: int :: { $typeof(a) <: IntArray(T, r) } a != null && $typeof(a) <: IntArray(T, r) ==> $Rank(a) == r); - -function $Length(ref) returns (int); - -axiom (forall a: ref :: { $Length(a) } 0 <= $Length(a) && $Length(a) <= int#2147483647); - -function $DimLength(ref, int) returns (int); - -axiom (forall a: ref, i: int :: 0 <= $DimLength(a, i)); - -axiom (forall a: ref :: { $DimLength(a, 0) } $Rank(a) == 1 ==> $DimLength(a, 0) == $Length(a)); - -function $LBound(ref, int) returns (int); - -function $UBound(ref, int) returns (int); - -axiom (forall a: ref, i: int :: { $LBound(a, i) } $LBound(a, i) == 0); - -axiom (forall a: ref, i: int :: { $UBound(a, i) } $UBound(a, i) == $DimLength(a, i) - 1); - -const unique $ArrayCategoryValue: name; - -const unique $ArrayCategoryInt: name; - -const unique $ArrayCategoryRef: name; - -const unique $ArrayCategoryNonNullRef: name; - -function $ArrayCategory(arrayType: name) returns (arrayCategory: name); - -axiom (forall T: name, ET: name, r: int :: { T <: ValueArray(ET, r) } T <: ValueArray(ET, r) ==> $ArrayCategory(T) == $ArrayCategoryValue); - -axiom (forall T: name, ET: name, r: int :: { T <: IntArray(ET, r) } T <: IntArray(ET, r) ==> $ArrayCategory(T) == $ArrayCategoryInt); - -axiom (forall T: name, ET: name, r: int :: { T <: RefArray(ET, r) } T <: RefArray(ET, r) ==> $ArrayCategory(T) == $ArrayCategoryRef); - -axiom (forall T: name, ET: name, r: int :: { T <: NonNullRefArray(ET, r) } T <: NonNullRefArray(ET, r) ==> $ArrayCategory(T) == $ArrayCategoryNonNullRef); - -const unique System.Array: name; - -axiom System.Array <: System.Object; - -function $ElementType(name) returns (name); - -function ValueArray(elementType: name, rank: int) returns (name); - -axiom (forall T: name, r: int :: { ValueArray(T, r) } ValueArray(T, r) <: ValueArray(T, r) && ValueArray(T, r) <: System.Array); - -function IntArray(elementType: name, rank: int) returns (name); - -axiom (forall T: name, r: int :: { IntArray(T, r) } IntArray(T, r) <: IntArray(T, r) && IntArray(T, r) <: System.Array); - -function RefArray(elementType: name, rank: int) returns (name); - -axiom (forall T: name, r: int :: { RefArray(T, r) } RefArray(T, r) <: RefArray(T, r) && RefArray(T, r) <: System.Array); - -function NonNullRefArray(elementType: name, rank: int) returns (name); - -axiom (forall T: name, r: int :: { NonNullRefArray(T, r) } NonNullRefArray(T, r) <: NonNullRefArray(T, r) && NonNullRefArray(T, r) <: System.Array); - -function NonNullRefArrayRaw(array: ref, elementType: name, rank: int) returns (bool); - -axiom (forall array: ref, elementType: name, rank: int :: { NonNullRefArrayRaw(array, elementType, rank) } NonNullRefArrayRaw(array, elementType, rank) ==> $typeof(array) <: System.Array && $Rank(array) == rank && elementType <: $ElementType($typeof(array))); - -axiom (forall T: name, U: name, r: int :: U <: T ==> RefArray(U, r) <: RefArray(T, r)); - -axiom (forall T: name, U: name, r: int :: U <: T ==> NonNullRefArray(U, r) <: NonNullRefArray(T, r)); - -axiom (forall A: name, r: int :: $ElementType(ValueArray(A, r)) == A); - -axiom (forall A: name, r: int :: $ElementType(IntArray(A, r)) == A); - -axiom (forall A: name, r: int :: $ElementType(RefArray(A, r)) == A); - -axiom (forall A: name, r: int :: $ElementType(NonNullRefArray(A, r)) == A); - -axiom (forall A: name, r: int, T: name :: { T <: RefArray(A, r) } T <: RefArray(A, r) ==> T != A && T == RefArray($ElementType(T), r) && $ElementType(T) <: A); - -axiom (forall A: name, r: int, T: name :: { T <: NonNullRefArray(A, r) } T <: NonNullRefArray(A, r) ==> T != A && T == NonNullRefArray($ElementType(T), r) && $ElementType(T) <: A); - -axiom (forall A: name, r: int, T: name :: { T <: ValueArray(A, r) } T <: ValueArray(A, r) ==> T == ValueArray(A, r)); - -axiom (forall A: name, r: int, T: name :: { T <: IntArray(A, r) } T <: IntArray(A, r) ==> T == IntArray(A, r)); - -axiom (forall A: name, r: int, T: name :: { RefArray(A, r) <: T } RefArray(A, r) <: T ==> System.Array <: T || (T == RefArray($ElementType(T), r) && A <: $ElementType(T))); - -axiom (forall A: name, r: int, T: name :: { NonNullRefArray(A, r) <: T } NonNullRefArray(A, r) <: T ==> System.Array <: T || (T == NonNullRefArray($ElementType(T), r) && A <: $ElementType(T))); - -axiom (forall A: name, r: int, T: name :: { ValueArray(A, r) <: T } ValueArray(A, r) <: T ==> System.Array <: T || T == ValueArray(A, r)); - -axiom (forall A: name, r: int, T: name :: { IntArray(A, r) <: T } IntArray(A, r) <: T ==> System.Array <: T || T == IntArray(A, r)); - -function $ArrayPtr(elementType: name) returns (name); - -function $ElementProxy(ref, int) returns (ref); - -function $ElementProxyStruct(struct, int) returns (ref); - -axiom (forall a: ref, i: int, heap: Heap :: { heap[RefArrayGet(heap[a, $elements], i), $ownerRef] } { heap[RefArrayGet(heap[a, $elements], i), $ownerFrame] } IsHeap(heap) && $typeof(a) <: System.Array ==> RefArrayGet(heap[a, $elements], i) == null || $IsImmutable($typeof(RefArrayGet(heap[a, $elements], i))) || (heap[RefArrayGet(heap[a, $elements], i), $ownerRef] == heap[$ElementProxy(a, 0 - 1), $ownerRef] && heap[RefArrayGet(heap[a, $elements], i), $ownerFrame] == heap[$ElementProxy(a, 0 - 1), $ownerFrame])); - -axiom (forall a: ref, heap: Heap :: { IsAllocated(heap, a) } IsHeap(heap) && IsAllocated(heap, a) && $typeof(a) <: System.Array ==> IsAllocated(heap, $ElementProxy(a, 0 - 1))); - -axiom (forall o: ref, pos: int :: { $typeof($ElementProxy(o, pos)) } $typeof($ElementProxy(o, pos)) == System.Object); - -axiom (forall o: struct, pos: int :: { $typeof($ElementProxyStruct(o, pos)) } $typeof($ElementProxyStruct(o, pos)) == System.Object); - -function $StructGet(struct, name) returns (any); - -function $StructSet(struct, name, any) returns (struct); - -axiom (forall s: struct, f: name, x: any :: $StructGet($StructSet(s, f, x), f) == x); - -axiom (forall s: struct, f: name, f': name, x: any :: f != f' ==> $StructGet($StructSet(s, f, x), f') == $StructGet(s, f')); - -function ZeroInit(s: struct, typ: name) returns (bool); - -function $typeof(ref) returns (name); - -function $BaseClass(sub: name) returns (base: name); - -axiom (forall T: name :: { $BaseClass(T) } T <: $BaseClass(T) && (T != System.Object ==> T != $BaseClass(T))); - -function AsDirectSubClass(sub: name, base: name) returns (sub': name); - -function OneClassDown(sub: name, base: name) returns (directSub: name); - -axiom (forall A: name, B: name, C: name :: { C <: AsDirectSubClass(B, A) } C <: AsDirectSubClass(B, A) ==> OneClassDown(C, A) == B); - -function $IsValueType(name) returns (bool); - -axiom (forall T: name :: $IsValueType(T) ==> (forall U: name :: T <: U ==> T == U) && (forall U: name :: U <: T ==> T == U)); - -const unique System.Boolean: name; - -axiom $IsValueType(System.Boolean); - -const unique System.Object: name; - -function $IsTokenForType(struct, name) returns (bool); - -function TypeObject(name) returns (ref); - -const unique System.Type: name; - -axiom System.Type <: System.Object; - -axiom (forall T: name :: { TypeObject(T) } $IsNotNull(TypeObject(T), System.Type)); - -function TypeName(ref) returns (name); - -axiom (forall T: name :: { TypeObject(T) } TypeName(TypeObject(T)) == T); - -function $Is(ref, name) returns (bool); - -axiom (forall o: ref, T: name :: { $Is(o, T) } $Is(o, T) <==> o == null || $typeof(o) <: T); - -function $IsNotNull(ref, name) returns (bool); - -axiom (forall o: ref, T: name :: { $IsNotNull(o, T) } $IsNotNull(o, T) <==> o != null && $Is(o, T)); - -function $As(ref, name) returns (ref); - -axiom (forall o: ref, T: name :: $Is(o, T) ==> $As(o, T) == o); - -axiom (forall o: ref, T: name :: !$Is(o, T) ==> $As(o, T) == null); - -axiom (forall h: Heap, o: ref :: { $typeof(o) <: System.Array, h[o, $inv] } IsHeap(h) && o != null && $typeof(o) <: System.Array ==> h[o, $inv] == $typeof(o) && h[o, $localinv] == $typeof(o)); - -function IsAllocated(h: Heap, o: a) returns (bool); - -axiom (forall h: Heap, o: ref, f: Field a :: { IsAllocated(h, h[o, f]) } IsHeap(h) && h[o, $allocated] ==> IsAllocated(h, h[o, f])); - -axiom (forall h: Heap, o: ref, f: Field ref :: { h[h[o, f], $allocated] } IsHeap(h) && h[o, $allocated] ==> h[h[o, f], $allocated]); - -axiom (forall h: Heap, s: struct, f: name :: { IsAllocated(h, $StructGet(s, f)) } IsAllocated(h, s) ==> IsAllocated(h, $StructGet(s, f))); - -axiom (forall h: Heap, e: elements, i: int :: { IsAllocated(h, RefArrayGet(e, i)) } IsAllocated(h, e) ==> IsAllocated(h, RefArrayGet(e, i))); - -axiom (forall h: Heap, e: elements, i: int :: { IsAllocated(h, ValueArrayGet(e, i)) } IsAllocated(h, e) ==> IsAllocated(h, ValueArrayGet(e, i))); - -axiom (forall h: Heap, o: ref :: { h[o, $allocated] } IsAllocated(h, o) ==> h[o, $allocated]); - -axiom (forall h: Heap, c: name :: { h[ClassRepr(c), $allocated] } IsHeap(h) ==> h[ClassRepr(c), $allocated]); - -const $BeingConstructed: ref; - -const unique $NonNullFieldsAreInitialized: Field bool; - -const $PurityAxiomsCanBeAssumed: bool; - -axiom DeclType222($NonNullFieldsAreInitialized) == System.Object; - - - -function AsNonNullRefField(field: Field ref, T: name) returns (f: Field ref); - -function AsRefField(field: Field ref, T: name) returns (f: Field ref); - -function AsRangeField(field: Field int, T: name) returns (f: Field int); - -axiom (forall f: Field ref, T: name :: { AsNonNullRefField(f, T) } AsNonNullRefField(f, T) == f ==> AsRefField(f, T) == f); - -axiom (forall h: Heap, o: ref, f: Field ref, T: name :: { h[o, AsRefField(f, T)] } IsHeap(h) ==> $Is(h[o, AsRefField(f, T)], T)); - -axiom (forall h: Heap, o: ref, f: Field ref, T: name :: { h[o, AsNonNullRefField(f, T)] } IsHeap(h) && o != null && (o != $BeingConstructed || h[$BeingConstructed, $NonNullFieldsAreInitialized] == true) ==> h[o, AsNonNullRefField(f, T)] != null); - -axiom (forall h: Heap, o: ref, f: Field int, T: name :: { h[o, AsRangeField(f, T)] } IsHeap(h) ==> InRange(h[o, AsRangeField(f, T)], T)); - -function $IsMemberlessType(name) returns (bool); - -axiom (forall o: ref :: { $IsMemberlessType($typeof(o)) } !$IsMemberlessType($typeof(o))); - -function $AsInterface(name) returns (name); - -axiom (forall $J: name, s: any, b: ref :: { UnboxedType(Box(s, b)) <: $AsInterface($J) } $AsInterface($J) == $J && Box(s, b) == b && UnboxedType(Box(s, b)) <: $AsInterface($J) ==> $typeof(b) <: $J); - -function $HeapSucc(oldHeap: Heap, newHeap: Heap) returns (bool); - -function $IsImmutable(T: name) returns (bool); - -axiom !$IsImmutable(System.Object); - -function $AsImmutable(T: name) returns (theType: name); - -function $AsMutable(T: name) returns (theType: name); - -axiom (forall T: name, U: name :: { U <: $AsImmutable(T) } U <: $AsImmutable(T) ==> $IsImmutable(U) && $AsImmutable(U) == U); - -axiom (forall T: name, U: name :: { U <: $AsMutable(T) } U <: $AsMutable(T) ==> !$IsImmutable(U) && $AsMutable(U) == U); - -function AsOwner(string: ref, owner: ref) returns (theString: ref); - -axiom (forall o: ref, T: name :: { $typeof(o) <: $AsImmutable(T) } o != null && o != $BeingConstructed && $typeof(o) <: $AsImmutable(T) ==> (forall h: Heap :: { IsHeap(h) } IsHeap(h) ==> h[o, $inv] == $typeof(o) && h[o, $localinv] == $typeof(o) && h[o, $ownerFrame] == $PeerGroupPlaceholder && AsOwner(o, h[o, $ownerRef]) == o && (forall t: ref :: { AsOwner(o, h[t, $ownerRef]) } AsOwner(o, h[t, $ownerRef]) == o ==> t == o || h[t, $ownerFrame] != $PeerGroupPlaceholder))); - -const unique System.String: name; - -function $StringLength(ref) returns (int); - -axiom (forall s: ref :: { $StringLength(s) } 0 <= $StringLength(s)); - -function AsRepField(f: Field ref, declaringType: name) returns (theField: Field ref); - -axiom (forall h: Heap, o: ref, f: Field ref, T: name :: { h[o, AsRepField(f, T)] } IsHeap(h) && h[o, AsRepField(f, T)] != null ==> h[h[o, AsRepField(f, T)], $ownerRef] == o && h[h[o, AsRepField(f, T)], $ownerFrame] == T); - -function AsPeerField(f: Field ref) returns (theField: Field ref); - -axiom (forall h: Heap, o: ref, f: Field ref :: { h[o, AsPeerField(f)] } IsHeap(h) && h[o, AsPeerField(f)] != null ==> h[h[o, AsPeerField(f)], $ownerRef] == h[o, $ownerRef] && h[h[o, AsPeerField(f)], $ownerFrame] == h[o, $ownerFrame]); - -function AsElementsRepField(f: Field ref, declaringType: name, position: int) returns (theField: Field ref); - -axiom (forall h: Heap, o: ref, f: Field ref, T: name, i: int :: { h[o, AsElementsRepField(f, T, i)] } IsHeap(h) && h[o, AsElementsRepField(f, T, i)] != null ==> h[$ElementProxy(h[o, AsElementsRepField(f, T, i)], i), $ownerRef] == o && h[$ElementProxy(h[o, AsElementsRepField(f, T, i)], i), $ownerFrame] == T); - -function AsElementsPeerField(f: Field ref, position: int) returns (theField: Field ref); - -axiom (forall h: Heap, o: ref, f: Field ref, i: int :: { h[o, AsElementsPeerField(f, i)] } IsHeap(h) && h[o, AsElementsPeerField(f, i)] != null ==> h[$ElementProxy(h[o, AsElementsPeerField(f, i)], i), $ownerRef] == h[o, $ownerRef] && h[$ElementProxy(h[o, AsElementsPeerField(f, i)], i), $ownerFrame] == h[o, $ownerFrame]); - -axiom (forall h: Heap, o: ref :: { h[h[o, $ownerRef], $inv] <: h[o, $ownerFrame] } IsHeap(h) && h[o, $ownerFrame] != $PeerGroupPlaceholder && h[h[o, $ownerRef], $inv] <: h[o, $ownerFrame] && h[h[o, $ownerRef], $localinv] != $BaseClass(h[o, $ownerFrame]) ==> h[o, $inv] == $typeof(o) && h[o, $localinv] == $typeof(o)); - -procedure $SetOwner(o: ref, ow: ref, fr: name); - modifies $Heap; - ensures (forall p: ref, F: Field a :: { $Heap[p, F] } (F != $ownerRef && F != $ownerFrame) || old($Heap[p, $ownerRef] != $Heap[o, $ownerRef]) || old($Heap[p, $ownerFrame] != $Heap[o, $ownerFrame]) ==> old($Heap[p, F]) == $Heap[p, F]); - ensures (forall p: ref :: { $Heap[p, $ownerRef] } { $Heap[p, $ownerFrame] } old($Heap[p, $ownerRef] == $Heap[o, $ownerRef]) && old($Heap[p, $ownerFrame] == $Heap[o, $ownerFrame]) ==> $Heap[p, $ownerRef] == ow && $Heap[p, $ownerFrame] == fr); - free ensures $HeapSucc(old($Heap), $Heap); - - - -procedure $UpdateOwnersForRep(o: ref, T: name, e: ref); - modifies $Heap; - ensures (forall p: ref, F: Field a :: { $Heap[p, F] } (F != $ownerRef && F != $ownerFrame) || old($Heap[p, $ownerRef] != $Heap[e, $ownerRef]) || old($Heap[p, $ownerFrame] != $Heap[e, $ownerFrame]) ==> old($Heap[p, F]) == $Heap[p, F]); - ensures e == null ==> $Heap == old($Heap); - ensures e != null ==> (forall p: ref :: { $Heap[p, $ownerRef] } { $Heap[p, $ownerFrame] } old($Heap[p, $ownerRef] == $Heap[e, $ownerRef]) && old($Heap[p, $ownerFrame] == $Heap[e, $ownerFrame]) ==> $Heap[p, $ownerRef] == o && $Heap[p, $ownerFrame] == T); - free ensures $HeapSucc(old($Heap), $Heap); - - - -procedure $UpdateOwnersForPeer(c: ref, d: ref); - modifies $Heap; - ensures (forall p: ref, F: Field a :: { $Heap[p, F] } (F != $ownerRef && F != $ownerFrame) || old($Heap[p, $ownerRef] != $Heap[d, $ownerRef] || $Heap[p, $ownerFrame] != $Heap[d, $ownerFrame]) ==> old($Heap[p, F]) == $Heap[p, F]); - ensures d == null ==> $Heap == old($Heap); - ensures d != null ==> (forall p: ref :: { $Heap[p, $ownerRef] } { $Heap[p, $ownerFrame] } old($Heap[p, $ownerRef] == $Heap[d, $ownerRef] && $Heap[p, $ownerFrame] == $Heap[d, $ownerFrame]) ==> $Heap[p, $ownerRef] == old($Heap)[c, $ownerRef] && $Heap[p, $ownerFrame] == old($Heap)[c, $ownerFrame]); - free ensures $HeapSucc(old($Heap), $Heap); - - - -const unique $FirstConsistentOwner: Field ref; - -function $AsPureObject(ref) returns (ref); - -function ##FieldDependsOnFCO(o: ref, f: Field a, ev: exposeVersionType) returns (value: any); - -axiom (forall o: ref, f: Field a, h: Heap :: { h[$AsPureObject(o), f] } IsHeap(h) && o != null && h[o, $allocated] == true && $AsPureObject(o) == o && h[o, $ownerFrame] != $PeerGroupPlaceholder && h[h[o, $ownerRef], $inv] <: h[o, $ownerFrame] && h[h[o, $ownerRef], $localinv] != $BaseClass(h[o, $ownerFrame]) ==> h[o, f] == ##FieldDependsOnFCO(o, f, h[h[o, $FirstConsistentOwner], $exposeVersion])); - -axiom (forall o: ref, h: Heap :: { h[o, $FirstConsistentOwner] } IsHeap(h) && o != null && h[o, $allocated] == true && h[o, $ownerFrame] != $PeerGroupPlaceholder && h[h[o, $ownerRef], $inv] <: h[o, $ownerFrame] && h[h[o, $ownerRef], $localinv] != $BaseClass(h[o, $ownerFrame]) ==> h[o, $FirstConsistentOwner] != null && h[h[o, $FirstConsistentOwner], $allocated] == true && (h[h[o, $FirstConsistentOwner], $ownerFrame] == $PeerGroupPlaceholder || !(h[h[h[o, $FirstConsistentOwner], $ownerRef], $inv] <: h[h[o, $FirstConsistentOwner], $ownerFrame]) || h[h[h[o, $FirstConsistentOwner], $ownerRef], $localinv] == $BaseClass(h[h[o, $FirstConsistentOwner], $ownerFrame]))); - -function Box(a, ref) returns (ref); - -function Unbox(ref) returns (any); - -type NondetType; - -function MeldNondets(NondetType, any) returns (NondetType); - -function BoxFunc(value: a, typ: name) returns (boxedValue: ref); - -function AllocFunc(typ: name) returns (newValue: ref); - -function NewInstance(object: ref, occurrence: NondetType, activity: ActivityType) returns (newInstance: ref); - -axiom (forall value: any, typ: name, occurrence: NondetType, activity: ActivityType :: { NewInstance(BoxFunc(value, typ), occurrence, activity) } Box(value, NewInstance(BoxFunc(value, typ), occurrence, activity)) == NewInstance(BoxFunc(value, typ), occurrence, activity) && UnboxedType(NewInstance(BoxFunc(value, typ), occurrence, activity)) == typ); - -axiom (forall x: ref, typ: name, occurrence: NondetType, activity: ActivityType :: !$IsValueType(UnboxedType(x)) ==> NewInstance(BoxFunc(x, typ), occurrence, activity) == x); - -axiom (forall x: any, p: ref :: { Unbox(Box(x, p)) } Unbox(Box(x, p)) == x); - -function UnboxedType(ref) returns (name); - -axiom (forall p: ref :: { $IsValueType(UnboxedType(p)) } $IsValueType(UnboxedType(p)) ==> (forall heap: Heap, x: any :: { heap[Box(x, p), $inv] } IsHeap(heap) ==> heap[Box(x, p), $inv] == $typeof(Box(x, p)) && heap[Box(x, p), $localinv] == $typeof(Box(x, p)))); - -axiom (forall x: a, p: ref :: { UnboxedType(Box(x, p)) <: System.Object } UnboxedType(Box(x, p)) <: System.Object && Box(x, p) == p ==> x == p); - -function BoxTester(p: ref, typ: name) returns (ref); - -axiom (forall p: ref, typ: name :: { BoxTester(p, typ) } UnboxedType(p) == typ <==> BoxTester(p, typ) != null); - -axiom (forall p: ref, typ: name :: { BoxTester(p, typ) } BoxTester(p, typ) != null ==> Box(Unbox(p), p) == p); - -axiom (forall typ: name, occurrence: NondetType, activity: ActivityType :: { NewInstance(AllocFunc(typ), occurrence, activity) } $typeof(NewInstance(AllocFunc(typ), occurrence, activity)) == typ && NewInstance(AllocFunc(typ), occurrence, activity) != null); - -axiom (forall typ: name, occurrence: NondetType, activity: ActivityType, heap: Heap :: { heap[NewInstance(AllocFunc(typ), occurrence, activity), $allocated] } IsHeap(heap) ==> heap[NewInstance(AllocFunc(typ), occurrence, activity), $allocated]); - -const unique System.SByte: name; - -axiom $IsValueType(System.SByte); - -const unique System.Byte: name; - -axiom $IsValueType(System.Byte); - -const unique System.Int16: name; - -axiom $IsValueType(System.Int16); - -const unique System.UInt16: name; - -axiom $IsValueType(System.UInt16); - -const unique System.Int32: name; - -axiom $IsValueType(System.Int32); - -const unique System.UInt32: name; - -axiom $IsValueType(System.UInt32); - -const unique System.Int64: name; - -axiom $IsValueType(System.Int64); - -const unique System.UInt64: name; - -axiom $IsValueType(System.UInt64); - -const unique System.Char: name; - -axiom $IsValueType(System.Char); - -const unique System.UIntPtr: name; - -axiom $IsValueType(System.UIntPtr); - -const unique System.IntPtr: name; - -axiom $IsValueType(System.IntPtr); - -const int#m2147483648: int; - -const int#2147483647: int; - -const int#4294967295: int; - -const int#m9223372036854775808: int; - -const int#9223372036854775807: int; - -const int#18446744073709551615: int; - -axiom int#m9223372036854775808 < int#m2147483648; - -axiom int#m2147483648 < 0 - 100000; - -axiom 100000 < int#2147483647; - -axiom int#2147483647 < int#4294967295; - -axiom int#4294967295 < int#9223372036854775807; - -axiom int#9223372036854775807 < int#18446744073709551615; - -axiom int#m9223372036854775808 + 1 == 0 - int#9223372036854775807; - -axiom int#m2147483648 + 1 == 0 - int#2147483647; - -function InRange(i: int, T: name) returns (bool); - -axiom (forall i: int :: InRange(i, System.SByte) <==> 0 - 128 <= i && i < 128); - -axiom (forall i: int :: InRange(i, System.Byte) <==> 0 <= i && i < 256); - -axiom (forall i: int :: InRange(i, System.Int16) <==> 0 - 32768 <= i && i < 32768); - -axiom (forall i: int :: InRange(i, System.UInt16) <==> 0 <= i && i < 65536); - -axiom (forall i: int :: InRange(i, System.Int32) <==> int#m2147483648 <= i && i <= int#2147483647); - -axiom (forall i: int :: InRange(i, System.UInt32) <==> 0 <= i && i <= int#4294967295); - -axiom (forall i: int :: InRange(i, System.Int64) <==> int#m9223372036854775808 <= i && i <= int#9223372036854775807); - -axiom (forall i: int :: InRange(i, System.UInt64) <==> 0 <= i && i <= int#18446744073709551615); - -axiom (forall i: int :: InRange(i, System.Char) <==> 0 <= i && i < 65536); - -function $IntToInt(val: int, fromType: name, toType: name) returns (int); - -function $IntToReal(int, fromType: name, toType: name) returns (real); - -function $RealToInt(real, fromType: name, toType: name) returns (int); - -function $RealToReal(val: real, fromType: name, toType: name) returns (real); - -axiom (forall z: int, B: name, C: name :: InRange(z, C) ==> $IntToInt(z, B, C) == z); - -function $SizeIs(name, int) returns (bool); - -function $IfThenElse(bool, any, any) returns (any); - -axiom (forall b: bool, x: any, y: any :: { $IfThenElse(b, x, y) } b ==> $IfThenElse(b, x, y) == x); - -axiom (forall b: bool, x: any, y: any :: { $IfThenElse(b, x, y) } !b ==> $IfThenElse(b, x, y) == y); - -function #neg(int) returns (int); - -function #and(int, int) returns (int); - -function #or(int, int) returns (int); - -function #xor(int, int) returns (int); - -function #shl(int, int) returns (int); - -function #shr(int, int) returns (int); - -function #rneg(real) returns (real); - -function #radd(real, real) returns (real); - -function #rsub(real, real) returns (real); - -function #rmul(real, real) returns (real); - -function #rdiv(real, real) returns (real); - -function #rmod(real, real) returns (real); - -function #rLess(real, real) returns (bool); - -function #rAtmost(real, real) returns (bool); - -function #rEq(real, real) returns (bool); - -function #rNeq(real, real) returns (bool); - -function #rAtleast(real, real) returns (bool); - -function #rGreater(real, real) returns (bool); - -axiom (forall x: int, y: int :: { x % y } { x / y } x % y == x - x / y * y); - -axiom (forall x: int, y: int :: { x % y } 0 <= x && 0 < y ==> 0 <= x % y && x % y < y); - -axiom (forall x: int, y: int :: { x % y } 0 <= x && y < 0 ==> 0 <= x % y && x % y < 0 - y); - -axiom (forall x: int, y: int :: { x % y } x <= 0 && 0 < y ==> 0 - y < x % y && x % y <= 0); - -axiom (forall x: int, y: int :: { x % y } x <= 0 && y < 0 ==> y < x % y && x % y <= 0); - -axiom (forall x: int, y: int :: { (x + y) % y } 0 <= x && 0 <= y ==> (x + y) % y == x % y); - -axiom (forall x: int, y: int :: { (y + x) % y } 0 <= x && 0 <= y ==> (y + x) % y == x % y); - -axiom (forall x: int, y: int :: { (x - y) % y } 0 <= x - y && 0 <= y ==> (x - y) % y == x % y); - -axiom (forall a: int, b: int, d: int :: { a % d, b % d } 2 <= d && a % d == b % d && a < b ==> a + d <= b); - -axiom (forall x: int, y: int :: { #and(x, y) } 0 <= x || 0 <= y ==> 0 <= #and(x, y)); - -axiom (forall x: int, y: int :: { #or(x, y) } 0 <= x && 0 <= y ==> 0 <= #or(x, y) && #or(x, y) <= x + y); - -axiom (forall i: int :: { #shl(i, 0) } #shl(i, 0) == i); - -axiom (forall i: int, j: int :: { #shl(i, j) } 1 <= j ==> #shl(i, j) == #shl(i, j - 1) * 2); - -axiom (forall i: int, j: int :: { #shl(i, j) } 0 <= i && i < 32768 && 0 <= j && j <= 16 ==> 0 <= #shl(i, j) && #shl(i, j) <= int#2147483647); - -axiom (forall i: int :: { #shr(i, 0) } #shr(i, 0) == i); - -axiom (forall i: int, j: int :: { #shr(i, j) } 1 <= j ==> #shr(i, j) == #shr(i, j - 1) / 2); - -function #min(int, int) returns (int); - -function #max(int, int) returns (int); - -axiom (forall x: int, y: int :: { #min(x, y) } (#min(x, y) == x || #min(x, y) == y) && #min(x, y) <= x && #min(x, y) <= y); - -axiom (forall x: int, y: int :: { #max(x, y) } (#max(x, y) == x || #max(x, y) == y) && x <= #max(x, y) && y <= #max(x, y)); - -function #System.String.IsInterned$System.String$notnull(Heap, ref) returns (ref); - -function #System.String.Equals$System.String(Heap, ref, ref) returns (bool); - -function #System.String.Equals$System.String$System.String(Heap, ref, ref) returns (bool); - -function ##StringEquals(ref, ref) returns (bool); - -axiom (forall h: Heap, a: ref, b: ref :: { #System.String.Equals$System.String(h, a, b) } #System.String.Equals$System.String(h, a, b) == #System.String.Equals$System.String$System.String(h, a, b)); - -axiom (forall h: Heap, a: ref, b: ref :: { #System.String.Equals$System.String$System.String(h, a, b) } #System.String.Equals$System.String$System.String(h, a, b) == ##StringEquals(a, b) && #System.String.Equals$System.String$System.String(h, a, b) == ##StringEquals(b, a) && (a == b ==> ##StringEquals(a, b))); - -axiom (forall a: ref, b: ref, c: ref :: ##StringEquals(a, b) && ##StringEquals(b, c) ==> ##StringEquals(a, c)); - -axiom (forall h: Heap, a: ref, b: ref :: { #System.String.Equals$System.String$System.String(h, a, b) } a != null && b != null && #System.String.Equals$System.String$System.String(h, a, b) ==> #System.String.IsInterned$System.String$notnull(h, a) == #System.String.IsInterned$System.String$notnull(h, b)); - -const $UnknownRef: ref; - -const unique Bag.a: Field ref; - -const unique Bag.n: Field int; - -const unique Microsoft.Contracts.GuardException: name; - -const unique System.ICloneable: name; - -const unique Microsoft.Contracts.ObjectInvariantException: name; - -const unique System.Exception: name; - -const unique System.Collections.IEnumerable: name; - -const unique System.Collections.IList: name; - -const unique Microsoft.Contracts.ICheckedException: name; - -const unique System.Reflection.MemberInfo: name; - -const unique Bag: name; - -const unique System.Reflection.IReflect: name; - -const unique System.Runtime.InteropServices._MemberInfo: name; - -const unique System.Runtime.InteropServices._Type: name; - -const unique System.Collections.ICollection: name; - -const unique System.Runtime.InteropServices._Exception: name; - -const unique System.Runtime.Serialization.ISerializable: name; - -const unique System.Reflection.ICustomAttributeProvider: name; - -axiom !IsStaticField(Bag.n); - -axiom IncludeInMainFrameCondition(Bag.n); - -axiom $IncludedInModifiesStar(Bag.n); - -axiom DeclType222(Bag.n) == Bag; - -axiom AsRangeField(Bag.n, System.Int32) == Bag.n; - -axiom !IsStaticField(Bag.a); - -axiom IncludeInMainFrameCondition(Bag.a); - -axiom $IncludedInModifiesStar(Bag.a); - -axiom AsRepField(Bag.a, Bag) == Bag.a; - -axiom DeclType222(Bag.a) == Bag; - -axiom AsNonNullRefField(Bag.a, IntArray(System.Int32, 1)) == Bag.a; - -axiom Bag <: Bag; - -axiom $BaseClass(Bag) == System.Object && AsDirectSubClass(Bag, $BaseClass(Bag)) == Bag; - -axiom !$IsImmutable(Bag) && $AsMutable(Bag) == Bag; - -axiom System.Array <: System.Array; - -axiom $BaseClass(System.Array) == System.Object && AsDirectSubClass(System.Array, $BaseClass(System.Array)) == System.Array; - -axiom !$IsImmutable(System.Array) && $AsMutable(System.Array) == System.Array; - -axiom System.ICloneable <: System.ICloneable; - -axiom System.ICloneable <: System.Object; - -axiom $IsMemberlessType(System.ICloneable); - -axiom $AsInterface(System.ICloneable) == System.ICloneable; - -axiom System.Array <: System.ICloneable; - -axiom System.Collections.IList <: System.Collections.IList; - -axiom System.Collections.IList <: System.Object; - -axiom System.Collections.ICollection <: System.Collections.ICollection; - -axiom System.Collections.ICollection <: System.Object; - -axiom System.Collections.IEnumerable <: System.Collections.IEnumerable; - -axiom System.Collections.IEnumerable <: System.Object; - -axiom $IsMemberlessType(System.Collections.IEnumerable); - -axiom $AsInterface(System.Collections.IEnumerable) == System.Collections.IEnumerable; - -axiom System.Collections.ICollection <: System.Collections.IEnumerable; - -axiom $IsMemberlessType(System.Collections.ICollection); - -axiom $AsInterface(System.Collections.ICollection) == System.Collections.ICollection; - -axiom System.Collections.IList <: System.Collections.ICollection; - -axiom System.Collections.IList <: System.Collections.IEnumerable; - -axiom $IsMemberlessType(System.Collections.IList); - -axiom $AsInterface(System.Collections.IList) == System.Collections.IList; - -axiom System.Array <: System.Collections.IList; - -axiom System.Array <: System.Collections.ICollection; - -axiom System.Array <: System.Collections.IEnumerable; - -axiom $IsMemberlessType(System.Array); - -// System.Array object invariant -axiom (forall $oi: ref, $h: Heap :: { $h[$oi, $inv] <: System.Array } IsHeap($h) && $h[$oi, $inv] <: System.Array && $h[$oi, $localinv] != $BaseClass(System.Array) ==> true); - -// Bag object invariant -axiom (forall $oi: ref, $h: Heap :: { $h[$oi, $inv] <: Bag } IsHeap($h) && $h[$oi, $inv] <: Bag && $h[$oi, $localinv] != $BaseClass(Bag) ==> 0 <= $h[$oi, Bag.n] && $h[$oi, Bag.n] <= $Length($h[$oi, Bag.a])); - -procedure Bag.SpecSharp.CheckInvariant$System.Boolean(this: ref where $IsNotNull(this, Bag) && $Heap[this, $allocated], throwException$in: bool where true) returns ($result: bool where true); - // user-declared preconditions - requires ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame]) || $Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame])) && $Heap[this, $inv] == System.Object && $Heap[this, $localinv] == $typeof(this) && (forall $p: ref :: $p != null && $Heap[$p, $allocated] && $Heap[$p, $ownerRef] == this && $Heap[$p, $ownerFrame] == Bag ==> $Heap[$p, $inv] == $typeof($p) && $Heap[$p, $localinv] == $typeof($p)); - free requires $BeingConstructed == null; - free requires $PurityAxiomsCanBeAssumed; - modifies $Heap, $ActivityIndicator; - // newly allocated objects are fully valid - free ensures (forall $o: ref :: { $Heap[$o, $localinv] } { $Heap[$o, $inv] } $o != null && !old($Heap)[$o, $allocated] && $Heap[$o, $allocated] ==> $Heap[$o, $inv] == $typeof($o) && $Heap[$o, $localinv] == $typeof($o)); - // first consistent owner unchanged if its exposeVersion is - free ensures (forall $o: ref :: { $Heap[$o, $FirstConsistentOwner] } old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] ==> old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner]); - // frame condition - ensures (forall $o: ref, $f: Field a :: { $Heap[$o, $f] } IncludeInMainFrameCondition($f) && $o != null && old($Heap)[$o, $allocated] && (old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame]) || old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])) && old($o != this || !($typeof(this) <: DeclType222($f)) || !$IncludedInModifiesStar($f)) && old(true) ==> old($Heap)[$o, $f] == $Heap[$o, $f]); - free ensures $HeapSucc(old($Heap), $Heap); - // inv/localinv change only in blocks - free ensures (forall $o: ref :: { $Heap[$o, $localinv] } { $Heap[$o, $inv] } old($Heap)[$o, $allocated] ==> old($Heap)[$o, $inv] == $Heap[$o, $inv] && old($Heap)[$o, $localinv] == $Heap[$o, $localinv]); - free ensures (forall $o: ref :: { $Heap[$o, $allocated] } old($Heap)[$o, $allocated] ==> $Heap[$o, $allocated]) && (forall $ot: ref :: { $Heap[$ot, $ownerFrame] } { $Heap[$ot, $ownerRef] } old($Heap)[$ot, $allocated] && old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder ==> $Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef] && $Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]) && old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]; - free ensures (forall $o: ref :: { $Heap[$o, $sharingMode] } old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]); - - - -implementation Bag.SpecSharp.CheckInvariant$System.Boolean(this: ref, throwException$in: bool) returns ($result: bool) -{ - var throwException: bool where true, stack0i: int, stack1i: int, stack0b: bool, stack1o: ref, return.value: bool where true, stack50000o: ref, stack0o: ref, SS$Display.Return.Local: bool where true; - - entry: - throwException := throwException$in; - goto block2380; - - block2380: - goto block2482; - - block2482: - // ----- nop - // ----- load constant 0 - stack0i := 0; - // ----- load field - assert this != null; - stack1i := $Heap[this, Bag.n]; - // ----- binary operator - // ----- branch - goto true2482to2550, false2482to2414; - - true2482to2550: - assume stack0i > stack1i; - goto block2550; - - false2482to2414: - assume stack0i <= stack1i; - goto block2414; - - block2550: - // ----- copy - stack0b := throwException; - // ----- unary operator - // ----- branch - goto true2550to2584, false2550to2601; - - block2414: - // ----- load field - assert this != null; - stack0i := $Heap[this, Bag.n]; - // ----- load field - assert this != null; - stack1o := $Heap[this, Bag.a]; - // ----- unary operator - assert stack1o != null; - stack1i := $Length(stack1o); - // ----- unary operator - stack1i := $IntToInt(stack1i, System.UIntPtr, System.Int32); - // ----- binary operator - // ----- branch - goto true2414to2550, false2414to2465; - - true2414to2550: - assume stack0i > stack1i; - goto block2550; - - false2414to2465: - assume stack0i <= stack1i; - goto block2465; - - block2465: - // ----- branch - goto block2448; - - true2550to2584: - assume !stack0b; - goto block2584; - - false2550to2601: - assume stack0b; - goto block2601; - - block2584: - // ----- load constant 0 - return.value := false; - // ----- branch - goto block2567; - - block2601: - assume false; - // ----- new object - havoc stack50000o; - assume $Heap[stack50000o, $allocated] == false && stack50000o != null && $typeof(stack50000o) == Microsoft.Contracts.ObjectInvariantException; - assume $Heap[stack50000o, $ownerRef] == stack50000o && $Heap[stack50000o, $ownerFrame] == $PeerGroupPlaceholder; - // ----- call - assert stack50000o != null; - call Microsoft.Contracts.ObjectInvariantException..ctor(stack50000o); - // ----- copy - stack0o := stack50000o; - // ----- throw - assert stack0o != null; - assume false; - return; - - block2448: - // ----- load constant 1 - return.value := true; - // ----- branch - goto block2567; - - block2567: - // ----- copy - SS$Display.Return.Local := return.value; - // ----- copy - stack0b := return.value; - // ----- return - $result := stack0b; - return; -} - - - -axiom Microsoft.Contracts.ObjectInvariantException <: Microsoft.Contracts.ObjectInvariantException; - -axiom Microsoft.Contracts.GuardException <: Microsoft.Contracts.GuardException; - -axiom System.Exception <: System.Exception; - -axiom $BaseClass(System.Exception) == System.Object && AsDirectSubClass(System.Exception, $BaseClass(System.Exception)) == System.Exception; - -axiom !$IsImmutable(System.Exception) && $AsMutable(System.Exception) == System.Exception; - -axiom System.Runtime.Serialization.ISerializable <: System.Runtime.Serialization.ISerializable; - -axiom System.Runtime.Serialization.ISerializable <: System.Object; - -axiom $IsMemberlessType(System.Runtime.Serialization.ISerializable); - -axiom $AsInterface(System.Runtime.Serialization.ISerializable) == System.Runtime.Serialization.ISerializable; - -axiom System.Exception <: System.Runtime.Serialization.ISerializable; - -axiom System.Runtime.InteropServices._Exception <: System.Runtime.InteropServices._Exception; - -axiom System.Runtime.InteropServices._Exception <: System.Object; - -axiom $IsMemberlessType(System.Runtime.InteropServices._Exception); - -axiom $AsInterface(System.Runtime.InteropServices._Exception) == System.Runtime.InteropServices._Exception; - -axiom System.Exception <: System.Runtime.InteropServices._Exception; - -// System.Exception object invariant -axiom (forall $oi: ref, $h: Heap :: { $h[$oi, $inv] <: System.Exception } IsHeap($h) && $h[$oi, $inv] <: System.Exception && $h[$oi, $localinv] != $BaseClass(System.Exception) ==> true); - -axiom $BaseClass(Microsoft.Contracts.GuardException) == System.Exception && AsDirectSubClass(Microsoft.Contracts.GuardException, $BaseClass(Microsoft.Contracts.GuardException)) == Microsoft.Contracts.GuardException; - -axiom !$IsImmutable(Microsoft.Contracts.GuardException) && $AsMutable(Microsoft.Contracts.GuardException) == Microsoft.Contracts.GuardException; - -// Microsoft.Contracts.GuardException object invariant -axiom (forall $oi: ref, $h: Heap :: { $h[$oi, $inv] <: Microsoft.Contracts.GuardException } IsHeap($h) && $h[$oi, $inv] <: Microsoft.Contracts.GuardException && $h[$oi, $localinv] != $BaseClass(Microsoft.Contracts.GuardException) ==> true); - -axiom $BaseClass(Microsoft.Contracts.ObjectInvariantException) == Microsoft.Contracts.GuardException && AsDirectSubClass(Microsoft.Contracts.ObjectInvariantException, $BaseClass(Microsoft.Contracts.ObjectInvariantException)) == Microsoft.Contracts.ObjectInvariantException; - -axiom !$IsImmutable(Microsoft.Contracts.ObjectInvariantException) && $AsMutable(Microsoft.Contracts.ObjectInvariantException) == Microsoft.Contracts.ObjectInvariantException; - -// Microsoft.Contracts.ObjectInvariantException object invariant -axiom (forall $oi: ref, $h: Heap :: { $h[$oi, $inv] <: Microsoft.Contracts.ObjectInvariantException } IsHeap($h) && $h[$oi, $inv] <: Microsoft.Contracts.ObjectInvariantException && $h[$oi, $localinv] != $BaseClass(Microsoft.Contracts.ObjectInvariantException) ==> true); - -procedure Microsoft.Contracts.ObjectInvariantException..ctor(this: ref where $IsNotNull(this, Microsoft.Contracts.ObjectInvariantException) && $Heap[this, $allocated]); - // object is fully unpacked: this.inv == Object - free requires ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame]) || $Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame])) && $Heap[this, $inv] == System.Object && $Heap[this, $localinv] == $typeof(this); - // nothing is owned by [this,*] and 'this' is alone in its own peer group - free requires (forall $o: ref :: $o != this ==> $Heap[$o, $ownerRef] != this) && $Heap[this, $ownerRef] == this && $Heap[this, $ownerFrame] == $PeerGroupPlaceholder; - free requires $BeingConstructed == this; - free requires $PurityAxiomsCanBeAssumed; - modifies $Heap, $ActivityIndicator; - // target object is allocated upon return - free ensures $Heap[this, $allocated]; - // target object is additively exposable for Microsoft.Contracts.ObjectInvariantException - ensures ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame]) || $Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame])) && $Heap[this, $inv] == Microsoft.Contracts.ObjectInvariantException && $Heap[this, $localinv] == $typeof(this); - ensures $Heap[this, $ownerRef] == old($Heap)[this, $ownerRef] && $Heap[this, $ownerFrame] == old($Heap)[this, $ownerFrame]; - ensures $Heap[this, $sharingMode] == $SharingMode_Unshared; - // newly allocated objects are fully valid - free ensures (forall $o: ref :: { $Heap[$o, $localinv] } { $Heap[$o, $inv] } $o != null && !old($Heap)[$o, $allocated] && $Heap[$o, $allocated] ==> $Heap[$o, $inv] == $typeof($o) && $Heap[$o, $localinv] == $typeof($o)); - // first consistent owner unchanged if its exposeVersion is - free ensures (forall $o: ref :: { $Heap[$o, $FirstConsistentOwner] } old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] ==> old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner]); - // frame condition - ensures (forall $o: ref, $f: Field a :: { $Heap[$o, $f] } IncludeInMainFrameCondition($f) && $o != null && old($Heap)[$o, $allocated] && (old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame]) || old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])) && ($o != this || !(Microsoft.Contracts.ObjectInvariantException <: DeclType222($f))) && old(true) && old(true) ==> old($Heap)[$o, $f] == $Heap[$o, $f]); - free ensures $HeapSucc(old($Heap), $Heap); - // inv/localinv change only in blocks - free ensures (forall $o: ref :: { $Heap[$o, $localinv] } { $Heap[$o, $inv] } old($Heap)[$o, $allocated] && $o != this ==> old($Heap)[$o, $inv] == $Heap[$o, $inv] && old($Heap)[$o, $localinv] == $Heap[$o, $localinv]); - free ensures (forall $o: ref :: { $Heap[$o, $allocated] } old($Heap)[$o, $allocated] ==> $Heap[$o, $allocated]) && (forall $ot: ref :: { $Heap[$ot, $ownerFrame] } { $Heap[$ot, $ownerRef] } old($Heap)[$ot, $allocated] && old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder ==> $Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef] && $Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]) && old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]; - free ensures (forall $o: ref :: { $Heap[$o, $sharingMode] } $o == this || old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]); - - - -procedure Bag..ctor$System.Int32.array$notnull(this: ref where $IsNotNull(this, Bag) && $Heap[this, $allocated], initialElements$in: ref where $IsNotNull(initialElements$in, IntArray(System.Int32, 1)) && $Heap[initialElements$in, $allocated]); - // object is fully unpacked: this.inv == Object - free requires ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame]) || $Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame])) && $Heap[this, $inv] == System.Object && $Heap[this, $localinv] == $typeof(this); - // initialElements is peer consistent - requires (forall $pc: ref :: { $typeof($pc) } { $Heap[$pc, $localinv] } { $Heap[$pc, $inv] } { $Heap[$pc, $ownerFrame] } { $Heap[$pc, $ownerRef] } $pc != null && $Heap[$pc, $allocated] && $Heap[$pc, $ownerRef] == $Heap[initialElements$in, $ownerRef] && $Heap[$pc, $ownerFrame] == $Heap[initialElements$in, $ownerFrame] ==> $Heap[$pc, $inv] == $typeof($pc) && $Heap[$pc, $localinv] == $typeof($pc)); - // initialElements is peer consistent (owner must not be valid) - requires $Heap[initialElements$in, $ownerFrame] == $PeerGroupPlaceholder || !($Heap[$Heap[initialElements$in, $ownerRef], $inv] <: $Heap[initialElements$in, $ownerFrame]) || $Heap[$Heap[initialElements$in, $ownerRef], $localinv] == $BaseClass($Heap[initialElements$in, $ownerFrame]); - // nothing is owned by [this,*] and 'this' is alone in its own peer group - free requires (forall $o: ref :: $o != this ==> $Heap[$o, $ownerRef] != this) && $Heap[this, $ownerRef] == this && $Heap[this, $ownerFrame] == $PeerGroupPlaceholder; - free requires $BeingConstructed == this; - free requires $PurityAxiomsCanBeAssumed; - modifies $Heap, $ActivityIndicator; - // target object is allocated upon return - free ensures $Heap[this, $allocated]; - // target object is additively exposable for Bag - ensures ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame]) || $Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame])) && $Heap[this, $inv] == Bag && $Heap[this, $localinv] == $typeof(this); - ensures $Heap[this, $ownerRef] == old($Heap)[this, $ownerRef] && $Heap[this, $ownerFrame] == old($Heap)[this, $ownerFrame]; - ensures $Heap[this, $sharingMode] == $SharingMode_Unshared; - // newly allocated objects are fully valid - free ensures (forall $o: ref :: { $Heap[$o, $localinv] } { $Heap[$o, $inv] } $o != null && !old($Heap)[$o, $allocated] && $Heap[$o, $allocated] ==> $Heap[$o, $inv] == $typeof($o) && $Heap[$o, $localinv] == $typeof($o)); - // first consistent owner unchanged if its exposeVersion is - free ensures (forall $o: ref :: { $Heap[$o, $FirstConsistentOwner] } old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] ==> old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner]); - // frame condition - ensures (forall $o: ref, $f: Field a :: { $Heap[$o, $f] } IncludeInMainFrameCondition($f) && $o != null && old($Heap)[$o, $allocated] && (old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame]) || old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])) && ($o != this || !(Bag <: DeclType222($f))) && old(true) && old(true) ==> old($Heap)[$o, $f] == $Heap[$o, $f]); - free ensures $HeapSucc(old($Heap), $Heap); - // inv/localinv change only in blocks - free ensures (forall $o: ref :: { $Heap[$o, $localinv] } { $Heap[$o, $inv] } old($Heap)[$o, $allocated] && $o != this ==> old($Heap)[$o, $inv] == $Heap[$o, $inv] && old($Heap)[$o, $localinv] == $Heap[$o, $localinv]); - free ensures (forall $o: ref :: { $Heap[$o, $allocated] } old($Heap)[$o, $allocated] ==> $Heap[$o, $allocated]) && (forall $ot: ref :: { $Heap[$ot, $ownerFrame] } { $Heap[$ot, $ownerRef] } old($Heap)[$ot, $allocated] && old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder ==> $Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef] && $Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]) && old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]; - free ensures (forall $o: ref :: { $Heap[$o, $sharingMode] } $o == this || old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]); - - - -implementation Bag..ctor$System.Int32.array$notnull(this: ref, initialElements$in: ref) -{ - var initialElements: ref where $IsNotNull(initialElements, IntArray(System.Int32, 1)) && $Heap[initialElements, $allocated], stack0o: ref, stack0i: int, temp0: exposeVersionType, temp1: ref, temp2: exposeVersionType, stack1i: int, temp3: ref; - - entry: - initialElements := initialElements$in; - assume $Heap[this, Bag.n] == 0; - goto block3332; - - block3332: - goto block3468; - - block3468: - // ----- nop - // ----- copy ----- AddMethod.ssc(13,5) - stack0o := initialElements; - // ----- unary operator ----- AddMethod.ssc(13,5) - assert stack0o != null; - stack0i := $Length(stack0o); - // ----- unary operator ----- AddMethod.ssc(13,5) - stack0i := $IntToInt(stack0i, System.UIntPtr, System.Int32); - // ----- store field ----- AddMethod.ssc(13,5) - assert this != null; - assert $Heap[this, $ownerFrame] == $PeerGroupPlaceholder || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame]) || $Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]); - havoc temp0; - $Heap[this, $exposeVersion] := temp0; - $Heap[this, Bag.n] := stack0i; - assert !($Heap[this, $inv] <: Bag && $Heap[this, $localinv] != $BaseClass(Bag)) || 0 <= $Heap[this, Bag.n]; - assert !($Heap[this, $inv] <: Bag && $Heap[this, $localinv] != $BaseClass(Bag)) || $Heap[this, Bag.n] <= $Length($Heap[this, Bag.a]); - assume IsHeap($Heap); - // ----- copy ----- AddMethod.ssc(14,5) - stack0o := initialElements; - // ----- unary operator ----- AddMethod.ssc(14,5) - assert stack0o != null; - stack0i := $Length(stack0o); - // ----- unary operator ----- AddMethod.ssc(14,5) - stack0i := $IntToInt(stack0i, System.UIntPtr, System.Int32); - // ----- new array ----- AddMethod.ssc(14,5) - assert 0 <= stack0i; - havoc temp1; - assume $Heap[temp1, $allocated] == false && $Length(temp1) == stack0i; - assume $Heap[$ElementProxy(temp1, -1), $allocated] == false && $ElementProxy(temp1, -1) != temp1 && $ElementProxy(temp1, -1) != null; - assume temp1 != null; - assume $typeof(temp1) == IntArray(System.Int32, 1); - assume $Heap[temp1, $ownerRef] == temp1 && $Heap[temp1, $ownerFrame] == $PeerGroupPlaceholder; - assume $Heap[$ElementProxy(temp1, -1), $ownerRef] == $ElementProxy(temp1, -1) && $Heap[$ElementProxy(temp1, -1), $ownerFrame] == $PeerGroupPlaceholder; - assume $Heap[temp1, $inv] == $typeof(temp1) && $Heap[temp1, $localinv] == $typeof(temp1); - assume (forall $i: int :: IntArrayGet($Heap[temp1, $elements], $i) == 0); - $Heap[temp1, $allocated] := true; - call System.Object..ctor($ElementProxy(temp1, -1)); - stack0o := temp1; - assume IsHeap($Heap); - // ----- store field ----- AddMethod.ssc(14,5) - assert this != null; - assert $Heap[this, $ownerFrame] == $PeerGroupPlaceholder || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame]) || $Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]); - assert ($Heap[stack0o, $ownerRef] == this && $Heap[stack0o, $ownerFrame] == Bag) || $Heap[stack0o, $ownerFrame] == $PeerGroupPlaceholder; - assert $Heap[stack0o, $ownerFrame] == $PeerGroupPlaceholder && $Heap[this, $inv] <: Bag && $Heap[this, $localinv] != $BaseClass(Bag) ==> (forall $pc: ref :: { $typeof($pc) } { $Heap[$pc, $localinv] } { $Heap[$pc, $inv] } { $Heap[$pc, $ownerFrame] } { $Heap[$pc, $ownerRef] } $pc != null && $Heap[$pc, $allocated] && $Heap[$pc, $ownerRef] == $Heap[stack0o, $ownerRef] && $Heap[$pc, $ownerFrame] == $Heap[stack0o, $ownerFrame] ==> $Heap[$pc, $inv] == $typeof($pc) && $Heap[$pc, $localinv] == $typeof($pc)); - assert $Heap[stack0o, $ownerFrame] == $PeerGroupPlaceholder && $Heap[this, $inv] <: Bag && $Heap[this, $localinv] != $BaseClass(Bag) ==> $Heap[this, $ownerRef] != $Heap[stack0o, $ownerRef] || $Heap[this, $ownerFrame] != $Heap[stack0o, $ownerFrame]; - call $UpdateOwnersForRep(this, Bag, stack0o); - havoc temp2; - $Heap[this, $exposeVersion] := temp2; - $Heap[this, Bag.a] := stack0o; - assert !($Heap[this, $inv] <: Bag && $Heap[this, $localinv] != $BaseClass(Bag)) || 0 <= $Heap[this, Bag.n]; - assert !($Heap[this, $inv] <: Bag && $Heap[this, $localinv] != $BaseClass(Bag)) || $Heap[this, Bag.n] <= $Length($Heap[this, Bag.a]); - assume IsHeap($Heap); - // ----- call ----- AddMethod.ssc(15,5) - assert this != null; - call System.Object..ctor(this); - $Heap[this, $NonNullFieldsAreInitialized] := true; - assume IsHeap($Heap); - goto block3417; - - block3417: - // ----- load field ----- AddMethod.ssc(16,5) - assert this != null; - stack0o := $Heap[this, Bag.a]; - // ----- load constant 0 ----- AddMethod.ssc(16,5) - stack1i := 0; - // ----- call ----- AddMethod.ssc(16,5) - assert initialElements != null; - call System.Array.CopyTo$System.Array$notnull$System.Int32$.Virtual.$(initialElements, stack0o, stack1i); - // ----- FrameGuard processing ----- AddMethod.ssc(17,3) - temp3 := this; - // ----- classic pack ----- AddMethod.ssc(17,3) - assert temp3 != null; - assert $Heap[temp3, $inv] == System.Object && $Heap[temp3, $localinv] == $typeof(temp3); - assert 0 <= $Heap[temp3, Bag.n]; - assert $Heap[temp3, Bag.n] <= $Length($Heap[temp3, Bag.a]); - assert (forall $p: ref :: $p != null && $Heap[$p, $allocated] && $Heap[$p, $ownerRef] == temp3 && $Heap[$p, $ownerFrame] == Bag ==> $Heap[$p, $inv] == $typeof($p) && $Heap[$p, $localinv] == $typeof($p)); - $Heap[temp3, $inv] := Bag; - assume IsHeap($Heap); - // ----- return - return; -} - - - -procedure System.Object..ctor(this: ref where $IsNotNull(this, System.Object) && $Heap[this, $allocated]); - // object is fully unpacked: this.inv == Object - free requires ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame]) || $Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame])) && $Heap[this, $inv] == System.Object && $Heap[this, $localinv] == $typeof(this); - // nothing is owned by [this,*] and 'this' is alone in its own peer group - free requires (forall $o: ref :: $o != this ==> $Heap[$o, $ownerRef] != this) && $Heap[this, $ownerRef] == this && $Heap[this, $ownerFrame] == $PeerGroupPlaceholder; - free requires $BeingConstructed == this; - free requires $PurityAxiomsCanBeAssumed; - modifies $Heap, $ActivityIndicator; - // target object is allocated upon return - free ensures $Heap[this, $allocated]; - // target object is additively exposable for System.Object - ensures ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame]) || $Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame])) && $Heap[this, $inv] == System.Object && $Heap[this, $localinv] == $typeof(this); - ensures $Heap[this, $ownerRef] == old($Heap)[this, $ownerRef] && $Heap[this, $ownerFrame] == old($Heap)[this, $ownerFrame]; - ensures $Heap[this, $sharingMode] == $SharingMode_Unshared; - // newly allocated objects are fully valid - free ensures (forall $o: ref :: { $Heap[$o, $localinv] } { $Heap[$o, $inv] } $o != null && !old($Heap)[$o, $allocated] && $Heap[$o, $allocated] ==> $Heap[$o, $inv] == $typeof($o) && $Heap[$o, $localinv] == $typeof($o)); - // first consistent owner unchanged if its exposeVersion is - free ensures (forall $o: ref :: { $Heap[$o, $FirstConsistentOwner] } old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] ==> old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner]); - // frame condition - ensures (forall $o: ref, $f: Field a :: { $Heap[$o, $f] } IncludeInMainFrameCondition($f) && $o != null && old($Heap)[$o, $allocated] && (old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame]) || old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])) && ($o != this || !(System.Object <: DeclType222($f))) && old(true) && old(true) ==> old($Heap)[$o, $f] == $Heap[$o, $f]); - free ensures $HeapSucc(old($Heap), $Heap); - // inv/localinv change only in blocks - free ensures (forall $o: ref :: { $Heap[$o, $localinv] } { $Heap[$o, $inv] } old($Heap)[$o, $allocated] && $o != this ==> old($Heap)[$o, $inv] == $Heap[$o, $inv] && old($Heap)[$o, $localinv] == $Heap[$o, $localinv]); - free ensures (forall $o: ref :: { $Heap[$o, $allocated] } old($Heap)[$o, $allocated] ==> $Heap[$o, $allocated]) && (forall $ot: ref :: { $Heap[$ot, $ownerFrame] } { $Heap[$ot, $ownerRef] } old($Heap)[$ot, $allocated] && old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder ==> $Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef] && $Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]) && old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]; - free ensures (forall $o: ref :: { $Heap[$o, $sharingMode] } $o == this || old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]); - - - -procedure System.Array.CopyTo$System.Array$notnull$System.Int32$.Virtual.$(this: ref where $IsNotNull(this, System.Array) && $Heap[this, $allocated], array$in: ref where $IsNotNull(array$in, System.Array) && $Heap[array$in, $allocated], index$in: int where InRange(index$in, System.Int32)); - // user-declared preconditions - requires array$in != null; - requires $LBound(array$in, 0) <= index$in; - requires $Rank(this) == 1; - requires $Rank(array$in) == 1; - requires $Length(this) <= $UBound(array$in, 0) + 1 - index$in; - // target object is peer consistent - requires (forall $pc: ref :: { $typeof($pc) } { $Heap[$pc, $localinv] } { $Heap[$pc, $inv] } { $Heap[$pc, $ownerFrame] } { $Heap[$pc, $ownerRef] } $pc != null && $Heap[$pc, $allocated] && $Heap[$pc, $ownerRef] == $Heap[this, $ownerRef] && $Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame] ==> $Heap[$pc, $inv] == $typeof($pc) && $Heap[$pc, $localinv] == $typeof($pc)); - // target object is peer consistent (owner must not be valid) - requires $Heap[this, $ownerFrame] == $PeerGroupPlaceholder || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame]) || $Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]); - // array is peer consistent - requires (forall $pc: ref :: { $typeof($pc) } { $Heap[$pc, $localinv] } { $Heap[$pc, $inv] } { $Heap[$pc, $ownerFrame] } { $Heap[$pc, $ownerRef] } $pc != null && $Heap[$pc, $allocated] && $Heap[$pc, $ownerRef] == $Heap[array$in, $ownerRef] && $Heap[$pc, $ownerFrame] == $Heap[array$in, $ownerFrame] ==> $Heap[$pc, $inv] == $typeof($pc) && $Heap[$pc, $localinv] == $typeof($pc)); - // array is peer consistent (owner must not be valid) - requires $Heap[array$in, $ownerFrame] == $PeerGroupPlaceholder || !($Heap[$Heap[array$in, $ownerRef], $inv] <: $Heap[array$in, $ownerFrame]) || $Heap[$Heap[array$in, $ownerRef], $localinv] == $BaseClass($Heap[array$in, $ownerFrame]); - free requires $BeingConstructed == null; - free requires $PurityAxiomsCanBeAssumed; - modifies $Heap, $ActivityIndicator; - // hard-coded postcondition - ensures (forall $k: int :: { ValueArrayGet($Heap[array$in, $elements], $k) } (index$in <= $k && $k < index$in + $Length(this) ==> old(ValueArrayGet($Heap[this, $elements], $k + 0 - index$in)) == ValueArrayGet($Heap[array$in, $elements], $k)) && (!(index$in <= $k && $k < index$in + $Length(this)) ==> old(ValueArrayGet($Heap[array$in, $elements], $k)) == ValueArrayGet($Heap[array$in, $elements], $k))); - ensures (forall $k: int :: { IntArrayGet($Heap[array$in, $elements], $k) } (index$in <= $k && $k < index$in + $Length(this) ==> old(IntArrayGet($Heap[this, $elements], $k + 0 - index$in)) == IntArrayGet($Heap[array$in, $elements], $k)) && (!(index$in <= $k && $k < index$in + $Length(this)) ==> old(IntArrayGet($Heap[array$in, $elements], $k)) == IntArrayGet($Heap[array$in, $elements], $k))); - ensures (forall $k: int :: { RefArrayGet($Heap[array$in, $elements], $k) } (index$in <= $k && $k < index$in + $Length(this) ==> old(RefArrayGet($Heap[this, $elements], $k + 0 - index$in)) == RefArrayGet($Heap[array$in, $elements], $k)) && (!(index$in <= $k && $k < index$in + $Length(this)) ==> old(RefArrayGet($Heap[array$in, $elements], $k)) == RefArrayGet($Heap[array$in, $elements], $k))); - // newly allocated objects are fully valid - free ensures (forall $o: ref :: { $Heap[$o, $localinv] } { $Heap[$o, $inv] } $o != null && !old($Heap)[$o, $allocated] && $Heap[$o, $allocated] ==> $Heap[$o, $inv] == $typeof($o) && $Heap[$o, $localinv] == $typeof($o)); - // first consistent owner unchanged if its exposeVersion is - free ensures (forall $o: ref :: { $Heap[$o, $FirstConsistentOwner] } old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] ==> old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner]); - // frame condition - ensures (forall $o: ref, $f: Field a :: { $Heap[$o, $f] } IncludeInMainFrameCondition($f) && $o != null && old($Heap)[$o, $allocated] && (old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame]) || old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])) && old($o != array$in || !($typeof(array$in) <: DeclType222($f)) || !$IncludedInModifiesStar($f)) && old($o != array$in || $f != $exposeVersion) ==> old($Heap)[$o, $f] == $Heap[$o, $f]); - free ensures $HeapSucc(old($Heap), $Heap); - // inv/localinv change only in blocks - free ensures (forall $o: ref :: { $Heap[$o, $localinv] } { $Heap[$o, $inv] } old($Heap)[$o, $allocated] ==> old($Heap)[$o, $inv] == $Heap[$o, $inv] && old($Heap)[$o, $localinv] == $Heap[$o, $localinv]); - free ensures (forall $o: ref :: { $Heap[$o, $allocated] } old($Heap)[$o, $allocated] ==> $Heap[$o, $allocated]) && (forall $ot: ref :: { $Heap[$ot, $ownerFrame] } { $Heap[$ot, $ownerRef] } old($Heap)[$ot, $allocated] && old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder ==> $Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef] && $Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]) && old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]; - free ensures (forall $o: ref :: { $Heap[$o, $sharingMode] } old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]); - - - -procedure Bag.Add$System.Int32(this: ref where $IsNotNull(this, Bag) && $Heap[this, $allocated], x$in: int where InRange(x$in, System.Int32)); - // target object is peer consistent - requires (forall $pc: ref :: { $typeof($pc) } { $Heap[$pc, $localinv] } { $Heap[$pc, $inv] } { $Heap[$pc, $ownerFrame] } { $Heap[$pc, $ownerRef] } $pc != null && $Heap[$pc, $allocated] && $Heap[$pc, $ownerRef] == $Heap[this, $ownerRef] && $Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame] ==> $Heap[$pc, $inv] == $typeof($pc) && $Heap[$pc, $localinv] == $typeof($pc)); - // target object is peer consistent (owner must not be valid) - requires $Heap[this, $ownerFrame] == $PeerGroupPlaceholder || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame]) || $Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]); - free requires $BeingConstructed == null; - free requires $PurityAxiomsCanBeAssumed; - modifies $Heap, $ActivityIndicator; - // newly allocated objects are fully valid - free ensures (forall $o: ref :: { $Heap[$o, $localinv] } { $Heap[$o, $inv] } $o != null && !old($Heap)[$o, $allocated] && $Heap[$o, $allocated] ==> $Heap[$o, $inv] == $typeof($o) && $Heap[$o, $localinv] == $typeof($o)); - // first consistent owner unchanged if its exposeVersion is - free ensures (forall $o: ref :: { $Heap[$o, $FirstConsistentOwner] } old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] ==> old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner]); - // frame condition - ensures (forall $o: ref, $f: Field a :: { $Heap[$o, $f] } IncludeInMainFrameCondition($f) && $o != null && old($Heap)[$o, $allocated] && (old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame]) || old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])) && old($o != this || !($typeof(this) <: DeclType222($f)) || !$IncludedInModifiesStar($f)) && old($o != this || $f != $exposeVersion) ==> old($Heap)[$o, $f] == $Heap[$o, $f]); - free ensures $HeapSucc(old($Heap), $Heap); - // inv/localinv change only in blocks - free ensures (forall $o: ref :: { $Heap[$o, $localinv] } { $Heap[$o, $inv] } old($Heap)[$o, $allocated] ==> old($Heap)[$o, $inv] == $Heap[$o, $inv] && old($Heap)[$o, $localinv] == $Heap[$o, $localinv]); - free ensures (forall $o: ref :: { $Heap[$o, $allocated] } old($Heap)[$o, $allocated] ==> $Heap[$o, $allocated]) && (forall $ot: ref :: { $Heap[$ot, $ownerFrame] } { $Heap[$ot, $ownerRef] } old($Heap)[$ot, $allocated] && old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder ==> $Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef] && $Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]) && old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]; - free ensures (forall $o: ref :: { $Heap[$o, $sharingMode] } old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]); - - - -implementation Bag.Add$System.Int32(this: ref, x$in: int) -{ - var x: int where InRange(x, System.Int32), temp0: ref, stack1s: struct, stack1o: ref, temp1: exposeVersionType, local2: ref where $Is(local2, System.Exception) && $Heap[local2, $allocated], stack0i: int, stack1i: int, stack0b: bool, b: ref where $Is(b, IntArray(System.Int32, 1)) && $Heap[b, $allocated], temp2: ref, stack0o: ref, stack2o: ref, stack3i: int, stack4o: ref, stack4i: int, temp3: exposeVersionType, local4: int where InRange(local4, System.Int32), temp4: exposeVersionType, stack0s: struct; - - entry: - x := x$in; - goto block4335; - - block4335: - goto block4488; - - block4488: - // ----- nop - // ----- FrameGuard processing ----- AddMethod.ssc(22,13) - temp0 := this; - // ----- load token ----- AddMethod.ssc(22,13) - havoc stack1s; - assume $IsTokenForType(stack1s, Bag); - // ----- statically resolved GetTypeFromHandle call ----- AddMethod.ssc(22,13) - stack1o := TypeObject(Bag); - // ----- local unpack ----- AddMethod.ssc(22,13) - assert temp0 != null; - assert ($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame]) || $Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame])) && $Heap[temp0, $inv] <: Bag && $Heap[temp0, $localinv] == $typeof(temp0); - $Heap[temp0, $localinv] := System.Object; - havoc temp1; - $Heap[temp0, $exposeVersion] := temp1; - assume IsHeap($Heap); - local2 := null; - goto block4505; - - block4505: - // ----- load field ----- AddMethod.ssc(24,7) - assert this != null; - stack0i := $Heap[this, Bag.n]; - // ----- load field ----- AddMethod.ssc(24,7) - assert this != null; - stack1o := $Heap[this, Bag.a]; - // ----- unary operator ----- AddMethod.ssc(24,7) - assert stack1o != null; - stack1i := $Length(stack1o); - // ----- unary operator ----- AddMethod.ssc(24,7) - stack1i := $IntToInt(stack1i, System.UIntPtr, System.Int32); - // ----- binary operator ----- AddMethod.ssc(24,7) - // ----- branch ----- AddMethod.ssc(24,7) - goto true4505to4539, false4505to4522; - - true4505to4539: - assume stack0i != stack1i; - goto block4539; - - false4505to4522: - assume stack0i == stack1i; - goto block4522; - - block4539: - // ----- load field ----- AddMethod.ssc(30,7) - assert this != null; - stack0o := $Heap[this, Bag.a]; - // ----- load field ----- AddMethod.ssc(30,7) - assert this != null; - stack1i := $Heap[this, Bag.n]; - // ----- store element ----- AddMethod.ssc(30,7) - assert stack0o != null; - assert 0 <= stack1i; - assert stack1i < $Length(stack0o); - assert $Heap[stack0o, $ownerFrame] == $PeerGroupPlaceholder || !($Heap[$Heap[stack0o, $ownerRef], $inv] <: $Heap[stack0o, $ownerFrame]) || $Heap[$Heap[stack0o, $ownerRef], $localinv] == $BaseClass($Heap[stack0o, $ownerFrame]); - $Heap[stack0o, $elements] := IntArraySet($Heap[stack0o, $elements], stack1i, x); - assume IsHeap($Heap); - // ----- load field ----- AddMethod.ssc(31,7) - assert this != null; - local4 := $Heap[this, Bag.n]; - // ----- load constant 1 ----- AddMethod.ssc(31,7) - stack0i := 1; - // ----- binary operator ----- AddMethod.ssc(31,7) - stack0i := local4 + stack0i; - // ----- store field ----- AddMethod.ssc(31,7) - assert this != null; - assert $Heap[this, $ownerFrame] == $PeerGroupPlaceholder || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame]) || $Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]); - havoc temp4; - $Heap[this, $exposeVersion] := temp4; - $Heap[this, Bag.n] := stack0i; - assert !($Heap[this, $inv] <: Bag && $Heap[this, $localinv] != $BaseClass(Bag)) || 0 <= $Heap[this, Bag.n]; - assert !($Heap[this, $inv] <: Bag && $Heap[this, $localinv] != $BaseClass(Bag)) || $Heap[this, Bag.n] <= $Length($Heap[this, Bag.a]); - assume IsHeap($Heap); - // ----- copy - stack0i := local4; - // ----- branch - goto block4658; - - block4522: - // ----- load constant 2 ----- AddMethod.ssc(26,15) - stack0i := 2; - // ----- load field ----- AddMethod.ssc(26,15) - assert this != null; - stack1o := $Heap[this, Bag.a]; - // ----- unary operator ----- AddMethod.ssc(26,15) - assert stack1o != null; - stack1i := $Length(stack1o); - // ----- unary operator ----- AddMethod.ssc(26,15) - stack1i := $IntToInt(stack1i, System.UIntPtr, System.Int32); - // ----- binary operator ----- AddMethod.ssc(26,15) - stack0i := stack0i * stack1i; - // ----- load constant 1 ----- AddMethod.ssc(26,15) - stack1i := 1; - // ----- binary operator ----- AddMethod.ssc(26,15) - stack0i := stack0i + stack1i; - // ----- new array ----- AddMethod.ssc(26,15) - assert 0 <= stack0i; - havoc temp2; - assume $Heap[temp2, $allocated] == false && $Length(temp2) == stack0i; - assume $Heap[$ElementProxy(temp2, -1), $allocated] == false && $ElementProxy(temp2, -1) != temp2 && $ElementProxy(temp2, -1) != null; - assume temp2 != null; - assume $typeof(temp2) == IntArray(System.Int32, 1); - assume $Heap[temp2, $ownerRef] == temp2 && $Heap[temp2, $ownerFrame] == $PeerGroupPlaceholder; - assume $Heap[$ElementProxy(temp2, -1), $ownerRef] == $ElementProxy(temp2, -1) && $Heap[$ElementProxy(temp2, -1), $ownerFrame] == $PeerGroupPlaceholder; - assume $Heap[temp2, $inv] == $typeof(temp2) && $Heap[temp2, $localinv] == $typeof(temp2); - assume (forall $i: int :: IntArrayGet($Heap[temp2, $elements], $i) == 0); - $Heap[temp2, $allocated] := true; - call System.Object..ctor($ElementProxy(temp2, -1)); - b := temp2; - assume IsHeap($Heap); - // ----- load field ----- AddMethod.ssc(27,9) - assert this != null; - stack0o := $Heap[this, Bag.a]; - // ----- load constant 0 ----- AddMethod.ssc(27,9) - stack1i := 0; - // ----- copy ----- AddMethod.ssc(27,9) - stack2o := b; - // ----- load constant 0 ----- AddMethod.ssc(27,9) - stack3i := 0; - // ----- load field ----- AddMethod.ssc(27,9) - assert this != null; - stack4o := $Heap[this, Bag.a]; - // ----- unary operator ----- AddMethod.ssc(27,9) - assert stack4o != null; - stack4i := $Length(stack4o); - // ----- unary operator ----- AddMethod.ssc(27,9) - stack4i := $IntToInt(stack4i, System.UIntPtr, System.Int32); - // ----- call ----- AddMethod.ssc(27,9) - call System.Array.Copy$System.Array$notnull$System.Int32$System.Array$notnull$System.Int32$System.Int32(stack0o, stack1i, stack2o, stack3i, stack4i); - // ----- store field ----- AddMethod.ssc(28,9) - assert this != null; - assert $Heap[this, $ownerFrame] == $PeerGroupPlaceholder || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame]) || $Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]); - assert ($Heap[b, $ownerRef] == this && $Heap[b, $ownerFrame] == Bag) || $Heap[b, $ownerFrame] == $PeerGroupPlaceholder; - assert $Heap[b, $ownerFrame] == $PeerGroupPlaceholder && $Heap[this, $inv] <: Bag && $Heap[this, $localinv] != $BaseClass(Bag) ==> (forall $pc: ref :: { $typeof($pc) } { $Heap[$pc, $localinv] } { $Heap[$pc, $inv] } { $Heap[$pc, $ownerFrame] } { $Heap[$pc, $ownerRef] } $pc != null && $Heap[$pc, $allocated] && $Heap[$pc, $ownerRef] == $Heap[b, $ownerRef] && $Heap[$pc, $ownerFrame] == $Heap[b, $ownerFrame] ==> $Heap[$pc, $inv] == $typeof($pc) && $Heap[$pc, $localinv] == $typeof($pc)); - assert $Heap[b, $ownerFrame] == $PeerGroupPlaceholder && $Heap[this, $inv] <: Bag && $Heap[this, $localinv] != $BaseClass(Bag) ==> $Heap[this, $ownerRef] != $Heap[b, $ownerRef] || $Heap[this, $ownerFrame] != $Heap[b, $ownerFrame]; - call $UpdateOwnersForRep(this, Bag, b); - havoc temp3; - $Heap[this, $exposeVersion] := temp3; - $Heap[this, Bag.a] := b; - assert !($Heap[this, $inv] <: Bag && $Heap[this, $localinv] != $BaseClass(Bag)) || 0 <= $Heap[this, Bag.n]; - assert !($Heap[this, $inv] <: Bag && $Heap[this, $localinv] != $BaseClass(Bag)) || $Heap[this, Bag.n] <= $Length($Heap[this, Bag.a]); - assume IsHeap($Heap); - goto block4539; - - block4658: - stack0o := null; - // ----- binary operator - // ----- branch - goto true4658to4624, false4658to4641; - - true4658to4624: - assume local2 == stack0o; - goto block4624; - - false4658to4641: - assume local2 != stack0o; - goto block4641; - - block4624: - // ----- load token ----- AddMethod.ssc(32,5) - havoc stack0s; - assume $IsTokenForType(stack0s, Bag); - // ----- statically resolved GetTypeFromHandle call ----- AddMethod.ssc(32,5) - stack0o := TypeObject(Bag); - // ----- local pack ----- AddMethod.ssc(32,5) - assert temp0 != null; - assert $Heap[temp0, $localinv] == System.Object; - assert 0 <= $Heap[temp0, Bag.n]; - assert $Heap[temp0, Bag.n] <= $Length($Heap[temp0, Bag.a]); - assert (forall $p: ref :: $p != null && $Heap[$p, $allocated] && $Heap[$p, $ownerRef] == temp0 && $Heap[$p, $ownerFrame] == Bag ==> $Heap[$p, $inv] == $typeof($p) && $Heap[$p, $localinv] == $typeof($p)); - $Heap[temp0, $localinv] := $typeof(temp0); - assume IsHeap($Heap); - goto block4726; - - block4641: - // ----- is instance - // ----- branch - goto true4641to4624, false4641to4692; - - true4641to4624: - assume $As(local2, Microsoft.Contracts.ICheckedException) != null; - goto block4624; - - false4641to4692: - assume $As(local2, Microsoft.Contracts.ICheckedException) == null; - goto block4692; - - block4692: - // ----- branch - goto block4726; - - block4726: - // ----- nop - // ----- branch - goto block4590; - - block4590: - // ----- return - return; -} - - - -axiom System.Type <: System.Type; - -axiom System.Reflection.MemberInfo <: System.Reflection.MemberInfo; - -axiom $BaseClass(System.Reflection.MemberInfo) == System.Object && AsDirectSubClass(System.Reflection.MemberInfo, $BaseClass(System.Reflection.MemberInfo)) == System.Reflection.MemberInfo; - -axiom $IsImmutable(System.Reflection.MemberInfo) && $AsImmutable(System.Reflection.MemberInfo) == System.Reflection.MemberInfo; - -axiom System.Reflection.ICustomAttributeProvider <: System.Reflection.ICustomAttributeProvider; - -axiom System.Reflection.ICustomAttributeProvider <: System.Object; - -axiom $IsMemberlessType(System.Reflection.ICustomAttributeProvider); - -axiom $AsInterface(System.Reflection.ICustomAttributeProvider) == System.Reflection.ICustomAttributeProvider; - -axiom System.Reflection.MemberInfo <: System.Reflection.ICustomAttributeProvider; - -axiom System.Runtime.InteropServices._MemberInfo <: System.Runtime.InteropServices._MemberInfo; - -axiom System.Runtime.InteropServices._MemberInfo <: System.Object; - -axiom $IsMemberlessType(System.Runtime.InteropServices._MemberInfo); - -axiom $AsInterface(System.Runtime.InteropServices._MemberInfo) == System.Runtime.InteropServices._MemberInfo; - -axiom System.Reflection.MemberInfo <: System.Runtime.InteropServices._MemberInfo; - -axiom $IsMemberlessType(System.Reflection.MemberInfo); - -// System.Reflection.MemberInfo object invariant -axiom (forall $oi: ref, $h: Heap :: { $h[$oi, $inv] <: System.Reflection.MemberInfo } IsHeap($h) && $h[$oi, $inv] <: System.Reflection.MemberInfo && $h[$oi, $localinv] != $BaseClass(System.Reflection.MemberInfo) ==> true); - -axiom $BaseClass(System.Type) == System.Reflection.MemberInfo && AsDirectSubClass(System.Type, $BaseClass(System.Type)) == System.Type; - -axiom $IsImmutable(System.Type) && $AsImmutable(System.Type) == System.Type; - -axiom System.Runtime.InteropServices._Type <: System.Runtime.InteropServices._Type; - -axiom System.Runtime.InteropServices._Type <: System.Object; - -axiom $IsMemberlessType(System.Runtime.InteropServices._Type); - -axiom $AsInterface(System.Runtime.InteropServices._Type) == System.Runtime.InteropServices._Type; - -axiom System.Type <: System.Runtime.InteropServices._Type; - -axiom System.Reflection.IReflect <: System.Reflection.IReflect; - -axiom System.Reflection.IReflect <: System.Object; - -axiom $IsMemberlessType(System.Reflection.IReflect); - -axiom $AsInterface(System.Reflection.IReflect) == System.Reflection.IReflect; - -axiom System.Type <: System.Reflection.IReflect; - -axiom $IsMemberlessType(System.Type); - -// System.Type object invariant -axiom (forall $oi: ref, $h: Heap :: { $h[$oi, $inv] <: System.Type } IsHeap($h) && $h[$oi, $inv] <: System.Type && $h[$oi, $localinv] != $BaseClass(System.Type) ==> true); - -procedure System.Array.Copy$System.Array$notnull$System.Int32$System.Array$notnull$System.Int32$System.Int32(sourceArray$in: ref where $IsNotNull(sourceArray$in, System.Array) && $Heap[sourceArray$in, $allocated], sourceIndex$in: int where InRange(sourceIndex$in, System.Int32), destinationArray$in: ref where $IsNotNull(destinationArray$in, System.Array) && $Heap[destinationArray$in, $allocated], destinationIndex$in: int where InRange(destinationIndex$in, System.Int32), length$in: int where InRange(length$in, System.Int32)); - // user-declared preconditions - requires sourceArray$in != null; - requires destinationArray$in != null; - requires $Rank(sourceArray$in) == $Rank(destinationArray$in); - requires sourceIndex$in >= $LBound(sourceArray$in, 0); - requires destinationIndex$in >= $LBound(destinationArray$in, 0); - requires length$in >= 0; - requires sourceIndex$in + length$in <= $LBound(sourceArray$in, 0) + $Length(sourceArray$in); - requires destinationIndex$in + length$in <= $LBound(destinationArray$in, 0) + $Length(destinationArray$in); - // sourceArray is peer consistent - requires (forall $pc: ref :: { $typeof($pc) } { $Heap[$pc, $localinv] } { $Heap[$pc, $inv] } { $Heap[$pc, $ownerFrame] } { $Heap[$pc, $ownerRef] } $pc != null && $Heap[$pc, $allocated] && $Heap[$pc, $ownerRef] == $Heap[sourceArray$in, $ownerRef] && $Heap[$pc, $ownerFrame] == $Heap[sourceArray$in, $ownerFrame] ==> $Heap[$pc, $inv] == $typeof($pc) && $Heap[$pc, $localinv] == $typeof($pc)); - // sourceArray is peer consistent (owner must not be valid) - requires $Heap[sourceArray$in, $ownerFrame] == $PeerGroupPlaceholder || !($Heap[$Heap[sourceArray$in, $ownerRef], $inv] <: $Heap[sourceArray$in, $ownerFrame]) || $Heap[$Heap[sourceArray$in, $ownerRef], $localinv] == $BaseClass($Heap[sourceArray$in, $ownerFrame]); - // destinationArray is peer consistent - requires (forall $pc: ref :: { $typeof($pc) } { $Heap[$pc, $localinv] } { $Heap[$pc, $inv] } { $Heap[$pc, $ownerFrame] } { $Heap[$pc, $ownerRef] } $pc != null && $Heap[$pc, $allocated] && $Heap[$pc, $ownerRef] == $Heap[destinationArray$in, $ownerRef] && $Heap[$pc, $ownerFrame] == $Heap[destinationArray$in, $ownerFrame] ==> $Heap[$pc, $inv] == $typeof($pc) && $Heap[$pc, $localinv] == $typeof($pc)); - // destinationArray is peer consistent (owner must not be valid) - requires $Heap[destinationArray$in, $ownerFrame] == $PeerGroupPlaceholder || !($Heap[$Heap[destinationArray$in, $ownerRef], $inv] <: $Heap[destinationArray$in, $ownerFrame]) || $Heap[$Heap[destinationArray$in, $ownerRef], $localinv] == $BaseClass($Heap[destinationArray$in, $ownerFrame]); - free requires $BeingConstructed == null; - free requires $PurityAxiomsCanBeAssumed; - modifies $Heap, $ActivityIndicator; - // hard-coded postcondition - ensures (forall $k: int :: { ValueArrayGet($Heap[destinationArray$in, $elements], $k) } (destinationIndex$in <= $k && $k < destinationIndex$in + length$in ==> old(ValueArrayGet($Heap[sourceArray$in, $elements], $k + sourceIndex$in - destinationIndex$in)) == ValueArrayGet($Heap[destinationArray$in, $elements], $k)) && (!(destinationIndex$in <= $k && $k < destinationIndex$in + length$in) ==> old(ValueArrayGet($Heap[destinationArray$in, $elements], $k)) == ValueArrayGet($Heap[destinationArray$in, $elements], $k))); - ensures (forall $k: int :: { IntArrayGet($Heap[destinationArray$in, $elements], $k) } (destinationIndex$in <= $k && $k < destinationIndex$in + length$in ==> old(IntArrayGet($Heap[sourceArray$in, $elements], $k + sourceIndex$in - destinationIndex$in)) == IntArrayGet($Heap[destinationArray$in, $elements], $k)) && (!(destinationIndex$in <= $k && $k < destinationIndex$in + length$in) ==> old(IntArrayGet($Heap[destinationArray$in, $elements], $k)) == IntArrayGet($Heap[destinationArray$in, $elements], $k))); - ensures (forall $k: int :: { RefArrayGet($Heap[destinationArray$in, $elements], $k) } (destinationIndex$in <= $k && $k < destinationIndex$in + length$in ==> old(RefArrayGet($Heap[sourceArray$in, $elements], $k + sourceIndex$in - destinationIndex$in)) == RefArrayGet($Heap[destinationArray$in, $elements], $k)) && (!(destinationIndex$in <= $k && $k < destinationIndex$in + length$in) ==> old(RefArrayGet($Heap[destinationArray$in, $elements], $k)) == RefArrayGet($Heap[destinationArray$in, $elements], $k))); - // newly allocated objects are fully valid - free ensures (forall $o: ref :: { $Heap[$o, $localinv] } { $Heap[$o, $inv] } $o != null && !old($Heap)[$o, $allocated] && $Heap[$o, $allocated] ==> $Heap[$o, $inv] == $typeof($o) && $Heap[$o, $localinv] == $typeof($o)); - // first consistent owner unchanged if its exposeVersion is - free ensures (forall $o: ref :: { $Heap[$o, $FirstConsistentOwner] } old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] ==> old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner]); - // frame condition - ensures (forall $o: ref, $f: Field a :: { $Heap[$o, $f] } IncludeInMainFrameCondition($f) && $o != null && old($Heap)[$o, $allocated] && (old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame]) || old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])) && old($o != destinationArray$in || !($typeof(destinationArray$in) <: DeclType222($f)) || !$IncludedInModifiesStar($f)) && old($o != destinationArray$in || $f != $exposeVersion) ==> old($Heap)[$o, $f] == $Heap[$o, $f]); - free ensures $HeapSucc(old($Heap), $Heap); - // inv/localinv change only in blocks - free ensures (forall $o: ref :: { $Heap[$o, $localinv] } { $Heap[$o, $inv] } old($Heap)[$o, $allocated] ==> old($Heap)[$o, $inv] == $Heap[$o, $inv] && old($Heap)[$o, $localinv] == $Heap[$o, $localinv]); - free ensures (forall $o: ref :: { $Heap[$o, $allocated] } old($Heap)[$o, $allocated] ==> $Heap[$o, $allocated]) && (forall $ot: ref :: { $Heap[$ot, $ownerFrame] } { $Heap[$ot, $ownerRef] } old($Heap)[$ot, $allocated] && old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder ==> $Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef] && $Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]) && old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]; - free ensures (forall $o: ref :: { $Heap[$o, $sharingMode] } old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]); - - - -axiom Microsoft.Contracts.ICheckedException <: Microsoft.Contracts.ICheckedException; - -axiom Microsoft.Contracts.ICheckedException <: System.Object; - -axiom $IsMemberlessType(Microsoft.Contracts.ICheckedException); - -axiom $AsInterface(Microsoft.Contracts.ICheckedException) == Microsoft.Contracts.ICheckedException; - -procedure Bag.AddAgain$System.Int32(this: ref where $IsNotNull(this, Bag) && $Heap[this, $allocated], x$in: int where InRange(x$in, System.Int32)); - // target object is peer consistent - requires (forall $pc: ref :: { $typeof($pc) } { $Heap[$pc, $localinv] } { $Heap[$pc, $inv] } { $Heap[$pc, $ownerFrame] } { $Heap[$pc, $ownerRef] } $pc != null && $Heap[$pc, $allocated] && $Heap[$pc, $ownerRef] == $Heap[this, $ownerRef] && $Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame] ==> $Heap[$pc, $inv] == $typeof($pc) && $Heap[$pc, $localinv] == $typeof($pc)); - // target object is peer consistent (owner must not be valid) - requires $Heap[this, $ownerFrame] == $PeerGroupPlaceholder || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame]) || $Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]); - free requires $BeingConstructed == null; - free requires $PurityAxiomsCanBeAssumed; - modifies $Heap, $ActivityIndicator; - // newly allocated objects are fully valid - free ensures (forall $o: ref :: { $Heap[$o, $localinv] } { $Heap[$o, $inv] } $o != null && !old($Heap)[$o, $allocated] && $Heap[$o, $allocated] ==> $Heap[$o, $inv] == $typeof($o) && $Heap[$o, $localinv] == $typeof($o)); - // first consistent owner unchanged if its exposeVersion is - free ensures (forall $o: ref :: { $Heap[$o, $FirstConsistentOwner] } old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] ==> old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner]); - // frame condition - ensures (forall $o: ref, $f: Field a :: { $Heap[$o, $f] } IncludeInMainFrameCondition($f) && $o != null && old($Heap)[$o, $allocated] && (old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame]) || old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])) && old($o != this || !($typeof(this) <: DeclType222($f)) || !$IncludedInModifiesStar($f)) && old($o != this || $f != $exposeVersion) ==> old($Heap)[$o, $f] == $Heap[$o, $f]); - free ensures $HeapSucc(old($Heap), $Heap); - // inv/localinv change only in blocks - free ensures (forall $o: ref :: { $Heap[$o, $localinv] } { $Heap[$o, $inv] } old($Heap)[$o, $allocated] ==> old($Heap)[$o, $inv] == $Heap[$o, $inv] && old($Heap)[$o, $localinv] == $Heap[$o, $localinv]); - free ensures (forall $o: ref :: { $Heap[$o, $allocated] } old($Heap)[$o, $allocated] ==> $Heap[$o, $allocated]) && (forall $ot: ref :: { $Heap[$ot, $ownerFrame] } { $Heap[$ot, $ownerRef] } old($Heap)[$ot, $allocated] && old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder ==> $Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef] && $Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]) && old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]; - free ensures (forall $o: ref :: { $Heap[$o, $sharingMode] } old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]); - - - -implementation Bag.AddAgain$System.Int32(this: ref, x$in: int) -{ - var x: int where InRange(x, System.Int32), temp0: ref, stack1s: struct, stack1o: ref, temp1: exposeVersionType, local2: ref where $Is(local2, System.Exception) && $Heap[local2, $allocated], stack0i: int, stack1i: int, stack0b: bool, stack0o: ref, local4: int where InRange(local4, System.Int32), temp2: exposeVersionType, b: ref where $Is(b, IntArray(System.Int32, 1)) && $Heap[b, $allocated], temp3: ref, stack2i: int, temp4: exposeVersionType, stack0s: struct; - - entry: - x := x$in; - goto block6188; - - block6188: - goto block6341; - - block6341: - // ----- nop - // ----- FrameGuard processing ----- AddMethod.ssc(38,13) - temp0 := this; - // ----- load token ----- AddMethod.ssc(38,13) - havoc stack1s; - assume $IsTokenForType(stack1s, Bag); - // ----- statically resolved GetTypeFromHandle call ----- AddMethod.ssc(38,13) - stack1o := TypeObject(Bag); - // ----- local unpack ----- AddMethod.ssc(38,13) - assert temp0 != null; - assert ($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame]) || $Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame])) && $Heap[temp0, $inv] <: Bag && $Heap[temp0, $localinv] == $typeof(temp0); - $Heap[temp0, $localinv] := System.Object; - havoc temp1; - $Heap[temp0, $exposeVersion] := temp1; - assume IsHeap($Heap); - local2 := null; - goto block6358; - - block6358: - // ----- load field ----- AddMethod.ssc(40,7) - assert this != null; - stack0i := $Heap[this, Bag.n]; - // ----- load field ----- AddMethod.ssc(40,7) - assert this != null; - stack1o := $Heap[this, Bag.a]; - // ----- unary operator ----- AddMethod.ssc(40,7) - assert stack1o != null; - stack1i := $Length(stack1o); - // ----- unary operator ----- AddMethod.ssc(40,7) - stack1i := $IntToInt(stack1i, System.UIntPtr, System.Int32); - // ----- binary operator ----- AddMethod.ssc(40,7) - // ----- branch ----- AddMethod.ssc(40,7) - goto true6358to6392, false6358to6375; - - true6358to6392: - assume stack0i != stack1i; - goto block6392; - - false6358to6375: - assume stack0i == stack1i; - goto block6375; - - block6392: - // ----- load field ----- AddMethod.ssc(46,7) - assert this != null; - stack0o := $Heap[this, Bag.a]; - // ----- load field ----- AddMethod.ssc(46,7) - assert this != null; - stack1i := $Heap[this, Bag.n]; - // ----- store element ----- AddMethod.ssc(46,7) - assert stack0o != null; - assert 0 <= stack1i; - assert stack1i < $Length(stack0o); - assert $Heap[stack0o, $ownerFrame] == $PeerGroupPlaceholder || !($Heap[$Heap[stack0o, $ownerRef], $inv] <: $Heap[stack0o, $ownerFrame]) || $Heap[$Heap[stack0o, $ownerRef], $localinv] == $BaseClass($Heap[stack0o, $ownerFrame]); - $Heap[stack0o, $elements] := IntArraySet($Heap[stack0o, $elements], stack1i, x); - assume IsHeap($Heap); - // ----- load field ----- AddMethod.ssc(47,7) - assert this != null; - local4 := $Heap[this, Bag.n]; - // ----- load constant 1 ----- AddMethod.ssc(47,7) - stack0i := 1; - // ----- binary operator ----- AddMethod.ssc(47,7) - stack0i := local4 + stack0i; - // ----- store field ----- AddMethod.ssc(47,7) - assert this != null; - assert $Heap[this, $ownerFrame] == $PeerGroupPlaceholder || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame]) || $Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]); - havoc temp2; - $Heap[this, $exposeVersion] := temp2; - $Heap[this, Bag.n] := stack0i; - assert !($Heap[this, $inv] <: Bag && $Heap[this, $localinv] != $BaseClass(Bag)) || 0 <= $Heap[this, Bag.n]; - assert !($Heap[this, $inv] <: Bag && $Heap[this, $localinv] != $BaseClass(Bag)) || $Heap[this, Bag.n] <= $Length($Heap[this, Bag.a]); - assume IsHeap($Heap); - // ----- copy - stack0i := local4; - // ----- branch - goto block6562; - - block6375: - // ----- load constant 2 ----- AddMethod.ssc(42,15) - stack0i := 2; - // ----- load field ----- AddMethod.ssc(42,15) - assert this != null; - stack1o := $Heap[this, Bag.a]; - // ----- unary operator ----- AddMethod.ssc(42,15) - assert stack1o != null; - stack1i := $Length(stack1o); - // ----- unary operator ----- AddMethod.ssc(42,15) - stack1i := $IntToInt(stack1i, System.UIntPtr, System.Int32); - // ----- binary operator ----- AddMethod.ssc(42,15) - stack0i := stack0i * stack1i; - // ----- load constant 1 ----- AddMethod.ssc(42,15) - stack1i := 1; - // ----- binary operator ----- AddMethod.ssc(42,15) - stack0i := stack0i + stack1i; - // ----- new array ----- AddMethod.ssc(42,15) - assert 0 <= stack0i; - havoc temp3; - assume $Heap[temp3, $allocated] == false && $Length(temp3) == stack0i; - assume $Heap[$ElementProxy(temp3, -1), $allocated] == false && $ElementProxy(temp3, -1) != temp3 && $ElementProxy(temp3, -1) != null; - assume temp3 != null; - assume $typeof(temp3) == IntArray(System.Int32, 1); - assume $Heap[temp3, $ownerRef] == temp3 && $Heap[temp3, $ownerFrame] == $PeerGroupPlaceholder; - assume $Heap[$ElementProxy(temp3, -1), $ownerRef] == $ElementProxy(temp3, -1) && $Heap[$ElementProxy(temp3, -1), $ownerFrame] == $PeerGroupPlaceholder; - assume $Heap[temp3, $inv] == $typeof(temp3) && $Heap[temp3, $localinv] == $typeof(temp3); - assume (forall $i: int :: IntArrayGet($Heap[temp3, $elements], $i) == 0); - $Heap[temp3, $allocated] := true; - call System.Object..ctor($ElementProxy(temp3, -1)); - b := temp3; - assume IsHeap($Heap); - // ----- load field ----- AddMethod.ssc(43,9) - assert this != null; - stack0o := $Heap[this, Bag.a]; - // ----- copy ----- AddMethod.ssc(43,9) - stack1o := b; - // ----- load constant 0 ----- AddMethod.ssc(43,9) - stack2i := 0; - // ----- call ----- AddMethod.ssc(43,9) - assert stack0o != null; - call System.Array.CopyTo$System.Array$notnull$System.Int32$.Virtual.$(stack0o, stack1o, stack2i); - // ----- store field ----- AddMethod.ssc(44,9) - assert this != null; - assert $Heap[this, $ownerFrame] == $PeerGroupPlaceholder || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame]) || $Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]); - assert ($Heap[b, $ownerRef] == this && $Heap[b, $ownerFrame] == Bag) || $Heap[b, $ownerFrame] == $PeerGroupPlaceholder; - assert $Heap[b, $ownerFrame] == $PeerGroupPlaceholder && $Heap[this, $inv] <: Bag && $Heap[this, $localinv] != $BaseClass(Bag) ==> (forall $pc: ref :: { $typeof($pc) } { $Heap[$pc, $localinv] } { $Heap[$pc, $inv] } { $Heap[$pc, $ownerFrame] } { $Heap[$pc, $ownerRef] } $pc != null && $Heap[$pc, $allocated] && $Heap[$pc, $ownerRef] == $Heap[b, $ownerRef] && $Heap[$pc, $ownerFrame] == $Heap[b, $ownerFrame] ==> $Heap[$pc, $inv] == $typeof($pc) && $Heap[$pc, $localinv] == $typeof($pc)); - assert $Heap[b, $ownerFrame] == $PeerGroupPlaceholder && $Heap[this, $inv] <: Bag && $Heap[this, $localinv] != $BaseClass(Bag) ==> $Heap[this, $ownerRef] != $Heap[b, $ownerRef] || $Heap[this, $ownerFrame] != $Heap[b, $ownerFrame]; - call $UpdateOwnersForRep(this, Bag, b); - havoc temp4; - $Heap[this, $exposeVersion] := temp4; - $Heap[this, Bag.a] := b; - assert !($Heap[this, $inv] <: Bag && $Heap[this, $localinv] != $BaseClass(Bag)) || 0 <= $Heap[this, Bag.n]; - assert !($Heap[this, $inv] <: Bag && $Heap[this, $localinv] != $BaseClass(Bag)) || $Heap[this, Bag.n] <= $Length($Heap[this, Bag.a]); - assume IsHeap($Heap); - goto block6392; - - block6562: - stack0o := null; - // ----- binary operator - // ----- branch - goto true6562to6477, false6562to6579; - - true6562to6477: - assume local2 == stack0o; - goto block6477; - - false6562to6579: - assume local2 != stack0o; - goto block6579; - - block6477: - // ----- load token ----- AddMethod.ssc(48,5) - havoc stack0s; - assume $IsTokenForType(stack0s, Bag); - // ----- statically resolved GetTypeFromHandle call ----- AddMethod.ssc(48,5) - stack0o := TypeObject(Bag); - // ----- local pack ----- AddMethod.ssc(48,5) - assert temp0 != null; - assert $Heap[temp0, $localinv] == System.Object; - assert 0 <= $Heap[temp0, Bag.n]; - assert $Heap[temp0, Bag.n] <= $Length($Heap[temp0, Bag.a]); - assert (forall $p: ref :: $p != null && $Heap[$p, $allocated] && $Heap[$p, $ownerRef] == temp0 && $Heap[$p, $ownerFrame] == Bag ==> $Heap[$p, $inv] == $typeof($p) && $Heap[$p, $localinv] == $typeof($p)); - $Heap[temp0, $localinv] := $typeof(temp0); - assume IsHeap($Heap); - goto block6545; - - block6579: - // ----- is instance - // ----- branch - goto true6579to6477, false6579to6528; - - true6579to6477: - assume $As(local2, Microsoft.Contracts.ICheckedException) != null; - goto block6477; - - false6579to6528: - assume $As(local2, Microsoft.Contracts.ICheckedException) == null; - goto block6528; - - block6528: - // ----- branch - goto block6545; - - block6545: - // ----- nop - // ----- branch - goto block6443; - - block6443: - // ----- return - return; -} - - - -procedure Bag..cctor(); - free requires $BeingConstructed == null; - free requires $PurityAxiomsCanBeAssumed; - modifies $Heap, $ActivityIndicator; - // newly allocated objects are fully valid - free ensures (forall $o: ref :: { $Heap[$o, $localinv] } { $Heap[$o, $inv] } $o != null && !old($Heap)[$o, $allocated] && $Heap[$o, $allocated] ==> $Heap[$o, $inv] == $typeof($o) && $Heap[$o, $localinv] == $typeof($o)); - // first consistent owner unchanged if its exposeVersion is - free ensures (forall $o: ref :: { $Heap[$o, $FirstConsistentOwner] } old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] ==> old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner]); - // frame condition - ensures (forall $o: ref, $f: Field a :: { $Heap[$o, $f] } IncludeInMainFrameCondition($f) && $o != null && old($Heap)[$o, $allocated] && (old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame]) || old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])) && old(true) && old(true) ==> old($Heap)[$o, $f] == $Heap[$o, $f]); - free ensures $HeapSucc(old($Heap), $Heap); - // inv/localinv change only in blocks - free ensures (forall $o: ref :: { $Heap[$o, $localinv] } { $Heap[$o, $inv] } old($Heap)[$o, $allocated] ==> old($Heap)[$o, $inv] == $Heap[$o, $inv] && old($Heap)[$o, $localinv] == $Heap[$o, $localinv]); - free ensures (forall $o: ref :: { $Heap[$o, $allocated] } old($Heap)[$o, $allocated] ==> $Heap[$o, $allocated]) && (forall $ot: ref :: { $Heap[$ot, $ownerFrame] } { $Heap[$ot, $ownerRef] } old($Heap)[$ot, $allocated] && old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder ==> $Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef] && $Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]) && old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]; - free ensures (forall $o: ref :: { $Heap[$o, $sharingMode] } old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]); - - - -implementation Bag..cctor() -{ - - entry: - goto block7650; - - block7650: - goto block7701; - - block7701: - // ----- nop - // ----- return - return; -} - - +// RUN: %boogie -typeEncoding:n -logPrefix:0n "%s" > "%t" +// RUN: %diff "%s.n.expect" "%t" +// RUN: %boogie -typeEncoding:p -logPrefix:0p "%s" > "%t" +// RUN: %diff "%s.p.expect" "%t" +// RUN: %boogie -typeEncoding:a -logPrefix:0a "%s" > "%t" +// RUN: %diff "%s.a.expect" "%t" +// XFAIL: * +// Spec# program verifier version 0.90, Copyright (c) 2003-2008, Microsoft. +// Command Line Options: /print:debug.txt AddMethod.dll + +type real; + +type elements; + +type struct; + +type name; +type any; + +type exposeVersionType; + +type Field a; +type Heap = [ref,Field x]x; + +var $Heap: Heap where IsHeap($Heap); + +type ActivityType; + +var $ActivityIndicator: ActivityType; + +function IsHeap(h: Heap) returns (bool); + +const unique $allocated: Field bool; + +const unique $elements: Field elements; + +function DeclType222(Field a) returns (name); + +axiom DeclType222($elements) == System.Object; + +const unique $inv: Field name; + +const unique $localinv: Field name; + +const unique $exposeVersion: Field exposeVersionType; + +axiom DeclType222($exposeVersion) == System.Object; + +const unique $sharingMode: Field any; + +const unique $SharingMode_Unshared: any; + +const unique $SharingMode_LockProtected: any; + +const unique $ownerRef: Field ref; + +const unique $ownerFrame: Field name; + +const unique $PeerGroupPlaceholder: name; + +function ClassRepr(class: name) returns (ref); + +function ClassReprInv(ref) returns (name); + +axiom (forall c: name :: { ClassRepr(c) } ClassReprInv(ClassRepr(c)) == c); + +axiom (forall T: name :: !($typeof(ClassRepr(T)) <: System.Object)); + +axiom (forall T: name :: ClassRepr(T) != null); + +axiom (forall T: name, h: Heap :: { h[ClassRepr(T), $ownerFrame] } IsHeap(h) ==> h[ClassRepr(T), $ownerFrame] == $PeerGroupPlaceholder); + +function IncludeInMainFrameCondition(f: Field a) returns (bool); + +axiom IncludeInMainFrameCondition($allocated); + +axiom IncludeInMainFrameCondition($elements); + +axiom !IncludeInMainFrameCondition($inv); + +axiom !IncludeInMainFrameCondition($localinv); + +axiom IncludeInMainFrameCondition($ownerRef); + +axiom IncludeInMainFrameCondition($ownerFrame); + +axiom IncludeInMainFrameCondition($exposeVersion); + +axiom !IncludeInMainFrameCondition($FirstConsistentOwner); + +function IsStaticField(f: Field a) returns (bool); + +axiom !IsStaticField($allocated); + +axiom !IsStaticField($elements); + +axiom !IsStaticField($inv); + +axiom !IsStaticField($localinv); + +axiom !IsStaticField($exposeVersion); + +function $IncludedInModifiesStar(f: Field a) returns (bool); + +axiom !$IncludedInModifiesStar($ownerRef); + +axiom !$IncludedInModifiesStar($ownerFrame); + +axiom $IncludedInModifiesStar($exposeVersion); + +axiom $IncludedInModifiesStar($elements); + +function ValueArrayGet(elements, int) returns (any); + +function ValueArraySet(elements, int, any) returns (elements); + +function IntArrayGet(elements, int) returns (int); + +function IntArraySet(elements, int, int) returns (elements); + +function RefArrayGet(elements, int) returns (ref); + +function RefArraySet(elements, int, ref) returns (elements); + +axiom (forall A: elements, i: int, x: any :: ValueArrayGet(ValueArraySet(A, i, x), i) == x); + +axiom (forall A: elements, i: int, j: int, x: any :: i != j ==> ValueArrayGet(ValueArraySet(A, i, x), j) == ValueArrayGet(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: 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)); + +function ArrayIndex(arr: ref, dim: int, indexAtDim: int, remainingIndexContribution: int) returns (int); + +function ArrayIndexInvX(arrayIndex: int) returns (indexAtDim: int); + +function ArrayIndexInvY(arrayIndex: int) returns (remainingIndexContribution: int); + +axiom (forall a: ref, d: int, x: int, y: int :: { ArrayIndex(a, d, x, y) } ArrayIndexInvX(ArrayIndex(a, d, x, y)) == x); + +axiom (forall a: ref, d: int, x: int, y: int :: { ArrayIndex(a, d, x, y) } ArrayIndexInvY(ArrayIndex(a, d, x, y)) == y); + +axiom (forall a: ref, i: int, heap: Heap :: { IntArrayGet(heap[a, $elements], i) } IsHeap(heap) ==> InRange(IntArrayGet(heap[a, $elements], i), $ElementType($typeof(a)))); + +axiom (forall a: ref, i: int, heap: Heap :: { $typeof(RefArrayGet(heap[a, $elements], i)) } IsHeap(heap) && RefArrayGet(heap[a, $elements], i) != null ==> $typeof(RefArrayGet(heap[a, $elements], i)) <: $ElementType($typeof(a))); + +axiom (forall a: ref, T: name, i: int, r: int, heap: Heap :: { $typeof(a) <: NonNullRefArray(T, r), RefArrayGet(heap[a, $elements], i) } IsHeap(heap) && $typeof(a) <: NonNullRefArray(T, r) ==> RefArrayGet(heap[a, $elements], i) != null); + +function $Rank(ref) returns (int); + +axiom (forall a: ref :: 1 <= $Rank(a)); + +axiom (forall a: ref, T: name, r: int :: { $typeof(a) <: RefArray(T, r) } a != null && $typeof(a) <: RefArray(T, r) ==> $Rank(a) == r); + +axiom (forall a: ref, T: name, r: int :: { $typeof(a) <: NonNullRefArray(T, r) } a != null && $typeof(a) <: NonNullRefArray(T, r) ==> $Rank(a) == r); + +axiom (forall a: ref, T: name, r: int :: { $typeof(a) <: ValueArray(T, r) } a != null && $typeof(a) <: ValueArray(T, r) ==> $Rank(a) == r); + +axiom (forall a: ref, T: name, r: int :: { $typeof(a) <: IntArray(T, r) } a != null && $typeof(a) <: IntArray(T, r) ==> $Rank(a) == r); + +function $Length(ref) returns (int); + +axiom (forall a: ref :: { $Length(a) } 0 <= $Length(a) && $Length(a) <= int#2147483647); + +function $DimLength(ref, int) returns (int); + +axiom (forall a: ref, i: int :: 0 <= $DimLength(a, i)); + +axiom (forall a: ref :: { $DimLength(a, 0) } $Rank(a) == 1 ==> $DimLength(a, 0) == $Length(a)); + +function $LBound(ref, int) returns (int); + +function $UBound(ref, int) returns (int); + +axiom (forall a: ref, i: int :: { $LBound(a, i) } $LBound(a, i) == 0); + +axiom (forall a: ref, i: int :: { $UBound(a, i) } $UBound(a, i) == $DimLength(a, i) - 1); + +const unique $ArrayCategoryValue: name; + +const unique $ArrayCategoryInt: name; + +const unique $ArrayCategoryRef: name; + +const unique $ArrayCategoryNonNullRef: name; + +function $ArrayCategory(arrayType: name) returns (arrayCategory: name); + +axiom (forall T: name, ET: name, r: int :: { T <: ValueArray(ET, r) } T <: ValueArray(ET, r) ==> $ArrayCategory(T) == $ArrayCategoryValue); + +axiom (forall T: name, ET: name, r: int :: { T <: IntArray(ET, r) } T <: IntArray(ET, r) ==> $ArrayCategory(T) == $ArrayCategoryInt); + +axiom (forall T: name, ET: name, r: int :: { T <: RefArray(ET, r) } T <: RefArray(ET, r) ==> $ArrayCategory(T) == $ArrayCategoryRef); + +axiom (forall T: name, ET: name, r: int :: { T <: NonNullRefArray(ET, r) } T <: NonNullRefArray(ET, r) ==> $ArrayCategory(T) == $ArrayCategoryNonNullRef); + +const unique System.Array: name; + +axiom System.Array <: System.Object; + +function $ElementType(name) returns (name); + +function ValueArray(elementType: name, rank: int) returns (name); + +axiom (forall T: name, r: int :: { ValueArray(T, r) } ValueArray(T, r) <: ValueArray(T, r) && ValueArray(T, r) <: System.Array); + +function IntArray(elementType: name, rank: int) returns (name); + +axiom (forall T: name, r: int :: { IntArray(T, r) } IntArray(T, r) <: IntArray(T, r) && IntArray(T, r) <: System.Array); + +function RefArray(elementType: name, rank: int) returns (name); + +axiom (forall T: name, r: int :: { RefArray(T, r) } RefArray(T, r) <: RefArray(T, r) && RefArray(T, r) <: System.Array); + +function NonNullRefArray(elementType: name, rank: int) returns (name); + +axiom (forall T: name, r: int :: { NonNullRefArray(T, r) } NonNullRefArray(T, r) <: NonNullRefArray(T, r) && NonNullRefArray(T, r) <: System.Array); + +function NonNullRefArrayRaw(array: ref, elementType: name, rank: int) returns (bool); + +axiom (forall array: ref, elementType: name, rank: int :: { NonNullRefArrayRaw(array, elementType, rank) } NonNullRefArrayRaw(array, elementType, rank) ==> $typeof(array) <: System.Array && $Rank(array) == rank && elementType <: $ElementType($typeof(array))); + +axiom (forall T: name, U: name, r: int :: U <: T ==> RefArray(U, r) <: RefArray(T, r)); + +axiom (forall T: name, U: name, r: int :: U <: T ==> NonNullRefArray(U, r) <: NonNullRefArray(T, r)); + +axiom (forall A: name, r: int :: $ElementType(ValueArray(A, r)) == A); + +axiom (forall A: name, r: int :: $ElementType(IntArray(A, r)) == A); + +axiom (forall A: name, r: int :: $ElementType(RefArray(A, r)) == A); + +axiom (forall A: name, r: int :: $ElementType(NonNullRefArray(A, r)) == A); + +axiom (forall A: name, r: int, T: name :: { T <: RefArray(A, r) } T <: RefArray(A, r) ==> T != A && T == RefArray($ElementType(T), r) && $ElementType(T) <: A); + +axiom (forall A: name, r: int, T: name :: { T <: NonNullRefArray(A, r) } T <: NonNullRefArray(A, r) ==> T != A && T == NonNullRefArray($ElementType(T), r) && $ElementType(T) <: A); + +axiom (forall A: name, r: int, T: name :: { T <: ValueArray(A, r) } T <: ValueArray(A, r) ==> T == ValueArray(A, r)); + +axiom (forall A: name, r: int, T: name :: { T <: IntArray(A, r) } T <: IntArray(A, r) ==> T == IntArray(A, r)); + +axiom (forall A: name, r: int, T: name :: { RefArray(A, r) <: T } RefArray(A, r) <: T ==> System.Array <: T || (T == RefArray($ElementType(T), r) && A <: $ElementType(T))); + +axiom (forall A: name, r: int, T: name :: { NonNullRefArray(A, r) <: T } NonNullRefArray(A, r) <: T ==> System.Array <: T || (T == NonNullRefArray($ElementType(T), r) && A <: $ElementType(T))); + +axiom (forall A: name, r: int, T: name :: { ValueArray(A, r) <: T } ValueArray(A, r) <: T ==> System.Array <: T || T == ValueArray(A, r)); + +axiom (forall A: name, r: int, T: name :: { IntArray(A, r) <: T } IntArray(A, r) <: T ==> System.Array <: T || T == IntArray(A, r)); + +function $ArrayPtr(elementType: name) returns (name); + +function $ElementProxy(ref, int) returns (ref); + +function $ElementProxyStruct(struct, int) returns (ref); + +axiom (forall a: ref, i: int, heap: Heap :: { heap[RefArrayGet(heap[a, $elements], i), $ownerRef] } { heap[RefArrayGet(heap[a, $elements], i), $ownerFrame] } IsHeap(heap) && $typeof(a) <: System.Array ==> RefArrayGet(heap[a, $elements], i) == null || $IsImmutable($typeof(RefArrayGet(heap[a, $elements], i))) || (heap[RefArrayGet(heap[a, $elements], i), $ownerRef] == heap[$ElementProxy(a, 0 - 1), $ownerRef] && heap[RefArrayGet(heap[a, $elements], i), $ownerFrame] == heap[$ElementProxy(a, 0 - 1), $ownerFrame])); + +axiom (forall a: ref, heap: Heap :: { IsAllocated(heap, a) } IsHeap(heap) && IsAllocated(heap, a) && $typeof(a) <: System.Array ==> IsAllocated(heap, $ElementProxy(a, 0 - 1))); + +axiom (forall o: ref, pos: int :: { $typeof($ElementProxy(o, pos)) } $typeof($ElementProxy(o, pos)) == System.Object); + +axiom (forall o: struct, pos: int :: { $typeof($ElementProxyStruct(o, pos)) } $typeof($ElementProxyStruct(o, pos)) == System.Object); + +function $StructGet(struct, name) returns (any); + +function $StructSet(struct, name, any) returns (struct); + +axiom (forall s: struct, f: name, x: any :: $StructGet($StructSet(s, f, x), f) == x); + +axiom (forall s: struct, f: name, f': name, x: any :: f != f' ==> $StructGet($StructSet(s, f, x), f') == $StructGet(s, f')); + +function ZeroInit(s: struct, typ: name) returns (bool); + +function $typeof(ref) returns (name); + +function $BaseClass(sub: name) returns (base: name); + +axiom (forall T: name :: { $BaseClass(T) } T <: $BaseClass(T) && (T != System.Object ==> T != $BaseClass(T))); + +function AsDirectSubClass(sub: name, base: name) returns (sub': name); + +function OneClassDown(sub: name, base: name) returns (directSub: name); + +axiom (forall A: name, B: name, C: name :: { C <: AsDirectSubClass(B, A) } C <: AsDirectSubClass(B, A) ==> OneClassDown(C, A) == B); + +function $IsValueType(name) returns (bool); + +axiom (forall T: name :: $IsValueType(T) ==> (forall U: name :: T <: U ==> T == U) && (forall U: name :: U <: T ==> T == U)); + +const unique System.Boolean: name; + +axiom $IsValueType(System.Boolean); + +const unique System.Object: name; + +function $IsTokenForType(struct, name) returns (bool); + +function TypeObject(name) returns (ref); + +const unique System.Type: name; + +axiom System.Type <: System.Object; + +axiom (forall T: name :: { TypeObject(T) } $IsNotNull(TypeObject(T), System.Type)); + +function TypeName(ref) returns (name); + +axiom (forall T: name :: { TypeObject(T) } TypeName(TypeObject(T)) == T); + +function $Is(ref, name) returns (bool); + +axiom (forall o: ref, T: name :: { $Is(o, T) } $Is(o, T) <==> o == null || $typeof(o) <: T); + +function $IsNotNull(ref, name) returns (bool); + +axiom (forall o: ref, T: name :: { $IsNotNull(o, T) } $IsNotNull(o, T) <==> o != null && $Is(o, T)); + +function $As(ref, name) returns (ref); + +axiom (forall o: ref, T: name :: $Is(o, T) ==> $As(o, T) == o); + +axiom (forall o: ref, T: name :: !$Is(o, T) ==> $As(o, T) == null); + +axiom (forall h: Heap, o: ref :: { $typeof(o) <: System.Array, h[o, $inv] } IsHeap(h) && o != null && $typeof(o) <: System.Array ==> h[o, $inv] == $typeof(o) && h[o, $localinv] == $typeof(o)); + +function IsAllocated(h: Heap, o: a) returns (bool); + +axiom (forall h: Heap, o: ref, f: Field a :: { IsAllocated(h, h[o, f]) } IsHeap(h) && h[o, $allocated] ==> IsAllocated(h, h[o, f])); + +axiom (forall h: Heap, o: ref, f: Field ref :: { h[h[o, f], $allocated] } IsHeap(h) && h[o, $allocated] ==> h[h[o, f], $allocated]); + +axiom (forall h: Heap, s: struct, f: name :: { IsAllocated(h, $StructGet(s, f)) } IsAllocated(h, s) ==> IsAllocated(h, $StructGet(s, f))); + +axiom (forall h: Heap, e: elements, i: int :: { IsAllocated(h, RefArrayGet(e, i)) } IsAllocated(h, e) ==> IsAllocated(h, RefArrayGet(e, i))); + +axiom (forall h: Heap, e: elements, i: int :: { IsAllocated(h, ValueArrayGet(e, i)) } IsAllocated(h, e) ==> IsAllocated(h, ValueArrayGet(e, i))); + +axiom (forall h: Heap, o: ref :: { h[o, $allocated] } IsAllocated(h, o) ==> h[o, $allocated]); + +axiom (forall h: Heap, c: name :: { h[ClassRepr(c), $allocated] } IsHeap(h) ==> h[ClassRepr(c), $allocated]); + +const $BeingConstructed: ref; + +const unique $NonNullFieldsAreInitialized: Field bool; + +const $PurityAxiomsCanBeAssumed: bool; + +axiom DeclType222($NonNullFieldsAreInitialized) == System.Object; + + + +function AsNonNullRefField(field: Field ref, T: name) returns (f: Field ref); + +function AsRefField(field: Field ref, T: name) returns (f: Field ref); + +function AsRangeField(field: Field int, T: name) returns (f: Field int); + +axiom (forall f: Field ref, T: name :: { AsNonNullRefField(f, T) } AsNonNullRefField(f, T) == f ==> AsRefField(f, T) == f); + +axiom (forall h: Heap, o: ref, f: Field ref, T: name :: { h[o, AsRefField(f, T)] } IsHeap(h) ==> $Is(h[o, AsRefField(f, T)], T)); + +axiom (forall h: Heap, o: ref, f: Field ref, T: name :: { h[o, AsNonNullRefField(f, T)] } IsHeap(h) && o != null && (o != $BeingConstructed || h[$BeingConstructed, $NonNullFieldsAreInitialized] == true) ==> h[o, AsNonNullRefField(f, T)] != null); + +axiom (forall h: Heap, o: ref, f: Field int, T: name :: { h[o, AsRangeField(f, T)] } IsHeap(h) ==> InRange(h[o, AsRangeField(f, T)], T)); + +function $IsMemberlessType(name) returns (bool); + +axiom (forall o: ref :: { $IsMemberlessType($typeof(o)) } !$IsMemberlessType($typeof(o))); + +function $AsInterface(name) returns (name); + +axiom (forall $J: name, s: any, b: ref :: { UnboxedType(Box(s, b)) <: $AsInterface($J) } $AsInterface($J) == $J && Box(s, b) == b && UnboxedType(Box(s, b)) <: $AsInterface($J) ==> $typeof(b) <: $J); + +function $HeapSucc(oldHeap: Heap, newHeap: Heap) returns (bool); + +function $IsImmutable(T: name) returns (bool); + +axiom !$IsImmutable(System.Object); + +function $AsImmutable(T: name) returns (theType: name); + +function $AsMutable(T: name) returns (theType: name); + +axiom (forall T: name, U: name :: { U <: $AsImmutable(T) } U <: $AsImmutable(T) ==> $IsImmutable(U) && $AsImmutable(U) == U); + +axiom (forall T: name, U: name :: { U <: $AsMutable(T) } U <: $AsMutable(T) ==> !$IsImmutable(U) && $AsMutable(U) == U); + +function AsOwner(string: ref, owner: ref) returns (theString: ref); + +axiom (forall o: ref, T: name :: { $typeof(o) <: $AsImmutable(T) } o != null && o != $BeingConstructed && $typeof(o) <: $AsImmutable(T) ==> (forall h: Heap :: { IsHeap(h) } IsHeap(h) ==> h[o, $inv] == $typeof(o) && h[o, $localinv] == $typeof(o) && h[o, $ownerFrame] == $PeerGroupPlaceholder && AsOwner(o, h[o, $ownerRef]) == o && (forall t: ref :: { AsOwner(o, h[t, $ownerRef]) } AsOwner(o, h[t, $ownerRef]) == o ==> t == o || h[t, $ownerFrame] != $PeerGroupPlaceholder))); + +const unique System.String: name; + +function $StringLength(ref) returns (int); + +axiom (forall s: ref :: { $StringLength(s) } 0 <= $StringLength(s)); + +function AsRepField(f: Field ref, declaringType: name) returns (theField: Field ref); + +axiom (forall h: Heap, o: ref, f: Field ref, T: name :: { h[o, AsRepField(f, T)] } IsHeap(h) && h[o, AsRepField(f, T)] != null ==> h[h[o, AsRepField(f, T)], $ownerRef] == o && h[h[o, AsRepField(f, T)], $ownerFrame] == T); + +function AsPeerField(f: Field ref) returns (theField: Field ref); + +axiom (forall h: Heap, o: ref, f: Field ref :: { h[o, AsPeerField(f)] } IsHeap(h) && h[o, AsPeerField(f)] != null ==> h[h[o, AsPeerField(f)], $ownerRef] == h[o, $ownerRef] && h[h[o, AsPeerField(f)], $ownerFrame] == h[o, $ownerFrame]); + +function AsElementsRepField(f: Field ref, declaringType: name, position: int) returns (theField: Field ref); + +axiom (forall h: Heap, o: ref, f: Field ref, T: name, i: int :: { h[o, AsElementsRepField(f, T, i)] } IsHeap(h) && h[o, AsElementsRepField(f, T, i)] != null ==> h[$ElementProxy(h[o, AsElementsRepField(f, T, i)], i), $ownerRef] == o && h[$ElementProxy(h[o, AsElementsRepField(f, T, i)], i), $ownerFrame] == T); + +function AsElementsPeerField(f: Field ref, position: int) returns (theField: Field ref); + +axiom (forall h: Heap, o: ref, f: Field ref, i: int :: { h[o, AsElementsPeerField(f, i)] } IsHeap(h) && h[o, AsElementsPeerField(f, i)] != null ==> h[$ElementProxy(h[o, AsElementsPeerField(f, i)], i), $ownerRef] == h[o, $ownerRef] && h[$ElementProxy(h[o, AsElementsPeerField(f, i)], i), $ownerFrame] == h[o, $ownerFrame]); + +axiom (forall h: Heap, o: ref :: { h[h[o, $ownerRef], $inv] <: h[o, $ownerFrame] } IsHeap(h) && h[o, $ownerFrame] != $PeerGroupPlaceholder && h[h[o, $ownerRef], $inv] <: h[o, $ownerFrame] && h[h[o, $ownerRef], $localinv] != $BaseClass(h[o, $ownerFrame]) ==> h[o, $inv] == $typeof(o) && h[o, $localinv] == $typeof(o)); + +procedure $SetOwner(o: ref, ow: ref, fr: name); + modifies $Heap; + ensures (forall p: ref, F: Field a :: { $Heap[p, F] } (F != $ownerRef && F != $ownerFrame) || old($Heap[p, $ownerRef] != $Heap[o, $ownerRef]) || old($Heap[p, $ownerFrame] != $Heap[o, $ownerFrame]) ==> old($Heap[p, F]) == $Heap[p, F]); + ensures (forall p: ref :: { $Heap[p, $ownerRef] } { $Heap[p, $ownerFrame] } old($Heap[p, $ownerRef] == $Heap[o, $ownerRef]) && old($Heap[p, $ownerFrame] == $Heap[o, $ownerFrame]) ==> $Heap[p, $ownerRef] == ow && $Heap[p, $ownerFrame] == fr); + free ensures $HeapSucc(old($Heap), $Heap); + + + +procedure $UpdateOwnersForRep(o: ref, T: name, e: ref); + modifies $Heap; + ensures (forall p: ref, F: Field a :: { $Heap[p, F] } (F != $ownerRef && F != $ownerFrame) || old($Heap[p, $ownerRef] != $Heap[e, $ownerRef]) || old($Heap[p, $ownerFrame] != $Heap[e, $ownerFrame]) ==> old($Heap[p, F]) == $Heap[p, F]); + ensures e == null ==> $Heap == old($Heap); + ensures e != null ==> (forall p: ref :: { $Heap[p, $ownerRef] } { $Heap[p, $ownerFrame] } old($Heap[p, $ownerRef] == $Heap[e, $ownerRef]) && old($Heap[p, $ownerFrame] == $Heap[e, $ownerFrame]) ==> $Heap[p, $ownerRef] == o && $Heap[p, $ownerFrame] == T); + free ensures $HeapSucc(old($Heap), $Heap); + + + +procedure $UpdateOwnersForPeer(c: ref, d: ref); + modifies $Heap; + ensures (forall p: ref, F: Field a :: { $Heap[p, F] } (F != $ownerRef && F != $ownerFrame) || old($Heap[p, $ownerRef] != $Heap[d, $ownerRef] || $Heap[p, $ownerFrame] != $Heap[d, $ownerFrame]) ==> old($Heap[p, F]) == $Heap[p, F]); + ensures d == null ==> $Heap == old($Heap); + ensures d != null ==> (forall p: ref :: { $Heap[p, $ownerRef] } { $Heap[p, $ownerFrame] } old($Heap[p, $ownerRef] == $Heap[d, $ownerRef] && $Heap[p, $ownerFrame] == $Heap[d, $ownerFrame]) ==> $Heap[p, $ownerRef] == old($Heap)[c, $ownerRef] && $Heap[p, $ownerFrame] == old($Heap)[c, $ownerFrame]); + free ensures $HeapSucc(old($Heap), $Heap); + + + +const unique $FirstConsistentOwner: Field ref; + +function $AsPureObject(ref) returns (ref); + +function ##FieldDependsOnFCO(o: ref, f: Field a, ev: exposeVersionType) returns (value: any); + +axiom (forall o: ref, f: Field a, h: Heap :: { h[$AsPureObject(o), f] } IsHeap(h) && o != null && h[o, $allocated] == true && $AsPureObject(o) == o && h[o, $ownerFrame] != $PeerGroupPlaceholder && h[h[o, $ownerRef], $inv] <: h[o, $ownerFrame] && h[h[o, $ownerRef], $localinv] != $BaseClass(h[o, $ownerFrame]) ==> h[o, f] == ##FieldDependsOnFCO(o, f, h[h[o, $FirstConsistentOwner], $exposeVersion])); + +axiom (forall o: ref, h: Heap :: { h[o, $FirstConsistentOwner] } IsHeap(h) && o != null && h[o, $allocated] == true && h[o, $ownerFrame] != $PeerGroupPlaceholder && h[h[o, $ownerRef], $inv] <: h[o, $ownerFrame] && h[h[o, $ownerRef], $localinv] != $BaseClass(h[o, $ownerFrame]) ==> h[o, $FirstConsistentOwner] != null && h[h[o, $FirstConsistentOwner], $allocated] == true && (h[h[o, $FirstConsistentOwner], $ownerFrame] == $PeerGroupPlaceholder || !(h[h[h[o, $FirstConsistentOwner], $ownerRef], $inv] <: h[h[o, $FirstConsistentOwner], $ownerFrame]) || h[h[h[o, $FirstConsistentOwner], $ownerRef], $localinv] == $BaseClass(h[h[o, $FirstConsistentOwner], $ownerFrame]))); + +function Box(a, ref) returns (ref); + +function Unbox(ref) returns (any); + +type NondetType; + +function MeldNondets(NondetType, any) returns (NondetType); + +function BoxFunc(value: a, typ: name) returns (boxedValue: ref); + +function AllocFunc(typ: name) returns (newValue: ref); + +function NewInstance(object: ref, occurrence: NondetType, activity: ActivityType) returns (newInstance: ref); + +axiom (forall value: any, typ: name, occurrence: NondetType, activity: ActivityType :: { NewInstance(BoxFunc(value, typ), occurrence, activity) } Box(value, NewInstance(BoxFunc(value, typ), occurrence, activity)) == NewInstance(BoxFunc(value, typ), occurrence, activity) && UnboxedType(NewInstance(BoxFunc(value, typ), occurrence, activity)) == typ); + +axiom (forall x: ref, typ: name, occurrence: NondetType, activity: ActivityType :: !$IsValueType(UnboxedType(x)) ==> NewInstance(BoxFunc(x, typ), occurrence, activity) == x); + +axiom (forall x: any, p: ref :: { Unbox(Box(x, p)) } Unbox(Box(x, p)) == x); + +function UnboxedType(ref) returns (name); + +axiom (forall p: ref :: { $IsValueType(UnboxedType(p)) } $IsValueType(UnboxedType(p)) ==> (forall heap: Heap, x: any :: { heap[Box(x, p), $inv] } IsHeap(heap) ==> heap[Box(x, p), $inv] == $typeof(Box(x, p)) && heap[Box(x, p), $localinv] == $typeof(Box(x, p)))); + +axiom (forall x: a, p: ref :: { UnboxedType(Box(x, p)) <: System.Object } UnboxedType(Box(x, p)) <: System.Object && Box(x, p) == p ==> x == p); + +function BoxTester(p: ref, typ: name) returns (ref); + +axiom (forall p: ref, typ: name :: { BoxTester(p, typ) } UnboxedType(p) == typ <==> BoxTester(p, typ) != null); + +axiom (forall p: ref, typ: name :: { BoxTester(p, typ) } BoxTester(p, typ) != null ==> Box(Unbox(p), p) == p); + +axiom (forall typ: name, occurrence: NondetType, activity: ActivityType :: { NewInstance(AllocFunc(typ), occurrence, activity) } $typeof(NewInstance(AllocFunc(typ), occurrence, activity)) == typ && NewInstance(AllocFunc(typ), occurrence, activity) != null); + +axiom (forall typ: name, occurrence: NondetType, activity: ActivityType, heap: Heap :: { heap[NewInstance(AllocFunc(typ), occurrence, activity), $allocated] } IsHeap(heap) ==> heap[NewInstance(AllocFunc(typ), occurrence, activity), $allocated]); + +const unique System.SByte: name; + +axiom $IsValueType(System.SByte); + +const unique System.Byte: name; + +axiom $IsValueType(System.Byte); + +const unique System.Int16: name; + +axiom $IsValueType(System.Int16); + +const unique System.UInt16: name; + +axiom $IsValueType(System.UInt16); + +const unique System.Int32: name; + +axiom $IsValueType(System.Int32); + +const unique System.UInt32: name; + +axiom $IsValueType(System.UInt32); + +const unique System.Int64: name; + +axiom $IsValueType(System.Int64); + +const unique System.UInt64: name; + +axiom $IsValueType(System.UInt64); + +const unique System.Char: name; + +axiom $IsValueType(System.Char); + +const unique System.UIntPtr: name; + +axiom $IsValueType(System.UIntPtr); + +const unique System.IntPtr: name; + +axiom $IsValueType(System.IntPtr); + +const int#m2147483648: int; + +const int#2147483647: int; + +const int#4294967295: int; + +const int#m9223372036854775808: int; + +const int#9223372036854775807: int; + +const int#18446744073709551615: int; + +axiom int#m9223372036854775808 < int#m2147483648; + +axiom int#m2147483648 < 0 - 100000; + +axiom 100000 < int#2147483647; + +axiom int#2147483647 < int#4294967295; + +axiom int#4294967295 < int#9223372036854775807; + +axiom int#9223372036854775807 < int#18446744073709551615; + +axiom int#m9223372036854775808 + 1 == 0 - int#9223372036854775807; + +axiom int#m2147483648 + 1 == 0 - int#2147483647; + +function InRange(i: int, T: name) returns (bool); + +axiom (forall i: int :: InRange(i, System.SByte) <==> 0 - 128 <= i && i < 128); + +axiom (forall i: int :: InRange(i, System.Byte) <==> 0 <= i && i < 256); + +axiom (forall i: int :: InRange(i, System.Int16) <==> 0 - 32768 <= i && i < 32768); + +axiom (forall i: int :: InRange(i, System.UInt16) <==> 0 <= i && i < 65536); + +axiom (forall i: int :: InRange(i, System.Int32) <==> int#m2147483648 <= i && i <= int#2147483647); + +axiom (forall i: int :: InRange(i, System.UInt32) <==> 0 <= i && i <= int#4294967295); + +axiom (forall i: int :: InRange(i, System.Int64) <==> int#m9223372036854775808 <= i && i <= int#9223372036854775807); + +axiom (forall i: int :: InRange(i, System.UInt64) <==> 0 <= i && i <= int#18446744073709551615); + +axiom (forall i: int :: InRange(i, System.Char) <==> 0 <= i && i < 65536); + +function $IntToInt(val: int, fromType: name, toType: name) returns (int); + +function $IntToReal(int, fromType: name, toType: name) returns (real); + +function $RealToInt(real, fromType: name, toType: name) returns (int); + +function $RealToReal(val: real, fromType: name, toType: name) returns (real); + +axiom (forall z: int, B: name, C: name :: InRange(z, C) ==> $IntToInt(z, B, C) == z); + +function $SizeIs(name, int) returns (bool); + +function $IfThenElse(bool, any, any) returns (any); + +axiom (forall b: bool, x: any, y: any :: { $IfThenElse(b, x, y) } b ==> $IfThenElse(b, x, y) == x); + +axiom (forall b: bool, x: any, y: any :: { $IfThenElse(b, x, y) } !b ==> $IfThenElse(b, x, y) == y); + +function #neg(int) returns (int); + +function #and(int, int) returns (int); + +function #or(int, int) returns (int); + +function #xor(int, int) returns (int); + +function #shl(int, int) returns (int); + +function #shr(int, int) returns (int); + +function #rneg(real) returns (real); + +function #radd(real, real) returns (real); + +function #rsub(real, real) returns (real); + +function #rmul(real, real) returns (real); + +function #rdiv(real, real) returns (real); + +function #rmod(real, real) returns (real); + +function #rLess(real, real) returns (bool); + +function #rAtmost(real, real) returns (bool); + +function #rEq(real, real) returns (bool); + +function #rNeq(real, real) returns (bool); + +function #rAtleast(real, real) returns (bool); + +function #rGreater(real, real) returns (bool); + +axiom (forall x: int, y: int :: { x % y } { x / y } x % y == x - x / y * y); + +axiom (forall x: int, y: int :: { x % y } 0 <= x && 0 < y ==> 0 <= x % y && x % y < y); + +axiom (forall x: int, y: int :: { x % y } 0 <= x && y < 0 ==> 0 <= x % y && x % y < 0 - y); + +axiom (forall x: int, y: int :: { x % y } x <= 0 && 0 < y ==> 0 - y < x % y && x % y <= 0); + +axiom (forall x: int, y: int :: { x % y } x <= 0 && y < 0 ==> y < x % y && x % y <= 0); + +axiom (forall x: int, y: int :: { (x + y) % y } 0 <= x && 0 <= y ==> (x + y) % y == x % y); + +axiom (forall x: int, y: int :: { (y + x) % y } 0 <= x && 0 <= y ==> (y + x) % y == x % y); + +axiom (forall x: int, y: int :: { (x - y) % y } 0 <= x - y && 0 <= y ==> (x - y) % y == x % y); + +axiom (forall a: int, b: int, d: int :: { a % d, b % d } 2 <= d && a % d == b % d && a < b ==> a + d <= b); + +axiom (forall x: int, y: int :: { #and(x, y) } 0 <= x || 0 <= y ==> 0 <= #and(x, y)); + +axiom (forall x: int, y: int :: { #or(x, y) } 0 <= x && 0 <= y ==> 0 <= #or(x, y) && #or(x, y) <= x + y); + +axiom (forall i: int :: { #shl(i, 0) } #shl(i, 0) == i); + +axiom (forall i: int, j: int :: { #shl(i, j) } 1 <= j ==> #shl(i, j) == #shl(i, j - 1) * 2); + +axiom (forall i: int, j: int :: { #shl(i, j) } 0 <= i && i < 32768 && 0 <= j && j <= 16 ==> 0 <= #shl(i, j) && #shl(i, j) <= int#2147483647); + +axiom (forall i: int :: { #shr(i, 0) } #shr(i, 0) == i); + +axiom (forall i: int, j: int :: { #shr(i, j) } 1 <= j ==> #shr(i, j) == #shr(i, j - 1) / 2); + +function #min(int, int) returns (int); + +function #max(int, int) returns (int); + +axiom (forall x: int, y: int :: { #min(x, y) } (#min(x, y) == x || #min(x, y) == y) && #min(x, y) <= x && #min(x, y) <= y); + +axiom (forall x: int, y: int :: { #max(x, y) } (#max(x, y) == x || #max(x, y) == y) && x <= #max(x, y) && y <= #max(x, y)); + +function #System.String.IsInterned$System.String$notnull(Heap, ref) returns (ref); + +function #System.String.Equals$System.String(Heap, ref, ref) returns (bool); + +function #System.String.Equals$System.String$System.String(Heap, ref, ref) returns (bool); + +function ##StringEquals(ref, ref) returns (bool); + +axiom (forall h: Heap, a: ref, b: ref :: { #System.String.Equals$System.String(h, a, b) } #System.String.Equals$System.String(h, a, b) == #System.String.Equals$System.String$System.String(h, a, b)); + +axiom (forall h: Heap, a: ref, b: ref :: { #System.String.Equals$System.String$System.String(h, a, b) } #System.String.Equals$System.String$System.String(h, a, b) == ##StringEquals(a, b) && #System.String.Equals$System.String$System.String(h, a, b) == ##StringEquals(b, a) && (a == b ==> ##StringEquals(a, b))); + +axiom (forall a: ref, b: ref, c: ref :: ##StringEquals(a, b) && ##StringEquals(b, c) ==> ##StringEquals(a, c)); + +axiom (forall h: Heap, a: ref, b: ref :: { #System.String.Equals$System.String$System.String(h, a, b) } a != null && b != null && #System.String.Equals$System.String$System.String(h, a, b) ==> #System.String.IsInterned$System.String$notnull(h, a) == #System.String.IsInterned$System.String$notnull(h, b)); + +const $UnknownRef: ref; + +const unique Bag.a: Field ref; + +const unique Bag.n: Field int; + +const unique Microsoft.Contracts.GuardException: name; + +const unique System.ICloneable: name; + +const unique Microsoft.Contracts.ObjectInvariantException: name; + +const unique System.Exception: name; + +const unique System.Collections.IEnumerable: name; + +const unique System.Collections.IList: name; + +const unique Microsoft.Contracts.ICheckedException: name; + +const unique System.Reflection.MemberInfo: name; + +const unique Bag: name; + +const unique System.Reflection.IReflect: name; + +const unique System.Runtime.InteropServices._MemberInfo: name; + +const unique System.Runtime.InteropServices._Type: name; + +const unique System.Collections.ICollection: name; + +const unique System.Runtime.InteropServices._Exception: name; + +const unique System.Runtime.Serialization.ISerializable: name; + +const unique System.Reflection.ICustomAttributeProvider: name; + +axiom !IsStaticField(Bag.n); + +axiom IncludeInMainFrameCondition(Bag.n); + +axiom $IncludedInModifiesStar(Bag.n); + +axiom DeclType222(Bag.n) == Bag; + +axiom AsRangeField(Bag.n, System.Int32) == Bag.n; + +axiom !IsStaticField(Bag.a); + +axiom IncludeInMainFrameCondition(Bag.a); + +axiom $IncludedInModifiesStar(Bag.a); + +axiom AsRepField(Bag.a, Bag) == Bag.a; + +axiom DeclType222(Bag.a) == Bag; + +axiom AsNonNullRefField(Bag.a, IntArray(System.Int32, 1)) == Bag.a; + +axiom Bag <: Bag; + +axiom $BaseClass(Bag) == System.Object && AsDirectSubClass(Bag, $BaseClass(Bag)) == Bag; + +axiom !$IsImmutable(Bag) && $AsMutable(Bag) == Bag; + +axiom System.Array <: System.Array; + +axiom $BaseClass(System.Array) == System.Object && AsDirectSubClass(System.Array, $BaseClass(System.Array)) == System.Array; + +axiom !$IsImmutable(System.Array) && $AsMutable(System.Array) == System.Array; + +axiom System.ICloneable <: System.ICloneable; + +axiom System.ICloneable <: System.Object; + +axiom $IsMemberlessType(System.ICloneable); + +axiom $AsInterface(System.ICloneable) == System.ICloneable; + +axiom System.Array <: System.ICloneable; + +axiom System.Collections.IList <: System.Collections.IList; + +axiom System.Collections.IList <: System.Object; + +axiom System.Collections.ICollection <: System.Collections.ICollection; + +axiom System.Collections.ICollection <: System.Object; + +axiom System.Collections.IEnumerable <: System.Collections.IEnumerable; + +axiom System.Collections.IEnumerable <: System.Object; + +axiom $IsMemberlessType(System.Collections.IEnumerable); + +axiom $AsInterface(System.Collections.IEnumerable) == System.Collections.IEnumerable; + +axiom System.Collections.ICollection <: System.Collections.IEnumerable; + +axiom $IsMemberlessType(System.Collections.ICollection); + +axiom $AsInterface(System.Collections.ICollection) == System.Collections.ICollection; + +axiom System.Collections.IList <: System.Collections.ICollection; + +axiom System.Collections.IList <: System.Collections.IEnumerable; + +axiom $IsMemberlessType(System.Collections.IList); + +axiom $AsInterface(System.Collections.IList) == System.Collections.IList; + +axiom System.Array <: System.Collections.IList; + +axiom System.Array <: System.Collections.ICollection; + +axiom System.Array <: System.Collections.IEnumerable; + +axiom $IsMemberlessType(System.Array); + +// System.Array object invariant +axiom (forall $oi: ref, $h: Heap :: { $h[$oi, $inv] <: System.Array } IsHeap($h) && $h[$oi, $inv] <: System.Array && $h[$oi, $localinv] != $BaseClass(System.Array) ==> true); + +// Bag object invariant +axiom (forall $oi: ref, $h: Heap :: { $h[$oi, $inv] <: Bag } IsHeap($h) && $h[$oi, $inv] <: Bag && $h[$oi, $localinv] != $BaseClass(Bag) ==> 0 <= $h[$oi, Bag.n] && $h[$oi, Bag.n] <= $Length($h[$oi, Bag.a])); + +procedure Bag.SpecSharp.CheckInvariant$System.Boolean(this: ref where $IsNotNull(this, Bag) && $Heap[this, $allocated], throwException$in: bool where true) returns ($result: bool where true); + // user-declared preconditions + requires ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame]) || $Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame])) && $Heap[this, $inv] == System.Object && $Heap[this, $localinv] == $typeof(this) && (forall $p: ref :: $p != null && $Heap[$p, $allocated] && $Heap[$p, $ownerRef] == this && $Heap[$p, $ownerFrame] == Bag ==> $Heap[$p, $inv] == $typeof($p) && $Heap[$p, $localinv] == $typeof($p)); + free requires $BeingConstructed == null; + free requires $PurityAxiomsCanBeAssumed; + modifies $Heap, $ActivityIndicator; + // newly allocated objects are fully valid + free ensures (forall $o: ref :: { $Heap[$o, $localinv] } { $Heap[$o, $inv] } $o != null && !old($Heap)[$o, $allocated] && $Heap[$o, $allocated] ==> $Heap[$o, $inv] == $typeof($o) && $Heap[$o, $localinv] == $typeof($o)); + // first consistent owner unchanged if its exposeVersion is + free ensures (forall $o: ref :: { $Heap[$o, $FirstConsistentOwner] } old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] ==> old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner]); + // frame condition + ensures (forall $o: ref, $f: Field a :: { $Heap[$o, $f] } IncludeInMainFrameCondition($f) && $o != null && old($Heap)[$o, $allocated] && (old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame]) || old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])) && old($o != this || !($typeof(this) <: DeclType222($f)) || !$IncludedInModifiesStar($f)) && old(true) ==> old($Heap)[$o, $f] == $Heap[$o, $f]); + free ensures $HeapSucc(old($Heap), $Heap); + // inv/localinv change only in blocks + free ensures (forall $o: ref :: { $Heap[$o, $localinv] } { $Heap[$o, $inv] } old($Heap)[$o, $allocated] ==> old($Heap)[$o, $inv] == $Heap[$o, $inv] && old($Heap)[$o, $localinv] == $Heap[$o, $localinv]); + free ensures (forall $o: ref :: { $Heap[$o, $allocated] } old($Heap)[$o, $allocated] ==> $Heap[$o, $allocated]) && (forall $ot: ref :: { $Heap[$ot, $ownerFrame] } { $Heap[$ot, $ownerRef] } old($Heap)[$ot, $allocated] && old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder ==> $Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef] && $Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]) && old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]; + free ensures (forall $o: ref :: { $Heap[$o, $sharingMode] } old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]); + + + +implementation Bag.SpecSharp.CheckInvariant$System.Boolean(this: ref, throwException$in: bool) returns ($result: bool) +{ + var throwException: bool where true, stack0i: int, stack1i: int, stack0b: bool, stack1o: ref, return.value: bool where true, stack50000o: ref, stack0o: ref, SS$Display.Return.Local: bool where true; + + entry: + throwException := throwException$in; + goto block2380; + + block2380: + goto block2482; + + block2482: + // ----- nop + // ----- load constant 0 + stack0i := 0; + // ----- load field + assert this != null; + stack1i := $Heap[this, Bag.n]; + // ----- binary operator + // ----- branch + goto true2482to2550, false2482to2414; + + true2482to2550: + assume stack0i > stack1i; + goto block2550; + + false2482to2414: + assume stack0i <= stack1i; + goto block2414; + + block2550: + // ----- copy + stack0b := throwException; + // ----- unary operator + // ----- branch + goto true2550to2584, false2550to2601; + + block2414: + // ----- load field + assert this != null; + stack0i := $Heap[this, Bag.n]; + // ----- load field + assert this != null; + stack1o := $Heap[this, Bag.a]; + // ----- unary operator + assert stack1o != null; + stack1i := $Length(stack1o); + // ----- unary operator + stack1i := $IntToInt(stack1i, System.UIntPtr, System.Int32); + // ----- binary operator + // ----- branch + goto true2414to2550, false2414to2465; + + true2414to2550: + assume stack0i > stack1i; + goto block2550; + + false2414to2465: + assume stack0i <= stack1i; + goto block2465; + + block2465: + // ----- branch + goto block2448; + + true2550to2584: + assume !stack0b; + goto block2584; + + false2550to2601: + assume stack0b; + goto block2601; + + block2584: + // ----- load constant 0 + return.value := false; + // ----- branch + goto block2567; + + block2601: + assume false; + // ----- new object + havoc stack50000o; + assume $Heap[stack50000o, $allocated] == false && stack50000o != null && $typeof(stack50000o) == Microsoft.Contracts.ObjectInvariantException; + assume $Heap[stack50000o, $ownerRef] == stack50000o && $Heap[stack50000o, $ownerFrame] == $PeerGroupPlaceholder; + // ----- call + assert stack50000o != null; + call Microsoft.Contracts.ObjectInvariantException..ctor(stack50000o); + // ----- copy + stack0o := stack50000o; + // ----- throw + assert stack0o != null; + assume false; + return; + + block2448: + // ----- load constant 1 + return.value := true; + // ----- branch + goto block2567; + + block2567: + // ----- copy + SS$Display.Return.Local := return.value; + // ----- copy + stack0b := return.value; + // ----- return + $result := stack0b; + return; +} + + + +axiom Microsoft.Contracts.ObjectInvariantException <: Microsoft.Contracts.ObjectInvariantException; + +axiom Microsoft.Contracts.GuardException <: Microsoft.Contracts.GuardException; + +axiom System.Exception <: System.Exception; + +axiom $BaseClass(System.Exception) == System.Object && AsDirectSubClass(System.Exception, $BaseClass(System.Exception)) == System.Exception; + +axiom !$IsImmutable(System.Exception) && $AsMutable(System.Exception) == System.Exception; + +axiom System.Runtime.Serialization.ISerializable <: System.Runtime.Serialization.ISerializable; + +axiom System.Runtime.Serialization.ISerializable <: System.Object; + +axiom $IsMemberlessType(System.Runtime.Serialization.ISerializable); + +axiom $AsInterface(System.Runtime.Serialization.ISerializable) == System.Runtime.Serialization.ISerializable; + +axiom System.Exception <: System.Runtime.Serialization.ISerializable; + +axiom System.Runtime.InteropServices._Exception <: System.Runtime.InteropServices._Exception; + +axiom System.Runtime.InteropServices._Exception <: System.Object; + +axiom $IsMemberlessType(System.Runtime.InteropServices._Exception); + +axiom $AsInterface(System.Runtime.InteropServices._Exception) == System.Runtime.InteropServices._Exception; + +axiom System.Exception <: System.Runtime.InteropServices._Exception; + +// System.Exception object invariant +axiom (forall $oi: ref, $h: Heap :: { $h[$oi, $inv] <: System.Exception } IsHeap($h) && $h[$oi, $inv] <: System.Exception && $h[$oi, $localinv] != $BaseClass(System.Exception) ==> true); + +axiom $BaseClass(Microsoft.Contracts.GuardException) == System.Exception && AsDirectSubClass(Microsoft.Contracts.GuardException, $BaseClass(Microsoft.Contracts.GuardException)) == Microsoft.Contracts.GuardException; + +axiom !$IsImmutable(Microsoft.Contracts.GuardException) && $AsMutable(Microsoft.Contracts.GuardException) == Microsoft.Contracts.GuardException; + +// Microsoft.Contracts.GuardException object invariant +axiom (forall $oi: ref, $h: Heap :: { $h[$oi, $inv] <: Microsoft.Contracts.GuardException } IsHeap($h) && $h[$oi, $inv] <: Microsoft.Contracts.GuardException && $h[$oi, $localinv] != $BaseClass(Microsoft.Contracts.GuardException) ==> true); + +axiom $BaseClass(Microsoft.Contracts.ObjectInvariantException) == Microsoft.Contracts.GuardException && AsDirectSubClass(Microsoft.Contracts.ObjectInvariantException, $BaseClass(Microsoft.Contracts.ObjectInvariantException)) == Microsoft.Contracts.ObjectInvariantException; + +axiom !$IsImmutable(Microsoft.Contracts.ObjectInvariantException) && $AsMutable(Microsoft.Contracts.ObjectInvariantException) == Microsoft.Contracts.ObjectInvariantException; + +// Microsoft.Contracts.ObjectInvariantException object invariant +axiom (forall $oi: ref, $h: Heap :: { $h[$oi, $inv] <: Microsoft.Contracts.ObjectInvariantException } IsHeap($h) && $h[$oi, $inv] <: Microsoft.Contracts.ObjectInvariantException && $h[$oi, $localinv] != $BaseClass(Microsoft.Contracts.ObjectInvariantException) ==> true); + +procedure Microsoft.Contracts.ObjectInvariantException..ctor(this: ref where $IsNotNull(this, Microsoft.Contracts.ObjectInvariantException) && $Heap[this, $allocated]); + // object is fully unpacked: this.inv == Object + free requires ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame]) || $Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame])) && $Heap[this, $inv] == System.Object && $Heap[this, $localinv] == $typeof(this); + // nothing is owned by [this,*] and 'this' is alone in its own peer group + free requires (forall $o: ref :: $o != this ==> $Heap[$o, $ownerRef] != this) && $Heap[this, $ownerRef] == this && $Heap[this, $ownerFrame] == $PeerGroupPlaceholder; + free requires $BeingConstructed == this; + free requires $PurityAxiomsCanBeAssumed; + modifies $Heap, $ActivityIndicator; + // target object is allocated upon return + free ensures $Heap[this, $allocated]; + // target object is additively exposable for Microsoft.Contracts.ObjectInvariantException + ensures ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame]) || $Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame])) && $Heap[this, $inv] == Microsoft.Contracts.ObjectInvariantException && $Heap[this, $localinv] == $typeof(this); + ensures $Heap[this, $ownerRef] == old($Heap)[this, $ownerRef] && $Heap[this, $ownerFrame] == old($Heap)[this, $ownerFrame]; + ensures $Heap[this, $sharingMode] == $SharingMode_Unshared; + // newly allocated objects are fully valid + free ensures (forall $o: ref :: { $Heap[$o, $localinv] } { $Heap[$o, $inv] } $o != null && !old($Heap)[$o, $allocated] && $Heap[$o, $allocated] ==> $Heap[$o, $inv] == $typeof($o) && $Heap[$o, $localinv] == $typeof($o)); + // first consistent owner unchanged if its exposeVersion is + free ensures (forall $o: ref :: { $Heap[$o, $FirstConsistentOwner] } old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] ==> old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner]); + // frame condition + ensures (forall $o: ref, $f: Field a :: { $Heap[$o, $f] } IncludeInMainFrameCondition($f) && $o != null && old($Heap)[$o, $allocated] && (old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame]) || old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])) && ($o != this || !(Microsoft.Contracts.ObjectInvariantException <: DeclType222($f))) && old(true) && old(true) ==> old($Heap)[$o, $f] == $Heap[$o, $f]); + free ensures $HeapSucc(old($Heap), $Heap); + // inv/localinv change only in blocks + free ensures (forall $o: ref :: { $Heap[$o, $localinv] } { $Heap[$o, $inv] } old($Heap)[$o, $allocated] && $o != this ==> old($Heap)[$o, $inv] == $Heap[$o, $inv] && old($Heap)[$o, $localinv] == $Heap[$o, $localinv]); + free ensures (forall $o: ref :: { $Heap[$o, $allocated] } old($Heap)[$o, $allocated] ==> $Heap[$o, $allocated]) && (forall $ot: ref :: { $Heap[$ot, $ownerFrame] } { $Heap[$ot, $ownerRef] } old($Heap)[$ot, $allocated] && old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder ==> $Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef] && $Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]) && old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]; + free ensures (forall $o: ref :: { $Heap[$o, $sharingMode] } $o == this || old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]); + + + +procedure Bag..ctor$System.Int32.array$notnull(this: ref where $IsNotNull(this, Bag) && $Heap[this, $allocated], initialElements$in: ref where $IsNotNull(initialElements$in, IntArray(System.Int32, 1)) && $Heap[initialElements$in, $allocated]); + // object is fully unpacked: this.inv == Object + free requires ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame]) || $Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame])) && $Heap[this, $inv] == System.Object && $Heap[this, $localinv] == $typeof(this); + // initialElements is peer consistent + requires (forall $pc: ref :: { $typeof($pc) } { $Heap[$pc, $localinv] } { $Heap[$pc, $inv] } { $Heap[$pc, $ownerFrame] } { $Heap[$pc, $ownerRef] } $pc != null && $Heap[$pc, $allocated] && $Heap[$pc, $ownerRef] == $Heap[initialElements$in, $ownerRef] && $Heap[$pc, $ownerFrame] == $Heap[initialElements$in, $ownerFrame] ==> $Heap[$pc, $inv] == $typeof($pc) && $Heap[$pc, $localinv] == $typeof($pc)); + // initialElements is peer consistent (owner must not be valid) + requires $Heap[initialElements$in, $ownerFrame] == $PeerGroupPlaceholder || !($Heap[$Heap[initialElements$in, $ownerRef], $inv] <: $Heap[initialElements$in, $ownerFrame]) || $Heap[$Heap[initialElements$in, $ownerRef], $localinv] == $BaseClass($Heap[initialElements$in, $ownerFrame]); + // nothing is owned by [this,*] and 'this' is alone in its own peer group + free requires (forall $o: ref :: $o != this ==> $Heap[$o, $ownerRef] != this) && $Heap[this, $ownerRef] == this && $Heap[this, $ownerFrame] == $PeerGroupPlaceholder; + free requires $BeingConstructed == this; + free requires $PurityAxiomsCanBeAssumed; + modifies $Heap, $ActivityIndicator; + // target object is allocated upon return + free ensures $Heap[this, $allocated]; + // target object is additively exposable for Bag + ensures ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame]) || $Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame])) && $Heap[this, $inv] == Bag && $Heap[this, $localinv] == $typeof(this); + ensures $Heap[this, $ownerRef] == old($Heap)[this, $ownerRef] && $Heap[this, $ownerFrame] == old($Heap)[this, $ownerFrame]; + ensures $Heap[this, $sharingMode] == $SharingMode_Unshared; + // newly allocated objects are fully valid + free ensures (forall $o: ref :: { $Heap[$o, $localinv] } { $Heap[$o, $inv] } $o != null && !old($Heap)[$o, $allocated] && $Heap[$o, $allocated] ==> $Heap[$o, $inv] == $typeof($o) && $Heap[$o, $localinv] == $typeof($o)); + // first consistent owner unchanged if its exposeVersion is + free ensures (forall $o: ref :: { $Heap[$o, $FirstConsistentOwner] } old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] ==> old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner]); + // frame condition + ensures (forall $o: ref, $f: Field a :: { $Heap[$o, $f] } IncludeInMainFrameCondition($f) && $o != null && old($Heap)[$o, $allocated] && (old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame]) || old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])) && ($o != this || !(Bag <: DeclType222($f))) && old(true) && old(true) ==> old($Heap)[$o, $f] == $Heap[$o, $f]); + free ensures $HeapSucc(old($Heap), $Heap); + // inv/localinv change only in blocks + free ensures (forall $o: ref :: { $Heap[$o, $localinv] } { $Heap[$o, $inv] } old($Heap)[$o, $allocated] && $o != this ==> old($Heap)[$o, $inv] == $Heap[$o, $inv] && old($Heap)[$o, $localinv] == $Heap[$o, $localinv]); + free ensures (forall $o: ref :: { $Heap[$o, $allocated] } old($Heap)[$o, $allocated] ==> $Heap[$o, $allocated]) && (forall $ot: ref :: { $Heap[$ot, $ownerFrame] } { $Heap[$ot, $ownerRef] } old($Heap)[$ot, $allocated] && old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder ==> $Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef] && $Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]) && old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]; + free ensures (forall $o: ref :: { $Heap[$o, $sharingMode] } $o == this || old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]); + + + +implementation Bag..ctor$System.Int32.array$notnull(this: ref, initialElements$in: ref) +{ + var initialElements: ref where $IsNotNull(initialElements, IntArray(System.Int32, 1)) && $Heap[initialElements, $allocated], stack0o: ref, stack0i: int, temp0: exposeVersionType, temp1: ref, temp2: exposeVersionType, stack1i: int, temp3: ref; + + entry: + initialElements := initialElements$in; + assume $Heap[this, Bag.n] == 0; + goto block3332; + + block3332: + goto block3468; + + block3468: + // ----- nop + // ----- copy ----- AddMethod.ssc(13,5) + stack0o := initialElements; + // ----- unary operator ----- AddMethod.ssc(13,5) + assert stack0o != null; + stack0i := $Length(stack0o); + // ----- unary operator ----- AddMethod.ssc(13,5) + stack0i := $IntToInt(stack0i, System.UIntPtr, System.Int32); + // ----- store field ----- AddMethod.ssc(13,5) + assert this != null; + assert $Heap[this, $ownerFrame] == $PeerGroupPlaceholder || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame]) || $Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]); + havoc temp0; + $Heap[this, $exposeVersion] := temp0; + $Heap[this, Bag.n] := stack0i; + assert !($Heap[this, $inv] <: Bag && $Heap[this, $localinv] != $BaseClass(Bag)) || 0 <= $Heap[this, Bag.n]; + assert !($Heap[this, $inv] <: Bag && $Heap[this, $localinv] != $BaseClass(Bag)) || $Heap[this, Bag.n] <= $Length($Heap[this, Bag.a]); + assume IsHeap($Heap); + // ----- copy ----- AddMethod.ssc(14,5) + stack0o := initialElements; + // ----- unary operator ----- AddMethod.ssc(14,5) + assert stack0o != null; + stack0i := $Length(stack0o); + // ----- unary operator ----- AddMethod.ssc(14,5) + stack0i := $IntToInt(stack0i, System.UIntPtr, System.Int32); + // ----- new array ----- AddMethod.ssc(14,5) + assert 0 <= stack0i; + havoc temp1; + assume $Heap[temp1, $allocated] == false && $Length(temp1) == stack0i; + assume $Heap[$ElementProxy(temp1, -1), $allocated] == false && $ElementProxy(temp1, -1) != temp1 && $ElementProxy(temp1, -1) != null; + assume temp1 != null; + assume $typeof(temp1) == IntArray(System.Int32, 1); + assume $Heap[temp1, $ownerRef] == temp1 && $Heap[temp1, $ownerFrame] == $PeerGroupPlaceholder; + assume $Heap[$ElementProxy(temp1, -1), $ownerRef] == $ElementProxy(temp1, -1) && $Heap[$ElementProxy(temp1, -1), $ownerFrame] == $PeerGroupPlaceholder; + assume $Heap[temp1, $inv] == $typeof(temp1) && $Heap[temp1, $localinv] == $typeof(temp1); + assume (forall $i: int :: IntArrayGet($Heap[temp1, $elements], $i) == 0); + $Heap[temp1, $allocated] := true; + call System.Object..ctor($ElementProxy(temp1, -1)); + stack0o := temp1; + assume IsHeap($Heap); + // ----- store field ----- AddMethod.ssc(14,5) + assert this != null; + assert $Heap[this, $ownerFrame] == $PeerGroupPlaceholder || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame]) || $Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]); + assert ($Heap[stack0o, $ownerRef] == this && $Heap[stack0o, $ownerFrame] == Bag) || $Heap[stack0o, $ownerFrame] == $PeerGroupPlaceholder; + assert $Heap[stack0o, $ownerFrame] == $PeerGroupPlaceholder && $Heap[this, $inv] <: Bag && $Heap[this, $localinv] != $BaseClass(Bag) ==> (forall $pc: ref :: { $typeof($pc) } { $Heap[$pc, $localinv] } { $Heap[$pc, $inv] } { $Heap[$pc, $ownerFrame] } { $Heap[$pc, $ownerRef] } $pc != null && $Heap[$pc, $allocated] && $Heap[$pc, $ownerRef] == $Heap[stack0o, $ownerRef] && $Heap[$pc, $ownerFrame] == $Heap[stack0o, $ownerFrame] ==> $Heap[$pc, $inv] == $typeof($pc) && $Heap[$pc, $localinv] == $typeof($pc)); + assert $Heap[stack0o, $ownerFrame] == $PeerGroupPlaceholder && $Heap[this, $inv] <: Bag && $Heap[this, $localinv] != $BaseClass(Bag) ==> $Heap[this, $ownerRef] != $Heap[stack0o, $ownerRef] || $Heap[this, $ownerFrame] != $Heap[stack0o, $ownerFrame]; + call $UpdateOwnersForRep(this, Bag, stack0o); + havoc temp2; + $Heap[this, $exposeVersion] := temp2; + $Heap[this, Bag.a] := stack0o; + assert !($Heap[this, $inv] <: Bag && $Heap[this, $localinv] != $BaseClass(Bag)) || 0 <= $Heap[this, Bag.n]; + assert !($Heap[this, $inv] <: Bag && $Heap[this, $localinv] != $BaseClass(Bag)) || $Heap[this, Bag.n] <= $Length($Heap[this, Bag.a]); + assume IsHeap($Heap); + // ----- call ----- AddMethod.ssc(15,5) + assert this != null; + call System.Object..ctor(this); + $Heap[this, $NonNullFieldsAreInitialized] := true; + assume IsHeap($Heap); + goto block3417; + + block3417: + // ----- load field ----- AddMethod.ssc(16,5) + assert this != null; + stack0o := $Heap[this, Bag.a]; + // ----- load constant 0 ----- AddMethod.ssc(16,5) + stack1i := 0; + // ----- call ----- AddMethod.ssc(16,5) + assert initialElements != null; + call System.Array.CopyTo$System.Array$notnull$System.Int32$.Virtual.$(initialElements, stack0o, stack1i); + // ----- FrameGuard processing ----- AddMethod.ssc(17,3) + temp3 := this; + // ----- classic pack ----- AddMethod.ssc(17,3) + assert temp3 != null; + assert $Heap[temp3, $inv] == System.Object && $Heap[temp3, $localinv] == $typeof(temp3); + assert 0 <= $Heap[temp3, Bag.n]; + assert $Heap[temp3, Bag.n] <= $Length($Heap[temp3, Bag.a]); + assert (forall $p: ref :: $p != null && $Heap[$p, $allocated] && $Heap[$p, $ownerRef] == temp3 && $Heap[$p, $ownerFrame] == Bag ==> $Heap[$p, $inv] == $typeof($p) && $Heap[$p, $localinv] == $typeof($p)); + $Heap[temp3, $inv] := Bag; + assume IsHeap($Heap); + // ----- return + return; +} + + + +procedure System.Object..ctor(this: ref where $IsNotNull(this, System.Object) && $Heap[this, $allocated]); + // object is fully unpacked: this.inv == Object + free requires ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame]) || $Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame])) && $Heap[this, $inv] == System.Object && $Heap[this, $localinv] == $typeof(this); + // nothing is owned by [this,*] and 'this' is alone in its own peer group + free requires (forall $o: ref :: $o != this ==> $Heap[$o, $ownerRef] != this) && $Heap[this, $ownerRef] == this && $Heap[this, $ownerFrame] == $PeerGroupPlaceholder; + free requires $BeingConstructed == this; + free requires $PurityAxiomsCanBeAssumed; + modifies $Heap, $ActivityIndicator; + // target object is allocated upon return + free ensures $Heap[this, $allocated]; + // target object is additively exposable for System.Object + ensures ($Heap[this, $ownerFrame] == $PeerGroupPlaceholder || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame]) || $Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame])) && $Heap[this, $inv] == System.Object && $Heap[this, $localinv] == $typeof(this); + ensures $Heap[this, $ownerRef] == old($Heap)[this, $ownerRef] && $Heap[this, $ownerFrame] == old($Heap)[this, $ownerFrame]; + ensures $Heap[this, $sharingMode] == $SharingMode_Unshared; + // newly allocated objects are fully valid + free ensures (forall $o: ref :: { $Heap[$o, $localinv] } { $Heap[$o, $inv] } $o != null && !old($Heap)[$o, $allocated] && $Heap[$o, $allocated] ==> $Heap[$o, $inv] == $typeof($o) && $Heap[$o, $localinv] == $typeof($o)); + // first consistent owner unchanged if its exposeVersion is + free ensures (forall $o: ref :: { $Heap[$o, $FirstConsistentOwner] } old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] ==> old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner]); + // frame condition + ensures (forall $o: ref, $f: Field a :: { $Heap[$o, $f] } IncludeInMainFrameCondition($f) && $o != null && old($Heap)[$o, $allocated] && (old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame]) || old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])) && ($o != this || !(System.Object <: DeclType222($f))) && old(true) && old(true) ==> old($Heap)[$o, $f] == $Heap[$o, $f]); + free ensures $HeapSucc(old($Heap), $Heap); + // inv/localinv change only in blocks + free ensures (forall $o: ref :: { $Heap[$o, $localinv] } { $Heap[$o, $inv] } old($Heap)[$o, $allocated] && $o != this ==> old($Heap)[$o, $inv] == $Heap[$o, $inv] && old($Heap)[$o, $localinv] == $Heap[$o, $localinv]); + free ensures (forall $o: ref :: { $Heap[$o, $allocated] } old($Heap)[$o, $allocated] ==> $Heap[$o, $allocated]) && (forall $ot: ref :: { $Heap[$ot, $ownerFrame] } { $Heap[$ot, $ownerRef] } old($Heap)[$ot, $allocated] && old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder ==> $Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef] && $Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]) && old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]; + free ensures (forall $o: ref :: { $Heap[$o, $sharingMode] } $o == this || old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]); + + + +procedure System.Array.CopyTo$System.Array$notnull$System.Int32$.Virtual.$(this: ref where $IsNotNull(this, System.Array) && $Heap[this, $allocated], array$in: ref where $IsNotNull(array$in, System.Array) && $Heap[array$in, $allocated], index$in: int where InRange(index$in, System.Int32)); + // user-declared preconditions + requires array$in != null; + requires $LBound(array$in, 0) <= index$in; + requires $Rank(this) == 1; + requires $Rank(array$in) == 1; + requires $Length(this) <= $UBound(array$in, 0) + 1 - index$in; + // target object is peer consistent + requires (forall $pc: ref :: { $typeof($pc) } { $Heap[$pc, $localinv] } { $Heap[$pc, $inv] } { $Heap[$pc, $ownerFrame] } { $Heap[$pc, $ownerRef] } $pc != null && $Heap[$pc, $allocated] && $Heap[$pc, $ownerRef] == $Heap[this, $ownerRef] && $Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame] ==> $Heap[$pc, $inv] == $typeof($pc) && $Heap[$pc, $localinv] == $typeof($pc)); + // target object is peer consistent (owner must not be valid) + requires $Heap[this, $ownerFrame] == $PeerGroupPlaceholder || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame]) || $Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]); + // array is peer consistent + requires (forall $pc: ref :: { $typeof($pc) } { $Heap[$pc, $localinv] } { $Heap[$pc, $inv] } { $Heap[$pc, $ownerFrame] } { $Heap[$pc, $ownerRef] } $pc != null && $Heap[$pc, $allocated] && $Heap[$pc, $ownerRef] == $Heap[array$in, $ownerRef] && $Heap[$pc, $ownerFrame] == $Heap[array$in, $ownerFrame] ==> $Heap[$pc, $inv] == $typeof($pc) && $Heap[$pc, $localinv] == $typeof($pc)); + // array is peer consistent (owner must not be valid) + requires $Heap[array$in, $ownerFrame] == $PeerGroupPlaceholder || !($Heap[$Heap[array$in, $ownerRef], $inv] <: $Heap[array$in, $ownerFrame]) || $Heap[$Heap[array$in, $ownerRef], $localinv] == $BaseClass($Heap[array$in, $ownerFrame]); + free requires $BeingConstructed == null; + free requires $PurityAxiomsCanBeAssumed; + modifies $Heap, $ActivityIndicator; + // hard-coded postcondition + ensures (forall $k: int :: { ValueArrayGet($Heap[array$in, $elements], $k) } (index$in <= $k && $k < index$in + $Length(this) ==> old(ValueArrayGet($Heap[this, $elements], $k + 0 - index$in)) == ValueArrayGet($Heap[array$in, $elements], $k)) && (!(index$in <= $k && $k < index$in + $Length(this)) ==> old(ValueArrayGet($Heap[array$in, $elements], $k)) == ValueArrayGet($Heap[array$in, $elements], $k))); + ensures (forall $k: int :: { IntArrayGet($Heap[array$in, $elements], $k) } (index$in <= $k && $k < index$in + $Length(this) ==> old(IntArrayGet($Heap[this, $elements], $k + 0 - index$in)) == IntArrayGet($Heap[array$in, $elements], $k)) && (!(index$in <= $k && $k < index$in + $Length(this)) ==> old(IntArrayGet($Heap[array$in, $elements], $k)) == IntArrayGet($Heap[array$in, $elements], $k))); + ensures (forall $k: int :: { RefArrayGet($Heap[array$in, $elements], $k) } (index$in <= $k && $k < index$in + $Length(this) ==> old(RefArrayGet($Heap[this, $elements], $k + 0 - index$in)) == RefArrayGet($Heap[array$in, $elements], $k)) && (!(index$in <= $k && $k < index$in + $Length(this)) ==> old(RefArrayGet($Heap[array$in, $elements], $k)) == RefArrayGet($Heap[array$in, $elements], $k))); + // newly allocated objects are fully valid + free ensures (forall $o: ref :: { $Heap[$o, $localinv] } { $Heap[$o, $inv] } $o != null && !old($Heap)[$o, $allocated] && $Heap[$o, $allocated] ==> $Heap[$o, $inv] == $typeof($o) && $Heap[$o, $localinv] == $typeof($o)); + // first consistent owner unchanged if its exposeVersion is + free ensures (forall $o: ref :: { $Heap[$o, $FirstConsistentOwner] } old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] ==> old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner]); + // frame condition + ensures (forall $o: ref, $f: Field a :: { $Heap[$o, $f] } IncludeInMainFrameCondition($f) && $o != null && old($Heap)[$o, $allocated] && (old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame]) || old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])) && old($o != array$in || !($typeof(array$in) <: DeclType222($f)) || !$IncludedInModifiesStar($f)) && old($o != array$in || $f != $exposeVersion) ==> old($Heap)[$o, $f] == $Heap[$o, $f]); + free ensures $HeapSucc(old($Heap), $Heap); + // inv/localinv change only in blocks + free ensures (forall $o: ref :: { $Heap[$o, $localinv] } { $Heap[$o, $inv] } old($Heap)[$o, $allocated] ==> old($Heap)[$o, $inv] == $Heap[$o, $inv] && old($Heap)[$o, $localinv] == $Heap[$o, $localinv]); + free ensures (forall $o: ref :: { $Heap[$o, $allocated] } old($Heap)[$o, $allocated] ==> $Heap[$o, $allocated]) && (forall $ot: ref :: { $Heap[$ot, $ownerFrame] } { $Heap[$ot, $ownerRef] } old($Heap)[$ot, $allocated] && old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder ==> $Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef] && $Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]) && old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]; + free ensures (forall $o: ref :: { $Heap[$o, $sharingMode] } old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]); + + + +procedure Bag.Add$System.Int32(this: ref where $IsNotNull(this, Bag) && $Heap[this, $allocated], x$in: int where InRange(x$in, System.Int32)); + // target object is peer consistent + requires (forall $pc: ref :: { $typeof($pc) } { $Heap[$pc, $localinv] } { $Heap[$pc, $inv] } { $Heap[$pc, $ownerFrame] } { $Heap[$pc, $ownerRef] } $pc != null && $Heap[$pc, $allocated] && $Heap[$pc, $ownerRef] == $Heap[this, $ownerRef] && $Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame] ==> $Heap[$pc, $inv] == $typeof($pc) && $Heap[$pc, $localinv] == $typeof($pc)); + // target object is peer consistent (owner must not be valid) + requires $Heap[this, $ownerFrame] == $PeerGroupPlaceholder || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame]) || $Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]); + free requires $BeingConstructed == null; + free requires $PurityAxiomsCanBeAssumed; + modifies $Heap, $ActivityIndicator; + // newly allocated objects are fully valid + free ensures (forall $o: ref :: { $Heap[$o, $localinv] } { $Heap[$o, $inv] } $o != null && !old($Heap)[$o, $allocated] && $Heap[$o, $allocated] ==> $Heap[$o, $inv] == $typeof($o) && $Heap[$o, $localinv] == $typeof($o)); + // first consistent owner unchanged if its exposeVersion is + free ensures (forall $o: ref :: { $Heap[$o, $FirstConsistentOwner] } old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] ==> old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner]); + // frame condition + ensures (forall $o: ref, $f: Field a :: { $Heap[$o, $f] } IncludeInMainFrameCondition($f) && $o != null && old($Heap)[$o, $allocated] && (old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame]) || old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])) && old($o != this || !($typeof(this) <: DeclType222($f)) || !$IncludedInModifiesStar($f)) && old($o != this || $f != $exposeVersion) ==> old($Heap)[$o, $f] == $Heap[$o, $f]); + free ensures $HeapSucc(old($Heap), $Heap); + // inv/localinv change only in blocks + free ensures (forall $o: ref :: { $Heap[$o, $localinv] } { $Heap[$o, $inv] } old($Heap)[$o, $allocated] ==> old($Heap)[$o, $inv] == $Heap[$o, $inv] && old($Heap)[$o, $localinv] == $Heap[$o, $localinv]); + free ensures (forall $o: ref :: { $Heap[$o, $allocated] } old($Heap)[$o, $allocated] ==> $Heap[$o, $allocated]) && (forall $ot: ref :: { $Heap[$ot, $ownerFrame] } { $Heap[$ot, $ownerRef] } old($Heap)[$ot, $allocated] && old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder ==> $Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef] && $Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]) && old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]; + free ensures (forall $o: ref :: { $Heap[$o, $sharingMode] } old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]); + + + +implementation Bag.Add$System.Int32(this: ref, x$in: int) +{ + var x: int where InRange(x, System.Int32), temp0: ref, stack1s: struct, stack1o: ref, temp1: exposeVersionType, local2: ref where $Is(local2, System.Exception) && $Heap[local2, $allocated], stack0i: int, stack1i: int, stack0b: bool, b: ref where $Is(b, IntArray(System.Int32, 1)) && $Heap[b, $allocated], temp2: ref, stack0o: ref, stack2o: ref, stack3i: int, stack4o: ref, stack4i: int, temp3: exposeVersionType, local4: int where InRange(local4, System.Int32), temp4: exposeVersionType, stack0s: struct; + + entry: + x := x$in; + goto block4335; + + block4335: + goto block4488; + + block4488: + // ----- nop + // ----- FrameGuard processing ----- AddMethod.ssc(22,13) + temp0 := this; + // ----- load token ----- AddMethod.ssc(22,13) + havoc stack1s; + assume $IsTokenForType(stack1s, Bag); + // ----- statically resolved GetTypeFromHandle call ----- AddMethod.ssc(22,13) + stack1o := TypeObject(Bag); + // ----- local unpack ----- AddMethod.ssc(22,13) + assert temp0 != null; + assert ($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame]) || $Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame])) && $Heap[temp0, $inv] <: Bag && $Heap[temp0, $localinv] == $typeof(temp0); + $Heap[temp0, $localinv] := System.Object; + havoc temp1; + $Heap[temp0, $exposeVersion] := temp1; + assume IsHeap($Heap); + local2 := null; + goto block4505; + + block4505: + // ----- load field ----- AddMethod.ssc(24,7) + assert this != null; + stack0i := $Heap[this, Bag.n]; + // ----- load field ----- AddMethod.ssc(24,7) + assert this != null; + stack1o := $Heap[this, Bag.a]; + // ----- unary operator ----- AddMethod.ssc(24,7) + assert stack1o != null; + stack1i := $Length(stack1o); + // ----- unary operator ----- AddMethod.ssc(24,7) + stack1i := $IntToInt(stack1i, System.UIntPtr, System.Int32); + // ----- binary operator ----- AddMethod.ssc(24,7) + // ----- branch ----- AddMethod.ssc(24,7) + goto true4505to4539, false4505to4522; + + true4505to4539: + assume stack0i != stack1i; + goto block4539; + + false4505to4522: + assume stack0i == stack1i; + goto block4522; + + block4539: + // ----- load field ----- AddMethod.ssc(30,7) + assert this != null; + stack0o := $Heap[this, Bag.a]; + // ----- load field ----- AddMethod.ssc(30,7) + assert this != null; + stack1i := $Heap[this, Bag.n]; + // ----- store element ----- AddMethod.ssc(30,7) + assert stack0o != null; + assert 0 <= stack1i; + assert stack1i < $Length(stack0o); + assert $Heap[stack0o, $ownerFrame] == $PeerGroupPlaceholder || !($Heap[$Heap[stack0o, $ownerRef], $inv] <: $Heap[stack0o, $ownerFrame]) || $Heap[$Heap[stack0o, $ownerRef], $localinv] == $BaseClass($Heap[stack0o, $ownerFrame]); + $Heap[stack0o, $elements] := IntArraySet($Heap[stack0o, $elements], stack1i, x); + assume IsHeap($Heap); + // ----- load field ----- AddMethod.ssc(31,7) + assert this != null; + local4 := $Heap[this, Bag.n]; + // ----- load constant 1 ----- AddMethod.ssc(31,7) + stack0i := 1; + // ----- binary operator ----- AddMethod.ssc(31,7) + stack0i := local4 + stack0i; + // ----- store field ----- AddMethod.ssc(31,7) + assert this != null; + assert $Heap[this, $ownerFrame] == $PeerGroupPlaceholder || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame]) || $Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]); + havoc temp4; + $Heap[this, $exposeVersion] := temp4; + $Heap[this, Bag.n] := stack0i; + assert !($Heap[this, $inv] <: Bag && $Heap[this, $localinv] != $BaseClass(Bag)) || 0 <= $Heap[this, Bag.n]; + assert !($Heap[this, $inv] <: Bag && $Heap[this, $localinv] != $BaseClass(Bag)) || $Heap[this, Bag.n] <= $Length($Heap[this, Bag.a]); + assume IsHeap($Heap); + // ----- copy + stack0i := local4; + // ----- branch + goto block4658; + + block4522: + // ----- load constant 2 ----- AddMethod.ssc(26,15) + stack0i := 2; + // ----- load field ----- AddMethod.ssc(26,15) + assert this != null; + stack1o := $Heap[this, Bag.a]; + // ----- unary operator ----- AddMethod.ssc(26,15) + assert stack1o != null; + stack1i := $Length(stack1o); + // ----- unary operator ----- AddMethod.ssc(26,15) + stack1i := $IntToInt(stack1i, System.UIntPtr, System.Int32); + // ----- binary operator ----- AddMethod.ssc(26,15) + stack0i := stack0i * stack1i; + // ----- load constant 1 ----- AddMethod.ssc(26,15) + stack1i := 1; + // ----- binary operator ----- AddMethod.ssc(26,15) + stack0i := stack0i + stack1i; + // ----- new array ----- AddMethod.ssc(26,15) + assert 0 <= stack0i; + havoc temp2; + assume $Heap[temp2, $allocated] == false && $Length(temp2) == stack0i; + assume $Heap[$ElementProxy(temp2, -1), $allocated] == false && $ElementProxy(temp2, -1) != temp2 && $ElementProxy(temp2, -1) != null; + assume temp2 != null; + assume $typeof(temp2) == IntArray(System.Int32, 1); + assume $Heap[temp2, $ownerRef] == temp2 && $Heap[temp2, $ownerFrame] == $PeerGroupPlaceholder; + assume $Heap[$ElementProxy(temp2, -1), $ownerRef] == $ElementProxy(temp2, -1) && $Heap[$ElementProxy(temp2, -1), $ownerFrame] == $PeerGroupPlaceholder; + assume $Heap[temp2, $inv] == $typeof(temp2) && $Heap[temp2, $localinv] == $typeof(temp2); + assume (forall $i: int :: IntArrayGet($Heap[temp2, $elements], $i) == 0); + $Heap[temp2, $allocated] := true; + call System.Object..ctor($ElementProxy(temp2, -1)); + b := temp2; + assume IsHeap($Heap); + // ----- load field ----- AddMethod.ssc(27,9) + assert this != null; + stack0o := $Heap[this, Bag.a]; + // ----- load constant 0 ----- AddMethod.ssc(27,9) + stack1i := 0; + // ----- copy ----- AddMethod.ssc(27,9) + stack2o := b; + // ----- load constant 0 ----- AddMethod.ssc(27,9) + stack3i := 0; + // ----- load field ----- AddMethod.ssc(27,9) + assert this != null; + stack4o := $Heap[this, Bag.a]; + // ----- unary operator ----- AddMethod.ssc(27,9) + assert stack4o != null; + stack4i := $Length(stack4o); + // ----- unary operator ----- AddMethod.ssc(27,9) + stack4i := $IntToInt(stack4i, System.UIntPtr, System.Int32); + // ----- call ----- AddMethod.ssc(27,9) + call System.Array.Copy$System.Array$notnull$System.Int32$System.Array$notnull$System.Int32$System.Int32(stack0o, stack1i, stack2o, stack3i, stack4i); + // ----- store field ----- AddMethod.ssc(28,9) + assert this != null; + assert $Heap[this, $ownerFrame] == $PeerGroupPlaceholder || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame]) || $Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]); + assert ($Heap[b, $ownerRef] == this && $Heap[b, $ownerFrame] == Bag) || $Heap[b, $ownerFrame] == $PeerGroupPlaceholder; + assert $Heap[b, $ownerFrame] == $PeerGroupPlaceholder && $Heap[this, $inv] <: Bag && $Heap[this, $localinv] != $BaseClass(Bag) ==> (forall $pc: ref :: { $typeof($pc) } { $Heap[$pc, $localinv] } { $Heap[$pc, $inv] } { $Heap[$pc, $ownerFrame] } { $Heap[$pc, $ownerRef] } $pc != null && $Heap[$pc, $allocated] && $Heap[$pc, $ownerRef] == $Heap[b, $ownerRef] && $Heap[$pc, $ownerFrame] == $Heap[b, $ownerFrame] ==> $Heap[$pc, $inv] == $typeof($pc) && $Heap[$pc, $localinv] == $typeof($pc)); + assert $Heap[b, $ownerFrame] == $PeerGroupPlaceholder && $Heap[this, $inv] <: Bag && $Heap[this, $localinv] != $BaseClass(Bag) ==> $Heap[this, $ownerRef] != $Heap[b, $ownerRef] || $Heap[this, $ownerFrame] != $Heap[b, $ownerFrame]; + call $UpdateOwnersForRep(this, Bag, b); + havoc temp3; + $Heap[this, $exposeVersion] := temp3; + $Heap[this, Bag.a] := b; + assert !($Heap[this, $inv] <: Bag && $Heap[this, $localinv] != $BaseClass(Bag)) || 0 <= $Heap[this, Bag.n]; + assert !($Heap[this, $inv] <: Bag && $Heap[this, $localinv] != $BaseClass(Bag)) || $Heap[this, Bag.n] <= $Length($Heap[this, Bag.a]); + assume IsHeap($Heap); + goto block4539; + + block4658: + stack0o := null; + // ----- binary operator + // ----- branch + goto true4658to4624, false4658to4641; + + true4658to4624: + assume local2 == stack0o; + goto block4624; + + false4658to4641: + assume local2 != stack0o; + goto block4641; + + block4624: + // ----- load token ----- AddMethod.ssc(32,5) + havoc stack0s; + assume $IsTokenForType(stack0s, Bag); + // ----- statically resolved GetTypeFromHandle call ----- AddMethod.ssc(32,5) + stack0o := TypeObject(Bag); + // ----- local pack ----- AddMethod.ssc(32,5) + assert temp0 != null; + assert $Heap[temp0, $localinv] == System.Object; + assert 0 <= $Heap[temp0, Bag.n]; + assert $Heap[temp0, Bag.n] <= $Length($Heap[temp0, Bag.a]); + assert (forall $p: ref :: $p != null && $Heap[$p, $allocated] && $Heap[$p, $ownerRef] == temp0 && $Heap[$p, $ownerFrame] == Bag ==> $Heap[$p, $inv] == $typeof($p) && $Heap[$p, $localinv] == $typeof($p)); + $Heap[temp0, $localinv] := $typeof(temp0); + assume IsHeap($Heap); + goto block4726; + + block4641: + // ----- is instance + // ----- branch + goto true4641to4624, false4641to4692; + + true4641to4624: + assume $As(local2, Microsoft.Contracts.ICheckedException) != null; + goto block4624; + + false4641to4692: + assume $As(local2, Microsoft.Contracts.ICheckedException) == null; + goto block4692; + + block4692: + // ----- branch + goto block4726; + + block4726: + // ----- nop + // ----- branch + goto block4590; + + block4590: + // ----- return + return; +} + + + +axiom System.Type <: System.Type; + +axiom System.Reflection.MemberInfo <: System.Reflection.MemberInfo; + +axiom $BaseClass(System.Reflection.MemberInfo) == System.Object && AsDirectSubClass(System.Reflection.MemberInfo, $BaseClass(System.Reflection.MemberInfo)) == System.Reflection.MemberInfo; + +axiom $IsImmutable(System.Reflection.MemberInfo) && $AsImmutable(System.Reflection.MemberInfo) == System.Reflection.MemberInfo; + +axiom System.Reflection.ICustomAttributeProvider <: System.Reflection.ICustomAttributeProvider; + +axiom System.Reflection.ICustomAttributeProvider <: System.Object; + +axiom $IsMemberlessType(System.Reflection.ICustomAttributeProvider); + +axiom $AsInterface(System.Reflection.ICustomAttributeProvider) == System.Reflection.ICustomAttributeProvider; + +axiom System.Reflection.MemberInfo <: System.Reflection.ICustomAttributeProvider; + +axiom System.Runtime.InteropServices._MemberInfo <: System.Runtime.InteropServices._MemberInfo; + +axiom System.Runtime.InteropServices._MemberInfo <: System.Object; + +axiom $IsMemberlessType(System.Runtime.InteropServices._MemberInfo); + +axiom $AsInterface(System.Runtime.InteropServices._MemberInfo) == System.Runtime.InteropServices._MemberInfo; + +axiom System.Reflection.MemberInfo <: System.Runtime.InteropServices._MemberInfo; + +axiom $IsMemberlessType(System.Reflection.MemberInfo); + +// System.Reflection.MemberInfo object invariant +axiom (forall $oi: ref, $h: Heap :: { $h[$oi, $inv] <: System.Reflection.MemberInfo } IsHeap($h) && $h[$oi, $inv] <: System.Reflection.MemberInfo && $h[$oi, $localinv] != $BaseClass(System.Reflection.MemberInfo) ==> true); + +axiom $BaseClass(System.Type) == System.Reflection.MemberInfo && AsDirectSubClass(System.Type, $BaseClass(System.Type)) == System.Type; + +axiom $IsImmutable(System.Type) && $AsImmutable(System.Type) == System.Type; + +axiom System.Runtime.InteropServices._Type <: System.Runtime.InteropServices._Type; + +axiom System.Runtime.InteropServices._Type <: System.Object; + +axiom $IsMemberlessType(System.Runtime.InteropServices._Type); + +axiom $AsInterface(System.Runtime.InteropServices._Type) == System.Runtime.InteropServices._Type; + +axiom System.Type <: System.Runtime.InteropServices._Type; + +axiom System.Reflection.IReflect <: System.Reflection.IReflect; + +axiom System.Reflection.IReflect <: System.Object; + +axiom $IsMemberlessType(System.Reflection.IReflect); + +axiom $AsInterface(System.Reflection.IReflect) == System.Reflection.IReflect; + +axiom System.Type <: System.Reflection.IReflect; + +axiom $IsMemberlessType(System.Type); + +// System.Type object invariant +axiom (forall $oi: ref, $h: Heap :: { $h[$oi, $inv] <: System.Type } IsHeap($h) && $h[$oi, $inv] <: System.Type && $h[$oi, $localinv] != $BaseClass(System.Type) ==> true); + +procedure System.Array.Copy$System.Array$notnull$System.Int32$System.Array$notnull$System.Int32$System.Int32(sourceArray$in: ref where $IsNotNull(sourceArray$in, System.Array) && $Heap[sourceArray$in, $allocated], sourceIndex$in: int where InRange(sourceIndex$in, System.Int32), destinationArray$in: ref where $IsNotNull(destinationArray$in, System.Array) && $Heap[destinationArray$in, $allocated], destinationIndex$in: int where InRange(destinationIndex$in, System.Int32), length$in: int where InRange(length$in, System.Int32)); + // user-declared preconditions + requires sourceArray$in != null; + requires destinationArray$in != null; + requires $Rank(sourceArray$in) == $Rank(destinationArray$in); + requires sourceIndex$in >= $LBound(sourceArray$in, 0); + requires destinationIndex$in >= $LBound(destinationArray$in, 0); + requires length$in >= 0; + requires sourceIndex$in + length$in <= $LBound(sourceArray$in, 0) + $Length(sourceArray$in); + requires destinationIndex$in + length$in <= $LBound(destinationArray$in, 0) + $Length(destinationArray$in); + // sourceArray is peer consistent + requires (forall $pc: ref :: { $typeof($pc) } { $Heap[$pc, $localinv] } { $Heap[$pc, $inv] } { $Heap[$pc, $ownerFrame] } { $Heap[$pc, $ownerRef] } $pc != null && $Heap[$pc, $allocated] && $Heap[$pc, $ownerRef] == $Heap[sourceArray$in, $ownerRef] && $Heap[$pc, $ownerFrame] == $Heap[sourceArray$in, $ownerFrame] ==> $Heap[$pc, $inv] == $typeof($pc) && $Heap[$pc, $localinv] == $typeof($pc)); + // sourceArray is peer consistent (owner must not be valid) + requires $Heap[sourceArray$in, $ownerFrame] == $PeerGroupPlaceholder || !($Heap[$Heap[sourceArray$in, $ownerRef], $inv] <: $Heap[sourceArray$in, $ownerFrame]) || $Heap[$Heap[sourceArray$in, $ownerRef], $localinv] == $BaseClass($Heap[sourceArray$in, $ownerFrame]); + // destinationArray is peer consistent + requires (forall $pc: ref :: { $typeof($pc) } { $Heap[$pc, $localinv] } { $Heap[$pc, $inv] } { $Heap[$pc, $ownerFrame] } { $Heap[$pc, $ownerRef] } $pc != null && $Heap[$pc, $allocated] && $Heap[$pc, $ownerRef] == $Heap[destinationArray$in, $ownerRef] && $Heap[$pc, $ownerFrame] == $Heap[destinationArray$in, $ownerFrame] ==> $Heap[$pc, $inv] == $typeof($pc) && $Heap[$pc, $localinv] == $typeof($pc)); + // destinationArray is peer consistent (owner must not be valid) + requires $Heap[destinationArray$in, $ownerFrame] == $PeerGroupPlaceholder || !($Heap[$Heap[destinationArray$in, $ownerRef], $inv] <: $Heap[destinationArray$in, $ownerFrame]) || $Heap[$Heap[destinationArray$in, $ownerRef], $localinv] == $BaseClass($Heap[destinationArray$in, $ownerFrame]); + free requires $BeingConstructed == null; + free requires $PurityAxiomsCanBeAssumed; + modifies $Heap, $ActivityIndicator; + // hard-coded postcondition + ensures (forall $k: int :: { ValueArrayGet($Heap[destinationArray$in, $elements], $k) } (destinationIndex$in <= $k && $k < destinationIndex$in + length$in ==> old(ValueArrayGet($Heap[sourceArray$in, $elements], $k + sourceIndex$in - destinationIndex$in)) == ValueArrayGet($Heap[destinationArray$in, $elements], $k)) && (!(destinationIndex$in <= $k && $k < destinationIndex$in + length$in) ==> old(ValueArrayGet($Heap[destinationArray$in, $elements], $k)) == ValueArrayGet($Heap[destinationArray$in, $elements], $k))); + ensures (forall $k: int :: { IntArrayGet($Heap[destinationArray$in, $elements], $k) } (destinationIndex$in <= $k && $k < destinationIndex$in + length$in ==> old(IntArrayGet($Heap[sourceArray$in, $elements], $k + sourceIndex$in - destinationIndex$in)) == IntArrayGet($Heap[destinationArray$in, $elements], $k)) && (!(destinationIndex$in <= $k && $k < destinationIndex$in + length$in) ==> old(IntArrayGet($Heap[destinationArray$in, $elements], $k)) == IntArrayGet($Heap[destinationArray$in, $elements], $k))); + ensures (forall $k: int :: { RefArrayGet($Heap[destinationArray$in, $elements], $k) } (destinationIndex$in <= $k && $k < destinationIndex$in + length$in ==> old(RefArrayGet($Heap[sourceArray$in, $elements], $k + sourceIndex$in - destinationIndex$in)) == RefArrayGet($Heap[destinationArray$in, $elements], $k)) && (!(destinationIndex$in <= $k && $k < destinationIndex$in + length$in) ==> old(RefArrayGet($Heap[destinationArray$in, $elements], $k)) == RefArrayGet($Heap[destinationArray$in, $elements], $k))); + // newly allocated objects are fully valid + free ensures (forall $o: ref :: { $Heap[$o, $localinv] } { $Heap[$o, $inv] } $o != null && !old($Heap)[$o, $allocated] && $Heap[$o, $allocated] ==> $Heap[$o, $inv] == $typeof($o) && $Heap[$o, $localinv] == $typeof($o)); + // first consistent owner unchanged if its exposeVersion is + free ensures (forall $o: ref :: { $Heap[$o, $FirstConsistentOwner] } old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] ==> old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner]); + // frame condition + ensures (forall $o: ref, $f: Field a :: { $Heap[$o, $f] } IncludeInMainFrameCondition($f) && $o != null && old($Heap)[$o, $allocated] && (old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame]) || old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])) && old($o != destinationArray$in || !($typeof(destinationArray$in) <: DeclType222($f)) || !$IncludedInModifiesStar($f)) && old($o != destinationArray$in || $f != $exposeVersion) ==> old($Heap)[$o, $f] == $Heap[$o, $f]); + free ensures $HeapSucc(old($Heap), $Heap); + // inv/localinv change only in blocks + free ensures (forall $o: ref :: { $Heap[$o, $localinv] } { $Heap[$o, $inv] } old($Heap)[$o, $allocated] ==> old($Heap)[$o, $inv] == $Heap[$o, $inv] && old($Heap)[$o, $localinv] == $Heap[$o, $localinv]); + free ensures (forall $o: ref :: { $Heap[$o, $allocated] } old($Heap)[$o, $allocated] ==> $Heap[$o, $allocated]) && (forall $ot: ref :: { $Heap[$ot, $ownerFrame] } { $Heap[$ot, $ownerRef] } old($Heap)[$ot, $allocated] && old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder ==> $Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef] && $Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]) && old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]; + free ensures (forall $o: ref :: { $Heap[$o, $sharingMode] } old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]); + + + +axiom Microsoft.Contracts.ICheckedException <: Microsoft.Contracts.ICheckedException; + +axiom Microsoft.Contracts.ICheckedException <: System.Object; + +axiom $IsMemberlessType(Microsoft.Contracts.ICheckedException); + +axiom $AsInterface(Microsoft.Contracts.ICheckedException) == Microsoft.Contracts.ICheckedException; + +procedure Bag.AddAgain$System.Int32(this: ref where $IsNotNull(this, Bag) && $Heap[this, $allocated], x$in: int where InRange(x$in, System.Int32)); + // target object is peer consistent + requires (forall $pc: ref :: { $typeof($pc) } { $Heap[$pc, $localinv] } { $Heap[$pc, $inv] } { $Heap[$pc, $ownerFrame] } { $Heap[$pc, $ownerRef] } $pc != null && $Heap[$pc, $allocated] && $Heap[$pc, $ownerRef] == $Heap[this, $ownerRef] && $Heap[$pc, $ownerFrame] == $Heap[this, $ownerFrame] ==> $Heap[$pc, $inv] == $typeof($pc) && $Heap[$pc, $localinv] == $typeof($pc)); + // target object is peer consistent (owner must not be valid) + requires $Heap[this, $ownerFrame] == $PeerGroupPlaceholder || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame]) || $Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]); + free requires $BeingConstructed == null; + free requires $PurityAxiomsCanBeAssumed; + modifies $Heap, $ActivityIndicator; + // newly allocated objects are fully valid + free ensures (forall $o: ref :: { $Heap[$o, $localinv] } { $Heap[$o, $inv] } $o != null && !old($Heap)[$o, $allocated] && $Heap[$o, $allocated] ==> $Heap[$o, $inv] == $typeof($o) && $Heap[$o, $localinv] == $typeof($o)); + // first consistent owner unchanged if its exposeVersion is + free ensures (forall $o: ref :: { $Heap[$o, $FirstConsistentOwner] } old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] ==> old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner]); + // frame condition + ensures (forall $o: ref, $f: Field a :: { $Heap[$o, $f] } IncludeInMainFrameCondition($f) && $o != null && old($Heap)[$o, $allocated] && (old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame]) || old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])) && old($o != this || !($typeof(this) <: DeclType222($f)) || !$IncludedInModifiesStar($f)) && old($o != this || $f != $exposeVersion) ==> old($Heap)[$o, $f] == $Heap[$o, $f]); + free ensures $HeapSucc(old($Heap), $Heap); + // inv/localinv change only in blocks + free ensures (forall $o: ref :: { $Heap[$o, $localinv] } { $Heap[$o, $inv] } old($Heap)[$o, $allocated] ==> old($Heap)[$o, $inv] == $Heap[$o, $inv] && old($Heap)[$o, $localinv] == $Heap[$o, $localinv]); + free ensures (forall $o: ref :: { $Heap[$o, $allocated] } old($Heap)[$o, $allocated] ==> $Heap[$o, $allocated]) && (forall $ot: ref :: { $Heap[$ot, $ownerFrame] } { $Heap[$ot, $ownerRef] } old($Heap)[$ot, $allocated] && old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder ==> $Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef] && $Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]) && old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]; + free ensures (forall $o: ref :: { $Heap[$o, $sharingMode] } old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]); + + + +implementation Bag.AddAgain$System.Int32(this: ref, x$in: int) +{ + var x: int where InRange(x, System.Int32), temp0: ref, stack1s: struct, stack1o: ref, temp1: exposeVersionType, local2: ref where $Is(local2, System.Exception) && $Heap[local2, $allocated], stack0i: int, stack1i: int, stack0b: bool, stack0o: ref, local4: int where InRange(local4, System.Int32), temp2: exposeVersionType, b: ref where $Is(b, IntArray(System.Int32, 1)) && $Heap[b, $allocated], temp3: ref, stack2i: int, temp4: exposeVersionType, stack0s: struct; + + entry: + x := x$in; + goto block6188; + + block6188: + goto block6341; + + block6341: + // ----- nop + // ----- FrameGuard processing ----- AddMethod.ssc(38,13) + temp0 := this; + // ----- load token ----- AddMethod.ssc(38,13) + havoc stack1s; + assume $IsTokenForType(stack1s, Bag); + // ----- statically resolved GetTypeFromHandle call ----- AddMethod.ssc(38,13) + stack1o := TypeObject(Bag); + // ----- local unpack ----- AddMethod.ssc(38,13) + assert temp0 != null; + assert ($Heap[temp0, $ownerFrame] == $PeerGroupPlaceholder || !($Heap[$Heap[temp0, $ownerRef], $inv] <: $Heap[temp0, $ownerFrame]) || $Heap[$Heap[temp0, $ownerRef], $localinv] == $BaseClass($Heap[temp0, $ownerFrame])) && $Heap[temp0, $inv] <: Bag && $Heap[temp0, $localinv] == $typeof(temp0); + $Heap[temp0, $localinv] := System.Object; + havoc temp1; + $Heap[temp0, $exposeVersion] := temp1; + assume IsHeap($Heap); + local2 := null; + goto block6358; + + block6358: + // ----- load field ----- AddMethod.ssc(40,7) + assert this != null; + stack0i := $Heap[this, Bag.n]; + // ----- load field ----- AddMethod.ssc(40,7) + assert this != null; + stack1o := $Heap[this, Bag.a]; + // ----- unary operator ----- AddMethod.ssc(40,7) + assert stack1o != null; + stack1i := $Length(stack1o); + // ----- unary operator ----- AddMethod.ssc(40,7) + stack1i := $IntToInt(stack1i, System.UIntPtr, System.Int32); + // ----- binary operator ----- AddMethod.ssc(40,7) + // ----- branch ----- AddMethod.ssc(40,7) + goto true6358to6392, false6358to6375; + + true6358to6392: + assume stack0i != stack1i; + goto block6392; + + false6358to6375: + assume stack0i == stack1i; + goto block6375; + + block6392: + // ----- load field ----- AddMethod.ssc(46,7) + assert this != null; + stack0o := $Heap[this, Bag.a]; + // ----- load field ----- AddMethod.ssc(46,7) + assert this != null; + stack1i := $Heap[this, Bag.n]; + // ----- store element ----- AddMethod.ssc(46,7) + assert stack0o != null; + assert 0 <= stack1i; + assert stack1i < $Length(stack0o); + assert $Heap[stack0o, $ownerFrame] == $PeerGroupPlaceholder || !($Heap[$Heap[stack0o, $ownerRef], $inv] <: $Heap[stack0o, $ownerFrame]) || $Heap[$Heap[stack0o, $ownerRef], $localinv] == $BaseClass($Heap[stack0o, $ownerFrame]); + $Heap[stack0o, $elements] := IntArraySet($Heap[stack0o, $elements], stack1i, x); + assume IsHeap($Heap); + // ----- load field ----- AddMethod.ssc(47,7) + assert this != null; + local4 := $Heap[this, Bag.n]; + // ----- load constant 1 ----- AddMethod.ssc(47,7) + stack0i := 1; + // ----- binary operator ----- AddMethod.ssc(47,7) + stack0i := local4 + stack0i; + // ----- store field ----- AddMethod.ssc(47,7) + assert this != null; + assert $Heap[this, $ownerFrame] == $PeerGroupPlaceholder || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame]) || $Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]); + havoc temp2; + $Heap[this, $exposeVersion] := temp2; + $Heap[this, Bag.n] := stack0i; + assert !($Heap[this, $inv] <: Bag && $Heap[this, $localinv] != $BaseClass(Bag)) || 0 <= $Heap[this, Bag.n]; + assert !($Heap[this, $inv] <: Bag && $Heap[this, $localinv] != $BaseClass(Bag)) || $Heap[this, Bag.n] <= $Length($Heap[this, Bag.a]); + assume IsHeap($Heap); + // ----- copy + stack0i := local4; + // ----- branch + goto block6562; + + block6375: + // ----- load constant 2 ----- AddMethod.ssc(42,15) + stack0i := 2; + // ----- load field ----- AddMethod.ssc(42,15) + assert this != null; + stack1o := $Heap[this, Bag.a]; + // ----- unary operator ----- AddMethod.ssc(42,15) + assert stack1o != null; + stack1i := $Length(stack1o); + // ----- unary operator ----- AddMethod.ssc(42,15) + stack1i := $IntToInt(stack1i, System.UIntPtr, System.Int32); + // ----- binary operator ----- AddMethod.ssc(42,15) + stack0i := stack0i * stack1i; + // ----- load constant 1 ----- AddMethod.ssc(42,15) + stack1i := 1; + // ----- binary operator ----- AddMethod.ssc(42,15) + stack0i := stack0i + stack1i; + // ----- new array ----- AddMethod.ssc(42,15) + assert 0 <= stack0i; + havoc temp3; + assume $Heap[temp3, $allocated] == false && $Length(temp3) == stack0i; + assume $Heap[$ElementProxy(temp3, -1), $allocated] == false && $ElementProxy(temp3, -1) != temp3 && $ElementProxy(temp3, -1) != null; + assume temp3 != null; + assume $typeof(temp3) == IntArray(System.Int32, 1); + assume $Heap[temp3, $ownerRef] == temp3 && $Heap[temp3, $ownerFrame] == $PeerGroupPlaceholder; + assume $Heap[$ElementProxy(temp3, -1), $ownerRef] == $ElementProxy(temp3, -1) && $Heap[$ElementProxy(temp3, -1), $ownerFrame] == $PeerGroupPlaceholder; + assume $Heap[temp3, $inv] == $typeof(temp3) && $Heap[temp3, $localinv] == $typeof(temp3); + assume (forall $i: int :: IntArrayGet($Heap[temp3, $elements], $i) == 0); + $Heap[temp3, $allocated] := true; + call System.Object..ctor($ElementProxy(temp3, -1)); + b := temp3; + assume IsHeap($Heap); + // ----- load field ----- AddMethod.ssc(43,9) + assert this != null; + stack0o := $Heap[this, Bag.a]; + // ----- copy ----- AddMethod.ssc(43,9) + stack1o := b; + // ----- load constant 0 ----- AddMethod.ssc(43,9) + stack2i := 0; + // ----- call ----- AddMethod.ssc(43,9) + assert stack0o != null; + call System.Array.CopyTo$System.Array$notnull$System.Int32$.Virtual.$(stack0o, stack1o, stack2i); + // ----- store field ----- AddMethod.ssc(44,9) + assert this != null; + assert $Heap[this, $ownerFrame] == $PeerGroupPlaceholder || !($Heap[$Heap[this, $ownerRef], $inv] <: $Heap[this, $ownerFrame]) || $Heap[$Heap[this, $ownerRef], $localinv] == $BaseClass($Heap[this, $ownerFrame]); + assert ($Heap[b, $ownerRef] == this && $Heap[b, $ownerFrame] == Bag) || $Heap[b, $ownerFrame] == $PeerGroupPlaceholder; + assert $Heap[b, $ownerFrame] == $PeerGroupPlaceholder && $Heap[this, $inv] <: Bag && $Heap[this, $localinv] != $BaseClass(Bag) ==> (forall $pc: ref :: { $typeof($pc) } { $Heap[$pc, $localinv] } { $Heap[$pc, $inv] } { $Heap[$pc, $ownerFrame] } { $Heap[$pc, $ownerRef] } $pc != null && $Heap[$pc, $allocated] && $Heap[$pc, $ownerRef] == $Heap[b, $ownerRef] && $Heap[$pc, $ownerFrame] == $Heap[b, $ownerFrame] ==> $Heap[$pc, $inv] == $typeof($pc) && $Heap[$pc, $localinv] == $typeof($pc)); + assert $Heap[b, $ownerFrame] == $PeerGroupPlaceholder && $Heap[this, $inv] <: Bag && $Heap[this, $localinv] != $BaseClass(Bag) ==> $Heap[this, $ownerRef] != $Heap[b, $ownerRef] || $Heap[this, $ownerFrame] != $Heap[b, $ownerFrame]; + call $UpdateOwnersForRep(this, Bag, b); + havoc temp4; + $Heap[this, $exposeVersion] := temp4; + $Heap[this, Bag.a] := b; + assert !($Heap[this, $inv] <: Bag && $Heap[this, $localinv] != $BaseClass(Bag)) || 0 <= $Heap[this, Bag.n]; + assert !($Heap[this, $inv] <: Bag && $Heap[this, $localinv] != $BaseClass(Bag)) || $Heap[this, Bag.n] <= $Length($Heap[this, Bag.a]); + assume IsHeap($Heap); + goto block6392; + + block6562: + stack0o := null; + // ----- binary operator + // ----- branch + goto true6562to6477, false6562to6579; + + true6562to6477: + assume local2 == stack0o; + goto block6477; + + false6562to6579: + assume local2 != stack0o; + goto block6579; + + block6477: + // ----- load token ----- AddMethod.ssc(48,5) + havoc stack0s; + assume $IsTokenForType(stack0s, Bag); + // ----- statically resolved GetTypeFromHandle call ----- AddMethod.ssc(48,5) + stack0o := TypeObject(Bag); + // ----- local pack ----- AddMethod.ssc(48,5) + assert temp0 != null; + assert $Heap[temp0, $localinv] == System.Object; + assert 0 <= $Heap[temp0, Bag.n]; + assert $Heap[temp0, Bag.n] <= $Length($Heap[temp0, Bag.a]); + assert (forall $p: ref :: $p != null && $Heap[$p, $allocated] && $Heap[$p, $ownerRef] == temp0 && $Heap[$p, $ownerFrame] == Bag ==> $Heap[$p, $inv] == $typeof($p) && $Heap[$p, $localinv] == $typeof($p)); + $Heap[temp0, $localinv] := $typeof(temp0); + assume IsHeap($Heap); + goto block6545; + + block6579: + // ----- is instance + // ----- branch + goto true6579to6477, false6579to6528; + + true6579to6477: + assume $As(local2, Microsoft.Contracts.ICheckedException) != null; + goto block6477; + + false6579to6528: + assume $As(local2, Microsoft.Contracts.ICheckedException) == null; + goto block6528; + + block6528: + // ----- branch + goto block6545; + + block6545: + // ----- nop + // ----- branch + goto block6443; + + block6443: + // ----- return + return; +} + + + +procedure Bag..cctor(); + free requires $BeingConstructed == null; + free requires $PurityAxiomsCanBeAssumed; + modifies $Heap, $ActivityIndicator; + // newly allocated objects are fully valid + free ensures (forall $o: ref :: { $Heap[$o, $localinv] } { $Heap[$o, $inv] } $o != null && !old($Heap)[$o, $allocated] && $Heap[$o, $allocated] ==> $Heap[$o, $inv] == $typeof($o) && $Heap[$o, $localinv] == $typeof($o)); + // first consistent owner unchanged if its exposeVersion is + free ensures (forall $o: ref :: { $Heap[$o, $FirstConsistentOwner] } old($Heap)[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] == $Heap[old($Heap)[$o, $FirstConsistentOwner], $exposeVersion] ==> old($Heap)[$o, $FirstConsistentOwner] == $Heap[$o, $FirstConsistentOwner]); + // frame condition + ensures (forall $o: ref, $f: Field a :: { $Heap[$o, $f] } IncludeInMainFrameCondition($f) && $o != null && old($Heap)[$o, $allocated] && (old($Heap)[$o, $ownerFrame] == $PeerGroupPlaceholder || !(old($Heap)[old($Heap)[$o, $ownerRef], $inv] <: old($Heap)[$o, $ownerFrame]) || old($Heap)[old($Heap)[$o, $ownerRef], $localinv] == $BaseClass(old($Heap)[$o, $ownerFrame])) && old(true) && old(true) ==> old($Heap)[$o, $f] == $Heap[$o, $f]); + free ensures $HeapSucc(old($Heap), $Heap); + // inv/localinv change only in blocks + free ensures (forall $o: ref :: { $Heap[$o, $localinv] } { $Heap[$o, $inv] } old($Heap)[$o, $allocated] ==> old($Heap)[$o, $inv] == $Heap[$o, $inv] && old($Heap)[$o, $localinv] == $Heap[$o, $localinv]); + free ensures (forall $o: ref :: { $Heap[$o, $allocated] } old($Heap)[$o, $allocated] ==> $Heap[$o, $allocated]) && (forall $ot: ref :: { $Heap[$ot, $ownerFrame] } { $Heap[$ot, $ownerRef] } old($Heap)[$ot, $allocated] && old($Heap)[$ot, $ownerFrame] != $PeerGroupPlaceholder ==> $Heap[$ot, $ownerRef] == old($Heap)[$ot, $ownerRef] && $Heap[$ot, $ownerFrame] == old($Heap)[$ot, $ownerFrame]) && old($Heap)[$BeingConstructed, $NonNullFieldsAreInitialized] == $Heap[$BeingConstructed, $NonNullFieldsAreInitialized]; + free ensures (forall $o: ref :: { $Heap[$o, $sharingMode] } old($Heap[$o, $sharingMode]) == $Heap[$o, $sharingMode]); + + + +implementation Bag..cctor() +{ + + entry: + goto block7650; + + block7650: + goto block7701; + + block7701: + // ----- nop + // ----- return + return; +} + + -- cgit v1.2.3