===========================================================
.___ __ __
_________________ __ __ __| _/|__|/ |_
/ ___\_` __ \__ \ | | \/ __ | | \\_ __\
/ /_/ > | \// __ \| | / /_/ | | || |
\___ /|__| (____ /____/\____ | |__||__|
/_____/ \/ \/
grep rough audit - static analysis tool
v2.8 written by @Wireghoul
=================================[justanotherhacker.com]===
boogie-2.4.1+dfsg/Source/Core/VCExp.cs-223- }
boogie-2.4.1+dfsg/Source/Core/VCExp.cs:224: Assembly asm = cce.NonNull(Assembly.LoadFrom(path));
boogie-2.4.1+dfsg/Source/Core/VCExp.cs-225- string name = cce.NonNull(asm.GetName().Name);
##############################################
boogie-2.4.1+dfsg/Source/ModelViewer/Main.resx-160- AAAAwQQABcEFAAXFBQAKwgoAFcAVAAWGSQBGlUYAUZNRAFiTWABKpkoATKdMAE25TQBXpFcAU7tTAFu1
boogie-2.4.1+dfsg/Source/ModelViewer/Main.resx:161: WwBmk2YAapRqAGqeagB5mHkAVKFkAG6nbgBsu2wACBuAAAoAkwAKCZYAChSSAAsYlgAaEJ8ACCSAAAsm
boogie-2.4.1+dfsg/Source/ModelViewer/Main.resx-162- nAAoO4gAODKVAAwHowALAKYACwCpAAwBqAAMBqgADACtAAsOqQAXDaMADACwAAwAtAAMDLEADQC5AA0A
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-115-axiom 0 < memLo && memLo <= memHi;
boogie-2.4.1+dfsg/Test/civl/GC.bpl:116:function {:inline} memAddr(i:int) returns (bool) { memLo <= i && i < memHi }
boogie-2.4.1+dfsg/Test/civl/GC.bpl-117-
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-121-axiom 0 <= numFields;
boogie-2.4.1+dfsg/Test/civl/GC.bpl:122:function {:inline} fieldAddr(i:int) returns (bool) { 0 <= i && i < numFields }
boogie-2.4.1+dfsg/Test/civl/GC.bpl-123-
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-125-axiom 0 <= numRoots;
boogie-2.4.1+dfsg/Test/civl/GC.bpl:126:function {:inline} rootAddr(i:int) returns (bool) { 0 <= i && i < numRoots }
boogie-2.4.1+dfsg/Test/civl/GC.bpl-127-
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-138-{
boogie-2.4.1+dfsg/Test/civl/GC.bpl:139: (forall x: int :: memAddr(x) <==> memAddrAbs(toAbs[x])) &&
boogie-2.4.1+dfsg/Test/civl/GC.bpl:140: (forall x: int, y: int :: toAbs[x] == toAbs[y] ==> x == y || (memAddr(x) && toAbs[x] == nil) || (memAddr(y) && toAbs[y] == nil)) &&
boogie-2.4.1+dfsg/Test/civl/GC.bpl:141: (forall x: idx :: rootAddr(x) ==> toAbs[root[x]] == rootAbs[x]) &&
boogie-2.4.1+dfsg/Test/civl/GC.bpl:142: (forall x: int, f: fld :: memAddr(x) && toAbs[x] != nil && fieldAddr(f) ==> toAbs[mem[x][f]] == memAbs[toAbs[x]][f]) &&
boogie-2.4.1+dfsg/Test/civl/GC.bpl:143: (forall x: int :: memAddr(x) && toAbs[x] != nil ==> allocSet[toAbs[x]]) &&
boogie-2.4.1+dfsg/Test/civl/GC.bpl:144: (forall x: idx :: rootAddr(x) && memAddr(root[x]) ==> toAbs[root[x]] != nil) &&
boogie-2.4.1+dfsg/Test/civl/GC.bpl:145: (forall x: int, f: fld :: memAddr(x) && toAbs[x] != nil && fieldAddr(f) && memAddr(mem[x][f]) ==> toAbs[mem[x][f]] != nil) &&
boogie-2.4.1+dfsg/Test/civl/GC.bpl:146: (forall x: int, f: fld :: memAddr(x) && Unalloc(Color[x]) ==> toAbs[x] == nil)
boogie-2.4.1+dfsg/Test/civl/GC.bpl-147-}
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-152-{
boogie-2.4.1+dfsg/Test/civl/GC.bpl:153: (forall i:int :: {MST(i)} MST(i) ==> (0 <= i && i < MarkStackPtr) ==> (memAddr(MarkStack[i]) && Gray(Color[MarkStack[i]]))) &&
boogie-2.4.1+dfsg/Test/civl/GC.bpl:154: (nodePeeked != 0 ==> memAddr(nodePeeked) && Gray(Color[nodePeeked])) &&
boogie-2.4.1+dfsg/Test/civl/GC.bpl:155: (forall i:int :: (memAddr(i) && Gray(Color[i])) ==> (exists j:int :: {MST(j)} MST(j) && 0 <= j && j < MarkStackPtr && MarkStack[j] == i) || nodePeeked == i) &&
boogie-2.4.1+dfsg/Test/civl/GC.bpl-156- (forall i:int :: {MST(i)} MST(i) ==> (0 <= i && i < MarkStackPtr) ==> (forall j:int :: {MST(j)} MST(j) ==> (0 <= j && j < MarkStackPtr && i != j) ==> MarkStack[i] != MarkStack[j])) &&
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-168- Iso(root, rootAbs, mem, memAbs, Color, toAbs, allocSet) &&
boogie-2.4.1+dfsg/Test/civl/GC.bpl:169: (forall x: int :: memAddr(x) ==> (toAbs[x] == nil <==> Unalloc(Color[x]))) &&
boogie-2.4.1+dfsg/Test/civl/GC.bpl:170: (forall x: int, f: fld :: memAddr(x) && Black(Color[x]) && fieldAddr(f) && memAddr(mem[x][f]) ==> Gray(Color[mem[x][f]]) || Black(Color[mem[x][f]]))
boogie-2.4.1+dfsg/Test/civl/GC.bpl-171-}
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-175- Iso(root, rootAbs, mem, memAbs, Color, toAbs, allocSet) &&
boogie-2.4.1+dfsg/Test/civl/GC.bpl:176: (forall x: int :: memAddr(x) ==> (toAbs[x] == nil <==> Unalloc(Color[x]))) &&
boogie-2.4.1+dfsg/Test/civl/GC.bpl:177: (forall x: int :: memAddr(x) ==> !Gray(Color[x])) &&
boogie-2.4.1+dfsg/Test/civl/GC.bpl:178: (forall x: int, f: fld :: memAddr(x) && Black(Color[x]) && fieldAddr(f) && memAddr(mem[x][f]) ==> Black(Color[mem[x][f]]))
boogie-2.4.1+dfsg/Test/civl/GC.bpl-179-}
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-183- Iso(root, rootAbs, mem, memAbs, Color, toAbs, allocSet) &&
boogie-2.4.1+dfsg/Test/civl/GC.bpl:184: (forall x: int :: memAddr(x) ==> (toAbs[x] != nil <==> Black(Color[x]))) &&
boogie-2.4.1+dfsg/Test/civl/GC.bpl:185: (forall x: int :: memAddr(x) ==> !Gray(Color[x])) &&
boogie-2.4.1+dfsg/Test/civl/GC.bpl:186: (forall x: int, f: fld :: memAddr(x) && Black(Color[x]) && fieldAddr(f) && memAddr(mem[x][f]) ==> Black(Color[mem[x][f]]))
boogie-2.4.1+dfsg/Test/civl/GC.bpl-187-}
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-192-requires {:layer 99} mutatorsInRootScanBarrier == MapConstBool(false);
boogie-2.4.1+dfsg/Test/civl/GC.bpl:193:requires {:layer 100} (forall x: idx :: rootAddr(x) ==> rootAbs[x] == Int(0));
boogie-2.4.1+dfsg/Test/civl/GC.bpl-194-ensures {:layer 99} mutatorsInRootScanBarrier == MapConstBool(false);
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-201- assert {:layer 99} mutatorsInRootScanBarrier == MapConstBool(false);
boogie-2.4.1+dfsg/Test/civl/GC.bpl:202: assert {:layer 100} (forall x: idx :: rootAddr(x) ==> rootAbs[x] == Int(0));
boogie-2.4.1+dfsg/Test/civl/GC.bpl-203-
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-221- havoc mem, root, Color, mutatorPhase;
boogie-2.4.1+dfsg/Test/civl/GC.bpl:222: assume (forall x: int, f: fld :: memAddr(x) && fieldAddr(f) ==> mem[x][f] == x);
boogie-2.4.1+dfsg/Test/civl/GC.bpl:223: assume (forall x: idx :: rootAddr(x) ==> root[x] == 0);
boogie-2.4.1+dfsg/Test/civl/GC.bpl:224: assume (forall i:int :: memAddr(i) ==> Color[i] == UNALLOC());
boogie-2.4.1+dfsg/Test/civl/GC.bpl-225- assume (forall i:int :: mutatorId(i) ==> mutatorPhase[i] == IDLE());
boogie-2.4.1+dfsg/Test/civl/GC.bpl:226: toAbs := (lambda i:int :: if memAddr(i) then nil else Int(i));
boogie-2.4.1+dfsg/Test/civl/GC.bpl-227- collectorPhase := IDLE();
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-239- invariant{:layer 96} memLo <= n && n <= memHi;
boogie-2.4.1+dfsg/Test/civl/GC.bpl:240: invariant{:layer 96} (forall i:int, f: fld :: memLo <= i && i < n && fieldAddr(f) ==> mem[i][f] == i);
boogie-2.4.1+dfsg/Test/civl/GC.bpl-241- {
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-244- invariant{:layer 96} 0 <= m && m <= numFields;
boogie-2.4.1+dfsg/Test/civl/GC.bpl:245: invariant{:layer 96} (forall i:int, f: fld :: memLo <= i && i < n && fieldAddr(f) ==> mem[i][f] == i);
boogie-2.4.1+dfsg/Test/civl/GC.bpl-246- invariant{:layer 96} (forall f: fld :: 0 <= f && f < m ==> mem[n][f] == n);
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-328- var o: obj;
boogie-2.4.1+dfsg/Test/civl/GC.bpl:329: assert mutatorTidWhole(tid) && rootAddr(y) && tidOwns(tid, y);
boogie-2.4.1+dfsg/Test/civl/GC.bpl-330- assume (memAddrAbs(o) && !allocSet[o]);
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-332- rootAbs[y] := o;
boogie-2.4.1+dfsg/Test/civl/GC.bpl:333: memAbs[o] := (lambda z: int :: if (fieldAddr(z)) then o else memAbs[o][z]);
boogie-2.4.1+dfsg/Test/civl/GC.bpl-334-}
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-394-modifies memAbs;
boogie-2.4.1+dfsg/Test/civl/GC.bpl:395:{ assert mutatorTidWhole(tid) && rootAddr(x) && tidOwns(tid, x) && fieldAddr(f) && rootAddr(y) && tidOwns(tid, y) && memAddrAbs(rootAbs[x]); memAbs[rootAbs[x]][f] := rootAbs[y]; }
boogie-2.4.1+dfsg/Test/civl/GC.bpl-396-
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-411- assert {:layer 100} Iso(root, rootAbs, mem, memAbs, Color, toAbs, allocSet);
boogie-2.4.1+dfsg/Test/civl/GC.bpl:412: assert {:layer 100} memAddr(root[y]) && MarkPhase(mutatorPhase[i#Tid(tid)]) ==> Gray(Color[root[y]]) || Black(Color[root[y]]);
boogie-2.4.1+dfsg/Test/civl/GC.bpl-413-
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-422-modifies rootAbs;
boogie-2.4.1+dfsg/Test/civl/GC.bpl:423:{ assert mutatorTidWhole(tid) && rootAddr(x) && tidOwns(tid, x) && fieldAddr(f) && rootAddr(y) && tidOwns(tid, y) && memAddrAbs(rootAbs[x]); rootAbs[y] := memAbs[rootAbs[x]][f]; }
boogie-2.4.1+dfsg/Test/civl/GC.bpl-424-
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-438-procedure {:atomic} {:layer 101} AtomicEq({:linear "tid"} tid:Tid, x: idx, y:idx) returns (isEqual:bool)
boogie-2.4.1+dfsg/Test/civl/GC.bpl:439:{ assert mutatorTidWhole(tid) && rootAddr(x) && tidOwns(tid, x) && rootAddr(y) && tidOwns(tid, y); isEqual := rootAbs[x] == rootAbs[y]; }
boogie-2.4.1+dfsg/Test/civl/GC.bpl-440-
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-508-requires {:layer 100} Iso(root, rootAbs, mem, memAbs, Color, toAbs, allocSet);
boogie-2.4.1+dfsg/Test/civl/GC.bpl:509:requires {:layer 100} (forall x: int :: memAddr(x) ==> (toAbs[x] == nil <==> Unalloc(Color[x])));
boogie-2.4.1+dfsg/Test/civl/GC.bpl:510:requires {:layer 100} sweepPtr == memHi ==> (forall x: int :: memAddr(x) ==> !Black(Color[x]));
boogie-2.4.1+dfsg/Test/civl/GC.bpl-511-requires {:layer 100}
boogie-2.4.1+dfsg/Test/civl/GC.bpl-512- sweepPtr == memLo ==>
boogie-2.4.1+dfsg/Test/civl/GC.bpl:513: (forall x: int :: memAddr(x) ==> !Gray(Color[x])) &&
boogie-2.4.1+dfsg/Test/civl/GC.bpl:514: (forall i: int :: rootAddr(i) && memAddr(root[i]) ==> Black(Color[root[i]])) &&
boogie-2.4.1+dfsg/Test/civl/GC.bpl:515: (forall x: int, f: fld :: memAddr(x) && Black(Color[x]) && fieldAddr(f) && memAddr(mem[x][f]) ==> Black(Color[mem[x][f]]));
boogie-2.4.1+dfsg/Test/civl/GC.bpl-516-ensures {:layer 98} MsWellFormed(MarkStack, MarkStackPtr, Color, 0);
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-518-ensures {:layer 100} Iso(root, rootAbs, mem, memAbs, Color, toAbs, allocSet);
boogie-2.4.1+dfsg/Test/civl/GC.bpl:519:ensures {:layer 100} (forall x: int :: memAddr(x) ==> (toAbs[x] == nil <==> Unalloc(Color[x])));
boogie-2.4.1+dfsg/Test/civl/GC.bpl:520:ensures {:layer 100} sweepPtr == memHi ==> (forall x: int :: memAddr(x) ==> !Black(Color[x]));
boogie-2.4.1+dfsg/Test/civl/GC.bpl-521-ensures {:layer 100}
boogie-2.4.1+dfsg/Test/civl/GC.bpl-522- sweepPtr == memLo ==>
boogie-2.4.1+dfsg/Test/civl/GC.bpl:523: (forall x: int :: memAddr(x) ==> !Gray(Color[x])) &&
boogie-2.4.1+dfsg/Test/civl/GC.bpl:524: (forall i: int :: rootAddr(i) && memAddr(root[i]) ==> Black(Color[root[i]])) &&
boogie-2.4.1+dfsg/Test/civl/GC.bpl:525: (forall x: int, f: fld :: memAddr(x) && Black(Color[x]) && fieldAddr(f) && memAddr(mem[x][f]) ==> Black(Color[mem[x][f]]));
boogie-2.4.1+dfsg/Test/civl/GC.bpl-526-ensures {:layer 97,99,100} old(collectorPhase) == collectorPhase;
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-534- assert {:layer 100} Iso(root, rootAbs, mem, memAbs, Color, toAbs, allocSet);
boogie-2.4.1+dfsg/Test/civl/GC.bpl:535: assert {:layer 100} (forall x: int :: memAddr(x) ==> (toAbs[x] == nil <==> Unalloc(Color[x])));
boogie-2.4.1+dfsg/Test/civl/GC.bpl:536: assert {:layer 100} sweepPtr == memHi ==> (forall x: int :: memAddr(x) ==> !Black(Color[x]));
boogie-2.4.1+dfsg/Test/civl/GC.bpl-537- assert {:layer 100}
boogie-2.4.1+dfsg/Test/civl/GC.bpl-538- sweepPtr == memLo ==>
boogie-2.4.1+dfsg/Test/civl/GC.bpl:539: (forall x: int :: memAddr(x) ==> !Gray(Color[x])) &&
boogie-2.4.1+dfsg/Test/civl/GC.bpl:540: (forall i: int :: rootAddr(i) && memAddr(root[i]) ==> Black(Color[root[i]])) &&
boogie-2.4.1+dfsg/Test/civl/GC.bpl:541: (forall x: int, f: fld :: memAddr(x) && Black(Color[x]) && fieldAddr(f) && memAddr(mem[x][f]) ==> Black(Color[mem[x][f]]));
boogie-2.4.1+dfsg/Test/civl/GC.bpl-542- assert {:layer 97,99,100} old(collectorPhase) == collectorPhase;
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-551-requires {:layer 100} Iso(root, rootAbs, mem, memAbs, Color, toAbs, allocSet);
boogie-2.4.1+dfsg/Test/civl/GC.bpl:552:requires {:layer 100} (forall x: int :: memAddr(x) ==> (toAbs[x] == nil <==> Unalloc(Color[x])));
boogie-2.4.1+dfsg/Test/civl/GC.bpl-553-requires {:layer 98,100} IdlePhase(collectorPhase) && PhaseConsistent(collectorPhase, mutatorPhase);
boogie-2.4.1+dfsg/Test/civl/GC.bpl:554:requires {:layer 100} (forall x: int :: memAddr(x) ==> !Black(Color[x]));
boogie-2.4.1+dfsg/Test/civl/GC.bpl-555-requires {:layer 100} sweepPtr == memHi;
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-564- invariant {:layer 100} Iso(root, rootAbs, mem, memAbs, Color, toAbs, allocSet);
boogie-2.4.1+dfsg/Test/civl/GC.bpl:565: invariant {:layer 100} (forall x: int :: memAddr(x) ==> (toAbs[x] == nil <==> Unalloc(Color[x])));
boogie-2.4.1+dfsg/Test/civl/GC.bpl:566: invariant {:layer 100} (forall x: int :: memAddr(x) ==> !Black(Color[x]));
boogie-2.4.1+dfsg/Test/civl/GC.bpl-567- invariant {:layer 100} sweepPtr == memHi;
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-593-requires {:layer 100} Iso(root, rootAbs, mem, memAbs, Color, toAbs, allocSet);
boogie-2.4.1+dfsg/Test/civl/GC.bpl:594:requires {:layer 100} (forall x: int :: memAddr(x) ==> (toAbs[x] == nil <==> Unalloc(Color[x])));
boogie-2.4.1+dfsg/Test/civl/GC.bpl:595:requires {:layer 100} (forall x: int :: memAddr(x) ==> !Black(Color[x]));
boogie-2.4.1+dfsg/Test/civl/GC.bpl-596-ensures {:layer 98} MsWellFormed(MarkStack, MarkStackPtr, Color, 0);
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-600-ensures {:layer 100} Iso(root, rootAbs, mem, memAbs, Color, toAbs, allocSet);
boogie-2.4.1+dfsg/Test/civl/GC.bpl:601:ensures {:layer 100} (forall x: int :: memAddr(x) ==> (toAbs[x] == nil <==> Unalloc(Color[x])));
boogie-2.4.1+dfsg/Test/civl/GC.bpl:602:ensures {:layer 100} (forall x: int :: memAddr(x) ==> !Black(Color[x]));
boogie-2.4.1+dfsg/Test/civl/GC.bpl-603-{
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-610- assert {:layer 100} Iso(root, rootAbs, mem, memAbs, Color, toAbs, allocSet);
boogie-2.4.1+dfsg/Test/civl/GC.bpl:611: assert {:layer 100} (forall x: int :: memAddr(x) ==> (toAbs[x] == nil <==> Unalloc(Color[x])));
boogie-2.4.1+dfsg/Test/civl/GC.bpl:612: assert {:layer 100} (forall x: int :: memAddr(x) ==> !Black(Color[x]));
boogie-2.4.1+dfsg/Test/civl/GC.bpl-613-}
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-625-ensures {:layer 100} MarkInv(root, rootAbs, mem, memAbs, Color, toAbs, allocSet);
boogie-2.4.1+dfsg/Test/civl/GC.bpl:626:ensures {:layer 100} (forall x: int :: memAddr(x) && !Unalloc(old(Color)[x]) ==> !Unalloc(Color[x]));
boogie-2.4.1+dfsg/Test/civl/GC.bpl:627:ensures {:layer 100} (forall x: int :: memAddr(x) && !Unalloc(old(Color)[x]) && !White(old(Color)[x]) ==> !White(Color[x]));
boogie-2.4.1+dfsg/Test/civl/GC.bpl-628-{
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-635- assert {:layer 100} MarkInv(root, rootAbs, mem, memAbs, Color, toAbs, allocSet);
boogie-2.4.1+dfsg/Test/civl/GC.bpl:636: assert {:layer 100} (forall x: int :: memAddr(x) && !Unalloc(old(Color)[x]) ==> !Unalloc(Color[x]));
boogie-2.4.1+dfsg/Test/civl/GC.bpl:637: assert {:layer 100} (forall x: int :: memAddr(x) && !Unalloc(old(Color)[x]) && !White(old(Color)[x]) ==> !White(Color[x]));
boogie-2.4.1+dfsg/Test/civl/GC.bpl-638-}
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-645-requires {:layer 100} MarkInv(root, rootAbs, mem, memAbs, Color, toAbs, allocSet);
boogie-2.4.1+dfsg/Test/civl/GC.bpl:646:requires {:layer 100} (forall x: int :: memAddr(x) ==> !Gray(Color[x]));
boogie-2.4.1+dfsg/Test/civl/GC.bpl:647:requires {:layer 100} (forall i: int :: rootAddr(i) && memAddr(root[i]) ==> Black(Color[root[i]]));
boogie-2.4.1+dfsg/Test/civl/GC.bpl-648-ensures {:layer 98} MsWellFormed(MarkStack, MarkStackPtr, Color, 0);
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-652-ensures {:layer 100} MarkInv(root, rootAbs, mem, memAbs, Color, toAbs, allocSet);
boogie-2.4.1+dfsg/Test/civl/GC.bpl:653:ensures {:layer 100} (forall x: int :: memAddr(x) ==> !Gray(Color[x]));
boogie-2.4.1+dfsg/Test/civl/GC.bpl:654:ensures {:layer 100} (forall i: int :: rootAddr(i) && memAddr(root[i]) ==> Black(Color[root[i]]));
boogie-2.4.1+dfsg/Test/civl/GC.bpl-655-{
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-662- assert {:layer 100} MarkInv(root, rootAbs, mem, memAbs, Color, toAbs, allocSet);
boogie-2.4.1+dfsg/Test/civl/GC.bpl:663: assert {:layer 100} (forall x: int :: memAddr(x) ==> !Gray(Color[x]));
boogie-2.4.1+dfsg/Test/civl/GC.bpl:664: assert {:layer 100} (forall i: int :: rootAddr(i) && memAddr(root[i]) ==> Black(Color[root[i]]));
boogie-2.4.1+dfsg/Test/civl/GC.bpl-665-}
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-671-requires {:layer 100} Iso(root, rootAbs, mem, memAbs, Color, toAbs, allocSet);
boogie-2.4.1+dfsg/Test/civl/GC.bpl:672:requires {:layer 100} (forall x: int :: memAddr(x) ==> (toAbs[x] == nil <==> Unalloc(Color[x])));
boogie-2.4.1+dfsg/Test/civl/GC.bpl:673:requires {:layer 100} (forall x: int :: memAddr(x) ==> !Black(Color[x]));
boogie-2.4.1+dfsg/Test/civl/GC.bpl-674-requires {:layer 100} MarkPhase(collectorPhase) && PhaseConsistent(collectorPhase, mutatorPhase) && sweepPtr == memHi;
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-679-ensures {:layer 100} MarkInv(root, rootAbs, mem, memAbs, Color, toAbs, allocSet);
boogie-2.4.1+dfsg/Test/civl/GC.bpl:680:ensures {:layer 100} (forall x: int :: memAddr(x) ==> !Gray(Color[x]));
boogie-2.4.1+dfsg/Test/civl/GC.bpl:681:ensures {:layer 100} (forall i: int :: rootAddr(i) && memAddr(root[i]) ==> Black(Color[root[i]]));
boogie-2.4.1+dfsg/Test/civl/GC.bpl-682-{
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-743- invariant {:layer 100} 0 <= fldIter && fldIter <= numFields;
boogie-2.4.1+dfsg/Test/civl/GC.bpl:744: invariant {:layer 100} (forall x: int :: 0 <= x && x < fldIter && memAddr(mem[nodeProcessed][x]) ==> !Unalloc(Color[mem[nodeProcessed][x]]) && !White(Color[mem[nodeProcessed][x]]));
boogie-2.4.1+dfsg/Test/civl/GC.bpl-745- {
boogie-2.4.1+dfsg/Test/civl/GC.bpl-746- call child := ReadFieldCollector(tid, nodeProcessed, fldIter);
boogie-2.4.1+dfsg/Test/civl/GC.bpl:747: if (memAddr(child))
boogie-2.4.1+dfsg/Test/civl/GC.bpl-748- {
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-759- assert {:layer 100} MarkInv(root, rootAbs, mem, memAbs, Color, toAbs, allocSet);
boogie-2.4.1+dfsg/Test/civl/GC.bpl:760: assert {:layer 100} (forall x: int :: 0 <= x && x < fldIter && memAddr(mem[nodeProcessed][x]) ==> !Unalloc(Color[mem[nodeProcessed][x]]) && !White(Color[mem[nodeProcessed][x]]));
boogie-2.4.1+dfsg/Test/civl/GC.bpl-761- }
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-772- havoc Color;
boogie-2.4.1+dfsg/Test/civl/GC.bpl:773: assume (forall u: int :: if memAddr(u) && White(old(Color)[u]) && (exists k: int :: rootAddr(k) && root[k] == u) then Color[u] == GRAY() else Color[u] == old(Color)[u]);
boogie-2.4.1+dfsg/Test/civl/GC.bpl:774: canStop := (forall v: int :: memAddr(v) ==> !Gray(Color[v]));
boogie-2.4.1+dfsg/Test/civl/GC.bpl-775-}
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-807- invariant {:layer 99} 0 <= i && i <= numRoots;
boogie-2.4.1+dfsg/Test/civl/GC.bpl:808: invariant {:layer 99} Color == (lambda u: int :: if memAddr(u) && White(snapColor[u]) && (exists k: int :: 0 <= k && k < i && root[k] == u) then GRAY() else snapColor[u]);
boogie-2.4.1+dfsg/Test/civl/GC.bpl-809- invariant {:layer 98} MsWellFormed(MarkStack, MarkStackPtr, Color, 0);
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-812- call o := ReadRootInRootScanBarrier(tid, i);
boogie-2.4.1+dfsg/Test/civl/GC.bpl:813: if (memAddr(o))
boogie-2.4.1+dfsg/Test/civl/GC.bpl-814- {
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-835-requires {:layer 100} isInit ==> SweepInvInit(root, rootAbs, mem, memAbs, Color, toAbs, allocSet);
boogie-2.4.1+dfsg/Test/civl/GC.bpl:836:requires {:layer 100} (forall i: int :: rootAddr(i) && memAddr(root[i]) ==> Black(Color[root[i]]));
boogie-2.4.1+dfsg/Test/civl/GC.bpl:837:requires {:layer 100} (forall x: int, f: fld :: memLo <= x && x < localSweepPtr && (Unalloc(Color[x]) || White(Color[x])) && fieldAddr(f) ==> mem[x][f] == x);
boogie-2.4.1+dfsg/Test/civl/GC.bpl-838-requires {:layer 100} (forall f: fld :: 0 <= f && f < fldIter ==> mem[localSweepPtr][f] == localSweepPtr);
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-844-ensures {:layer 100} isInit ==> SweepInvInit(root, rootAbs, mem, memAbs, Color, toAbs, allocSet);
boogie-2.4.1+dfsg/Test/civl/GC.bpl:845:ensures {:layer 100} (forall i: int :: rootAddr(i) && memAddr(root[i]) ==> Black(Color[root[i]]));
boogie-2.4.1+dfsg/Test/civl/GC.bpl-846-ensures {:layer 100} sweepPtr == memLo;
boogie-2.4.1+dfsg/Test/civl/GC.bpl:847:ensures {:layer 100} (forall x: int :: memAddr(x) && !Unalloc(old(Color)[x]) ==> old(Color)[x] == Color[x]);
boogie-2.4.1+dfsg/Test/civl/GC.bpl:848:ensures {:layer 100} (forall x: int, f: fld :: memLo <= x && x < localSweepPtr && (Unalloc(Color[x]) || White(Color[x])) && fieldAddr(f) ==> mem[x][f] == x);
boogie-2.4.1+dfsg/Test/civl/GC.bpl-849-ensures {:layer 100} (forall f: fld :: 0 <= f && f < fldIter ==> mem[localSweepPtr][f] == localSweepPtr);
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-859- assert {:layer 100} isInit ==> SweepInvInit(root, rootAbs, mem, memAbs, Color, toAbs, allocSet);
boogie-2.4.1+dfsg/Test/civl/GC.bpl:860: assert {:layer 100} (forall i: int :: rootAddr(i) && memAddr(root[i]) ==> Black(Color[root[i]]));
boogie-2.4.1+dfsg/Test/civl/GC.bpl:861: assert {:layer 100} (forall x: int :: memAddr(x) && !Unalloc(old(Color)[x]) ==> old(Color)[x] == Color[x]);
boogie-2.4.1+dfsg/Test/civl/GC.bpl:862: assert {:layer 100} (forall x: int, f: fld :: memLo <= x && x < localSweepPtr && (Unalloc(Color[x]) || White(Color[x])) && fieldAddr(f) ==> mem[x][f] == x);
boogie-2.4.1+dfsg/Test/civl/GC.bpl-863- assert {:layer 100} (forall f: fld :: 0 <= f && f < fldIter ==> mem[localSweepPtr][f] == localSweepPtr);
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-873-requires {:layer 100} SweepInv(root, rootAbs, mem, memAbs, Color, toAbs, allocSet);
boogie-2.4.1+dfsg/Test/civl/GC.bpl:874:requires {:layer 100} (forall x: int :: memAddr(x) ==> !Black(Color[x]));
boogie-2.4.1+dfsg/Test/civl/GC.bpl-875-ensures {:layer 98} MsWellFormed(MarkStack, MarkStackPtr, Color, 0);
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-878-ensures {:layer 100} SweepInv(root, rootAbs, mem, memAbs, Color, toAbs, allocSet);
boogie-2.4.1+dfsg/Test/civl/GC.bpl:879:ensures {:layer 100} (forall x: int :: memAddr(x) ==> !Black(Color[x]));
boogie-2.4.1+dfsg/Test/civl/GC.bpl-880-ensures {:layer 100} sweepPtr == memHi;
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-887- assert {:layer 100} SweepInv(root, rootAbs, mem, memAbs, Color, toAbs, allocSet);
boogie-2.4.1+dfsg/Test/civl/GC.bpl:888: assert {:layer 100} (forall x: int :: memAddr(x) ==> !Black(Color[x]));
boogie-2.4.1+dfsg/Test/civl/GC.bpl-889- assert {:layer 100} sweepPtr == memHi;
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-897-requires {:layer 100} sweepPtr == memLo;
boogie-2.4.1+dfsg/Test/civl/GC.bpl:898:requires {:layer 100} (forall i: int :: rootAddr(i) && memAddr(root[i]) ==> Black(Color[root[i]]));
boogie-2.4.1+dfsg/Test/civl/GC.bpl-899-requires {:layer 100} SweepInv(root, rootAbs, mem, memAbs, Color, toAbs, allocSet);
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-902-ensures {:layer 100} SweepInv(root, rootAbs, mem, memAbs, Color, toAbs, allocSet);
boogie-2.4.1+dfsg/Test/civl/GC.bpl:903:ensures {:layer 100} (forall x: int :: memAddr(x) ==> !Black(Color[x]));
boogie-2.4.1+dfsg/Test/civl/GC.bpl-904-ensures {:layer 100} sweepPtr == memHi;
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-920- invariant {:layer 100} localSweepPtr == sweepPtr && memLo <= sweepPtr && sweepPtr <= memHi;
boogie-2.4.1+dfsg/Test/civl/GC.bpl:921: invariant {:layer 100} (forall i: int :: rootAddr(i) && memAddr(root[i]) ==> Black(snapColor[root[i]]));
boogie-2.4.1+dfsg/Test/civl/GC.bpl-922- invariant {:layer 100} SweepInvInit(root, rootAbs, mem, memAbs, snapColor, toAbs, allocSet);
boogie-2.4.1+dfsg/Test/civl/GC.bpl:923: invariant {:layer 100} (forall i:int:: memAddr(i) ==> if sweepPtr <= i then Color[i] == snapColor[i] else if Black(snapColor[i]) then White(Color[i]) else Unalloc(Color[i]));
boogie-2.4.1+dfsg/Test/civl/GC.bpl-924- {
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-933-{
boogie-2.4.1+dfsg/Test/civl/GC.bpl:934: assert mutatorTidWhole(tid) && rootAddr(x) && tidOwns(tid, x) && fieldAddr(f) && rootAddr(y) && tidOwns(tid, y) && memAddr(root[x]) && toAbs[root[x]] != nil && memAddrAbs(rootAbs[x]);
boogie-2.4.1+dfsg/Test/civl/GC.bpl-935- memAbs[rootAbs[x]][f] := rootAbs[y];
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-957-{
boogie-2.4.1+dfsg/Test/civl/GC.bpl:958: assert mutatorTidWhole(tid) && rootAddr(x) && tidOwns(tid, x) && fieldAddr(f) && rootAddr(y) && tidOwns(tid, y) && memAddr(root[x]) && toAbs[root[x]] != nil && memAddrAbs(rootAbs[x]);
boogie-2.4.1+dfsg/Test/civl/GC.bpl-959- rootAbs[y] := memAbs[rootAbs[x]][f];
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-976-procedure {:atomic} {:layer 100} AtomicEqRaw({:linear "tid"} tid:Tid, x: idx, y:idx) returns (isEqual:bool)
boogie-2.4.1+dfsg/Test/civl/GC.bpl:977:{ assert mutatorTidWhole(tid) && rootAddr(x) && tidOwns(tid, x) && rootAddr(y) && tidOwns(tid, y); isEqual := root[x] == root[y]; }
boogie-2.4.1+dfsg/Test/civl/GC.bpl-978-
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-993-{
boogie-2.4.1+dfsg/Test/civl/GC.bpl:994: assert mutatorTidWhole(tid) && rootAddr(y) && tidOwns(tid, y);
boogie-2.4.1+dfsg/Test/civl/GC.bpl:995: assert (forall x: int, f: fld :: memAddr(x) && Unalloc(Color[x]) ==> toAbs[x] == nil);
boogie-2.4.1+dfsg/Test/civl/GC.bpl:996: assume(memAddr(ptr) && Unalloc(Color[ptr]));
boogie-2.4.1+dfsg/Test/civl/GC.bpl-997- assume(memAddrAbs(absPtr) && !allocSet[absPtr] && absPtr != nil);
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1001- toAbs[ptr] := absPtr;
boogie-2.4.1+dfsg/Test/civl/GC.bpl:1002: memAbs[absPtr] := (lambda z: int :: if (fieldAddr(z)) then absPtr else memAbs[absPtr][z]);
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1003- Color[ptr] := if sweepPtr <= ptr then BLACK() else WHITE();
boogie-2.4.1+dfsg/Test/civl/GC.bpl:1004: mem[ptr] := (lambda z: int :: if (fieldAddr(z)) then ptr else mem[ptr][z]);
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1005-}
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1021- assert mutatorTidWhole(tid);
boogie-2.4.1+dfsg/Test/civl/GC.bpl:1022: assert (forall x: int, f: fld :: memAddr(x) && Unalloc(Color[x]) ==> toAbs[x] == nil);
boogie-2.4.1+dfsg/Test/civl/GC.bpl:1023: assume (memAddr(ptr) && Unalloc(Color[ptr]));
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1024- Color[ptr] := if sweepPtr <= ptr then BLACK() else WHITE();
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1025- toAbs[ptr] := absPtr;
boogie-2.4.1+dfsg/Test/civl/GC.bpl:1026: mem[ptr] := (lambda z: int :: if (fieldAddr(z)) then ptr else mem[ptr][z]);
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1027-}
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1037- invariant {:layer 98} !spaceFound;
boogie-2.4.1+dfsg/Test/civl/GC.bpl:1038: invariant {:layer 98} (forall x: int, f: fld :: memAddr(x) && Unalloc(Color[x]) ==> toAbs[x] == nil);
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1039- {
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1043- invariant {:layer 98} memLo <= iter && iter <= memHi;
boogie-2.4.1+dfsg/Test/civl/GC.bpl:1044: invariant {:layer 98} memAddr(iter) && Unalloc(Color[iter]) ==> toAbs[iter] == nil;
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1045- {
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1070- var val:int;
boogie-2.4.1+dfsg/Test/civl/GC.bpl:1071: assert mutatorTidWhole(tid) && rootAddr(y) && tidOwns(tid, y);
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1072- val := root[y];
boogie-2.4.1+dfsg/Test/civl/GC.bpl:1073: if (MarkPhase(mutatorPhase[i#Tid(tid)]) && memAddr(val) && White(Color[val])) {
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1074- Color[val] := GRAY();
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1086- call rootVal := ReadRoot(tid, y);
boogie-2.4.1+dfsg/Test/civl/GC.bpl:1087: if (memAddr(rootVal))
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1088- {
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1101-{
boogie-2.4.1+dfsg/Test/civl/GC.bpl:1102: assert mutatorTidWhole(tid) && memAddr(memLocal) && MarkPhase(mutatorPhase[i#Tid(tid)]);
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1103- if (White(Color[memLocal])) {
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1139- assert tid == GcTid && rootScanOn && mutatorsInRootScanBarrier == Mutators;
boogie-2.4.1+dfsg/Test/civl/GC.bpl:1140: noGray := (forall i: int :: memAddr(i) ==> !Gray(Color[i]));
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1141-}
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1162-{
boogie-2.4.1+dfsg/Test/civl/GC.bpl:1163: assert tid == GcTid && rootScanOn && mutatorsInRootScanBarrier == Mutators && memAddr(memLocal);
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1164- if (White(Color[memLocal])) {
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1189- assert tid == GcTid;
boogie-2.4.1+dfsg/Test/civl/GC.bpl:1190: assert MarkPhase(collectorPhase) && PhaseConsistent(collectorPhase, mutatorPhase) && sweepPtr == memLo && memAddr(child);
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1191- if (White(Color[child])) {
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1196-procedure {:yields} {:layer 98} {:refines "AtomicSET_InsertIntoSetIfWhite"} SET_InsertIntoSetIfWhite({:linear "tid"} tid:Tid, parent: int, child:int)
boogie-2.4.1+dfsg/Test/civl/GC.bpl:1197:requires {:layer 98} tid == GcTid && memAddr(parent) && memAddr(child) && MsWellFormed(MarkStack, MarkStackPtr, Color, parent);
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1198-ensures {:layer 98} MsWellFormed(MarkStack, MarkStackPtr, Color, parent);
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1201- yield;
boogie-2.4.1+dfsg/Test/civl/GC.bpl:1202: assert {:layer 98} tid == GcTid && memAddr(parent) && memAddr(child);
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1203- assert {:layer 98} MsWellFormed(MarkStack, MarkStackPtr, Color, parent);
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1207- yield;
boogie-2.4.1+dfsg/Test/civl/GC.bpl:1208: assert {:layer 98} tid == GcTid && memAddr(parent) && memAddr(child);
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1209- assert {:layer 98} MsWellFormed(MarkStack, MarkStackPtr, Color, parent);
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1217- if (*) {
boogie-2.4.1+dfsg/Test/civl/GC.bpl:1218: assume (memAddr(val) && !Unalloc(Color[val]));
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1219- isEmpty := false;
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1250- assert tid == GcTid;
boogie-2.4.1+dfsg/Test/civl/GC.bpl:1251: assert memAddr(scannedLocal);
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1252- Color[scannedLocal] := BLACK();
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1266-{
boogie-2.4.1+dfsg/Test/civl/GC.bpl:1267: assert memAddr(val) && tid == GcTid;
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1268- if (White(Color[val])) {
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1296-{
boogie-2.4.1+dfsg/Test/civl/GC.bpl:1297: assert memAddr(val) && mutatorTidWhole(tid) && MarkPhase(mutatorPhase[i#Tid(tid)]);
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1298- if (White(Color[val])) {
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1392- assert tid == GcTid;
boogie-2.4.1+dfsg/Test/civl/GC.bpl:1393: assert memAddr(sweepPtr);
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1394- Color[sweepPtr] := if White(Color[sweepPtr]) then UNALLOC() else if Black(Color[sweepPtr]) then WHITE() else Color[sweepPtr];
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1567-{
boogie-2.4.1+dfsg/Test/civl/GC.bpl:1568: assert mutatorTidWhole(tid) && memAddr(ptr) && (Unalloc(Color[ptr]) ==> toAbs[ptr] == nil);
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1569- if (*) {
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1572- toAbs[ptr] := absPtr;
boogie-2.4.1+dfsg/Test/civl/GC.bpl:1573: mem[ptr] := (lambda z: int :: if (fieldAddr(z)) then ptr else mem[ptr][z]);
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1574- spaceFound := true;
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1629-procedure {:atomic} {:layer 97,100} AtomicIsWhiteByCollector({:linear "tid"} tid:Tid, i: int) returns (isWhite: bool)
boogie-2.4.1+dfsg/Test/civl/GC.bpl:1630:{ assert tid == GcTid && memAddr(i); isWhite := White(Color[i]); }
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1631-
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1644-modifies toAbs;
boogie-2.4.1+dfsg/Test/civl/GC.bpl:1645:{ assert tid == GcTid; toAbs := (lambda x: int :: if memAddr(x) && White(Color[x]) then nil else toAbs[x]); }
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1646-
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1661-modifies toAbs;
boogie-2.4.1+dfsg/Test/civl/GC.bpl:1662:{ assert tid == GcTid && tidHasLock(tid, lock); toAbs := (lambda x: int :: if memAddr(x) && White(Color[x]) then nil else toAbs[x]); }
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1663-
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1672-modifies mem;
boogie-2.4.1+dfsg/Test/civl/GC.bpl:1673:{ assert gcAndMutatorTids(tid, mutatorTids) && memAddr(x) && fieldAddr(f); mem[x][f] := x; }
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1674-
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1682-procedure {:atomic} {:layer 96,100} AtomicReadFieldCollector({:linear "tid"} tid:Tid, x:int, f: fld) returns (y: int)
boogie-2.4.1+dfsg/Test/civl/GC.bpl:1683:{ assert tid == GcTid && memAddr(x) && fieldAddr(f) && toAbs[x] != nil; y := mem[x][f]; }
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1684-
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1692-procedure {:atomic} {:layer 96,99} AtomicReadFieldGeneral({:linear "tid"} tid:Tid, x: int, f: fld) returns (y: int)
boogie-2.4.1+dfsg/Test/civl/GC.bpl:1693:{ assert mutatorTidWhole(tid) && memAddr(x) && fieldAddr(f) && toAbs[x] != nil; y := mem[x][f]; }
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1694-
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1703-modifies mem;
boogie-2.4.1+dfsg/Test/civl/GC.bpl:1704:{ assert mutatorTidWhole(tid) && memAddr(x) && fieldAddr(f) && toAbs[x] != nil; mem[x][f] := y; }
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1705-
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1714-modifies mem;
boogie-2.4.1+dfsg/Test/civl/GC.bpl:1715:{ assert mutatorTidWhole(tid) && tidHasLock(tid, lock) && memAddr(ptr) && fieldAddr(fld) && toAbs[ptr] == nil; mem[ptr][fld] := ptr; }
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1716-
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1996-modifies root;
boogie-2.4.1+dfsg/Test/civl/GC.bpl:1997:{ assert gcAndMutatorTids(tid, mutatorTids) && rootAddr(x); root[x] := 0; }
boogie-2.4.1+dfsg/Test/civl/GC.bpl-1998-
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-2006-procedure {:left} {:layer 96,99} AtomicReadRootInRootScanBarrier({:linear "tid"} tid:Tid, x: idx) returns (val: int)
boogie-2.4.1+dfsg/Test/civl/GC.bpl:2007:{ assert tid == GcTid && rootAddr(x) && rootScanOn && mutatorsInRootScanBarrier == Mutators; val := root[x]; }
boogie-2.4.1+dfsg/Test/civl/GC.bpl-2008-
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-2017-modifies root;
boogie-2.4.1+dfsg/Test/civl/GC.bpl:2018:{ assert mutatorTidWhole(tid) && rootAddr(i) && tidOwns(tid, i); root[i] := val; }
boogie-2.4.1+dfsg/Test/civl/GC.bpl-2019-
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-2027-procedure {:both} {:layer 96,99} AtomicReadRoot({:linear "tid"} tid: Tid, i: idx) returns (val: int)
boogie-2.4.1+dfsg/Test/civl/GC.bpl:2028:{ assert mutatorTidWhole(tid) && rootAddr(i) && tidOwns(tid, i); val := root[i]; }
boogie-2.4.1+dfsg/Test/civl/GC.bpl-2029-
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-2038-modifies Color;
boogie-2.4.1+dfsg/Test/civl/GC.bpl:2039:{ assert gcAndMutatorTids(tid, mutatorTids) && memAddr(x); Color[x] := UNALLOC(); }
boogie-2.4.1+dfsg/Test/civl/GC.bpl-2040-
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-2048-procedure {:both} {:layer 96} AtomicReadColorByCollector({:linear "tid"} tid:Tid, i: int) returns (val: int)
boogie-2.4.1+dfsg/Test/civl/GC.bpl:2049:{ assert tid == GcTid && tidHasLock(tid, lock) && memAddr(i); val := Color[i]; }
boogie-2.4.1+dfsg/Test/civl/GC.bpl-2050-
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-2058-procedure {:atomic} {:layer 96} AtomicReadColorByMutator1({:linear "tid"} tid:Tid, i: int) returns (val: int)
boogie-2.4.1+dfsg/Test/civl/GC.bpl:2059:{ assert mutatorTidWhole(tid) && memAddr(i); }
boogie-2.4.1+dfsg/Test/civl/GC.bpl-2060-
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-2068-procedure {:both} {:layer 96} AtomicReadColorByMutator2({:linear "tid"} tid:Tid, i: int) returns (val: int)
boogie-2.4.1+dfsg/Test/civl/GC.bpl:2069:{ assert mutatorTidWhole(tid) && tidHasLock(tid, lock) && memAddr(i); val := Color[i]; }
boogie-2.4.1+dfsg/Test/civl/GC.bpl-2070-
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-2079-{
boogie-2.4.1+dfsg/Test/civl/GC.bpl:2080: assert mutatorTidWhole(tid) && memAddr(i) && MarkPhase(mutatorPhase[i#Tid(tid)]);
boogie-2.4.1+dfsg/Test/civl/GC.bpl-2081- assume White(Color[i]) ==> White(val);
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-2092-modifies Color;
boogie-2.4.1+dfsg/Test/civl/GC.bpl:2093:{ assert tidHasLock(tid, lock) && memAddr(i) && PhaseConsistent(collectorPhase, mutatorPhase) && !MarkPhase(collectorPhase); Color[i] := val; }
boogie-2.4.1+dfsg/Test/civl/GC.bpl-2094-
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-2104-{
boogie-2.4.1+dfsg/Test/civl/GC.bpl:2105: assert tidHasLock(tid, lock) && memAddr(i);
boogie-2.4.1+dfsg/Test/civl/GC.bpl-2106- assert (MarkPhase(collectorPhase) || !PhaseConsistent(collectorPhase, mutatorPhase) ==> !White(val));
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-2119-{
boogie-2.4.1+dfsg/Test/civl/GC.bpl:2120: assert tidHasLock(tid, lock) && memAddr(i);
boogie-2.4.1+dfsg/Test/civl/GC.bpl-2121- assert White(val) ==> Unalloc(Color[i]);
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-2137- assert gcAndMutatorTids(tid, mutatorTids);
boogie-2.4.1+dfsg/Test/civl/GC.bpl:2138: toAbs := (lambda i:int :: if memAddr(i) then nil else Int(i));
boogie-2.4.1+dfsg/Test/civl/GC.bpl-2139-}
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-2213-procedure {:atomic} {:layer 1,95} AtomicPrimitiveReadField(x: int, f: fld) returns (y: int)
boogie-2.4.1+dfsg/Test/civl/GC.bpl:2214:{ assert memAddr(x) && fieldAddr(f); y := mem[x][f]; }
boogie-2.4.1+dfsg/Test/civl/GC.bpl-2215-procedure {:yields} {:layer 0} {:refines "AtomicPrimitiveReadField"} PrimitiveReadField(x: int, f: fld) returns (y: int);
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-2218-modifies mem;
boogie-2.4.1+dfsg/Test/civl/GC.bpl:2219:{ assert memAddr(x) && fieldAddr(f); mem[x][f] := y; }
boogie-2.4.1+dfsg/Test/civl/GC.bpl-2220-procedure {:yields} {:layer 0} {:refines "AtomicPrimitiveWriteField"} PrimitiveWriteField(x: int, f: fld, y: int);
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-2306-modifies root;
boogie-2.4.1+dfsg/Test/civl/GC.bpl:2307:{ assert rootAddr(i); root[i] := val; }
boogie-2.4.1+dfsg/Test/civl/GC.bpl-2308-procedure {:yields} {:layer 0} {:refines "AtomicPrimitiveWriteRoot"} PrimitiveWriteRoot(i: idx, val: int);
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-2310-procedure {:atomic} {:layer 1,95} AtomicPrimitiveReadRoot(i: idx) returns (val: int)
boogie-2.4.1+dfsg/Test/civl/GC.bpl:2311:{ assert rootAddr(i); val := root[i]; }
boogie-2.4.1+dfsg/Test/civl/GC.bpl-2312-procedure {:yields} {:layer 0} {:refines "AtomicPrimitiveReadRoot"} PrimitiveReadRoot(i: idx) returns (val: int);
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-2314-procedure {:atomic} {:layer 1,95} AtomicPrimitiveReadColor(i: int) returns (val: int)
boogie-2.4.1+dfsg/Test/civl/GC.bpl:2315:{ assert memAddr(i); val := Color[i]; }
boogie-2.4.1+dfsg/Test/civl/GC.bpl-2316-procedure {:yields} {:layer 0} {:refines "AtomicPrimitiveReadColor"} PrimitiveReadColor(i: int) returns (val: int);
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-2319-modifies Color;
boogie-2.4.1+dfsg/Test/civl/GC.bpl:2320:{ assert memAddr(i); Color[i] := val; }
boogie-2.4.1+dfsg/Test/civl/GC.bpl-2321-procedure {:yields} {:layer 0} {:refines "AtomicPrimitiveSetColor"} PrimitiveSetColor(i: int, val: int);
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-2354-{
boogie-2.4.1+dfsg/Test/civl/GC.bpl:2355: memAbs[absPtr] := (lambda z: int :: if (fieldAddr(z)) then absPtr else memAbs[absPtr][z]);
boogie-2.4.1+dfsg/Test/civl/GC.bpl-2356-}
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-2366-{
boogie-2.4.1+dfsg/Test/civl/GC.bpl:2367: toAbs := (lambda x: int :: if memAddr(x) && White(Color[x]) then nil else toAbs[x]);
boogie-2.4.1+dfsg/Test/civl/GC.bpl-2368-}
##############################################
boogie-2.4.1+dfsg/Test/civl/GC.bpl-2378-{
boogie-2.4.1+dfsg/Test/civl/GC.bpl:2379: toAbs := (lambda i:int :: if memAddr(i) then nil else Int(i));
boogie-2.4.1+dfsg/Test/civl/GC.bpl-2380-}
##############################################
boogie-2.4.1+dfsg/Test/civl/alloc-mem.bpl-84- call Yield();
boogie-2.4.1+dfsg/Test/civl/alloc-mem.bpl:85: call i := PickAddr();
boogie-2.4.1+dfsg/Test/civl/alloc-mem.bpl-86- call l := AllocLinear(i);
##############################################
boogie-2.4.1+dfsg/Test/civl/alloc-mem.bpl-103- call FreeLinear(l, i);
boogie-2.4.1+dfsg/Test/civl/alloc-mem.bpl:104: call ReturnAddr(i);
boogie-2.4.1+dfsg/Test/civl/alloc-mem.bpl-105- call Yield();
##############################################
boogie-2.4.1+dfsg/Test/civl/alloc-mem.bpl-190-
boogie-2.4.1+dfsg/Test/civl/alloc-mem.bpl:191:procedure {:atomic} {:layer 1} atomic_PickAddr () returns (i:int)
boogie-2.4.1+dfsg/Test/civl/alloc-mem.bpl-192-modifies unallocated;
##############################################
boogie-2.4.1+dfsg/Test/civl/alloc-mem.bpl-197-
boogie-2.4.1+dfsg/Test/civl/alloc-mem.bpl:198:procedure {:atomic} {:layer 1} atomic_ReturnAddr (i:int)
boogie-2.4.1+dfsg/Test/civl/alloc-mem.bpl-199-modifies unallocated;
##############################################
boogie-2.4.1+dfsg/Test/civl/alloc-mem.bpl-203-procedure {:yields} {:layer 0} {:refines "atomic_WriteLow"} WriteLow (i:int, o:int);
boogie-2.4.1+dfsg/Test/civl/alloc-mem.bpl:204:procedure {:yields} {:layer 0} {:refines "atomic_PickAddr"} PickAddr () returns (i:int);
boogie-2.4.1+dfsg/Test/civl/alloc-mem.bpl:205:procedure {:yields} {:layer 0} {:refines "atomic_ReturnAddr"} ReturnAddr (i:int);
##############################################
boogie-2.4.1+dfsg/Test/civl/linear_out_bug.bpl-9-
boogie-2.4.1+dfsg/Test/civl/linear_out_bug.bpl:10:procedure {:atomic} {:layer 1,2} AddAddr({:linear_in "addr"} i: int)
boogie-2.4.1+dfsg/Test/civl/linear_out_bug.bpl-11-modifies Addrs;
##############################################
boogie-2.4.1+dfsg/Test/civl/reserve.bpl-3-axiom 0 < memLo && memLo <= memHi;
boogie-2.4.1+dfsg/Test/civl/reserve.bpl:4:function memAddr(i:int) returns (bool) { memLo <= i && i < memHi }
boogie-2.4.1+dfsg/Test/civl/reserve.bpl-5-
##############################################
boogie-2.4.1+dfsg/Test/civl/reserve.bpl-7-axiom 0 < numMutators;
boogie-2.4.1+dfsg/Test/civl/reserve.bpl:8:function {:inline} mutatorAddr(i: int) returns (bool) { 1 <= i && i <= numMutators }
boogie-2.4.1+dfsg/Test/civl/reserve.bpl-9-
##############################################
boogie-2.4.1+dfsg/Test/civl/reserve.bpl-49- 0 <= freeSpace &&
boogie-2.4.1+dfsg/Test/civl/reserve.bpl:50: (forall u: int, v: int :: memAddr(u) && memAddr(v) && u <= v ==> Subset(AllocatingAtOrAfter[v], AllocatingAtOrAfter[u])) &&
boogie-2.4.1+dfsg/Test/civl/reserve.bpl:51: (forall u: int :: memAddr(u) || NumFreeAtOrAfter[u] == 0) &&
boogie-2.4.1+dfsg/Test/civl/reserve.bpl:52: (forall u: int :: {memAddr(u)} memAddr(u) ==> NumFreeAtOrAfter[u] == (NumFreeAtOrAfter[u+1] + (if Free[u] then 1 else 0)))
boogie-2.4.1+dfsg/Test/civl/reserve.bpl-53-}
##############################################
boogie-2.4.1+dfsg/Test/civl/reserve.bpl-63-ensures {:atomic} |{
boogie-2.4.1+dfsg/Test/civl/reserve.bpl:64: A: assert memAddr(ptr);
boogie-2.4.1+dfsg/Test/civl/reserve.bpl:65: assert Free[ptr] || memAddr(ptr + 1);
boogie-2.4.1+dfsg/Test/civl/reserve.bpl-66- assert (forall u: int :: AllocatingAtOrAfter[u][tid] <==> memLo <= u && u <= ptr);
##############################################
boogie-2.4.1+dfsg/Test/civl/reserve.bpl-79-ensures {:atomic} |{ var ptr: int;
boogie-2.4.1+dfsg/Test/civl/reserve.bpl:80: A: assume memAddr(ptr) && !Free[ptr];
boogie-2.4.1+dfsg/Test/civl/reserve.bpl-81- freeSpace := freeSpace + 1;
##############################################
boogie-2.4.1+dfsg/Test/civl/reserve.bpl-86-procedure {:yields} {:layer 1} YieldAlloc({:cnst "tid"} tid:int, i: int)
boogie-2.4.1+dfsg/Test/civl/reserve.bpl:87:requires {:layer 1} mutatorAddr(tid);
boogie-2.4.1+dfsg/Test/civl/reserve.bpl-88-requires {:expand} {:layer 1} Invariant(NumFreeAtOrAfter, AllocatingAtOrAfter, Free, freeSpace);
##############################################
boogie-2.4.1+dfsg/Test/civl/reserve.bpl-93- yield;
boogie-2.4.1+dfsg/Test/civl/reserve.bpl:94: assert {:layer 1} mutatorAddr(tid);
boogie-2.4.1+dfsg/Test/civl/reserve.bpl-95- assert {:layer 1} Invariant(NumFreeAtOrAfter, AllocatingAtOrAfter, Free, freeSpace);
##############################################
boogie-2.4.1+dfsg/Test/civl/reserve.bpl-99-procedure {:yields} {:layer 1} Malloc({:cnst "tid"} tid: X)
boogie-2.4.1+dfsg/Test/civl/reserve.bpl:100:requires {:layer 1} mutatorAddr(tid);
boogie-2.4.1+dfsg/Test/civl/reserve.bpl-101-requires {:layer 1} Invariant(NumFreeAtOrAfter, AllocatingAtOrAfter, Free, freeSpace);
##############################################
boogie-2.4.1+dfsg/Test/civl/reserve.bpl-110-
boogie-2.4.1+dfsg/Test/civl/reserve.bpl:111: assert {:layer 1} memAddr(memLo) ==> (forall v: int :: memAddr(v) && memLo <= v ==> Subset(AllocatingAtOrAfter[v], AllocatingAtOrAfter[memLo]));
boogie-2.4.1+dfsg/Test/civl/reserve.bpl:112: assert {:layer 1} memAddr(memLo) ==> (forall v: int :: memAddr(v) && v <= memLo ==> Subset(AllocatingAtOrAfter[memLo], AllocatingAtOrAfter[v]));
boogie-2.4.1+dfsg/Test/civl/reserve.bpl-113-
##############################################
boogie-2.4.1+dfsg/Test/civl/reserve.bpl-119- while (i < memHi)
boogie-2.4.1+dfsg/Test/civl/reserve.bpl:120: invariant {:layer 1} memAddr(i);
boogie-2.4.1+dfsg/Test/civl/reserve.bpl-121- invariant {:layer 1} Invariant(NumFreeAtOrAfter, AllocatingAtOrAfter, Free, freeSpace);
##############################################
boogie-2.4.1+dfsg/Test/civl/reserve.bpl-123- {
boogie-2.4.1+dfsg/Test/civl/reserve.bpl:124: assert {:layer 1} memAddr(i+1) ==> (forall v: int :: memAddr(v) && i+1 <= v ==> Subset(AllocatingAtOrAfter[v], AllocatingAtOrAfter[i+1]));
boogie-2.4.1+dfsg/Test/civl/reserve.bpl:125: assert {:layer 1} memAddr(i+1) ==> (forall v: int :: memAddr(v) && v <= i+1 ==> Subset(AllocatingAtOrAfter[i+1], AllocatingAtOrAfter[v]));
boogie-2.4.1+dfsg/Test/civl/reserve.bpl-126-
##############################################
boogie-2.4.1+dfsg/Test/test21/MapAxiomsConsistency.bpl-60-
boogie-2.4.1+dfsg/Test/test21/MapAxiomsConsistency.bpl:61:procedure Node.ReverseInPlace(this: ref where this != null && $Heap[this, alloc]) returns (reverse: ref where reverse == null || $Heap[reverse, alloc]);
boogie-2.4.1+dfsg/Test/test21/MapAxiomsConsistency.bpl-62- // user-defined preconditions
##############################################
boogie-2.4.1+dfsg/Test/test21/MapAxiomsConsistency.bpl-73-
boogie-2.4.1+dfsg/Test/test21/MapAxiomsConsistency.bpl:74:procedure CheckWellformed$$Node.Valid(this: ref where this != null && $Heap[this, alloc]);
boogie-2.4.1+dfsg/Test/test21/MapAxiomsConsistency.bpl-75-
##############################################
boogie-2.4.1+dfsg/Test/test21/MapAxiomsConsistency.bpl-81-{
boogie-2.4.1+dfsg/Test/test21/MapAxiomsConsistency.bpl:82: var current: ref where current == null || $Heap[current, alloc], $PreLoopHeap0: HeapType, nx: ref where nx == null || $Heap[nx, alloc];
boogie-2.4.1+dfsg/Test/test21/MapAxiomsConsistency.bpl-83-