type ref; type realVar; type classConst; // type Field x; // var $HeapVar : [ref, Field x]x; const unique $null : ref ; const unique $intArrNull : [int]int ; const unique $realArrNull : [int]realVar ; const unique $refArrNull : [int]ref ; const unique $arrSizeIdx : int; var $intArrSize : [int]int; var $realArrSize : [realVar]int; var $refArrSize : [ref]int; var $stringSize : [ref]int; //built-in axioms axiom ($arrSizeIdx == -1); //note: new version doesn't put helpers in the perlude anymore//Prelude finished const unique javaUtilEx.Content : classConst ; const unique javaUtilEx.RandomAccess : classConst ; const unique javaUtilEx.List : classConst ; var $fresh1 : ref; var javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$previous302 : Field ref; var int$javaUtilEx.SubList$offset0 : Field int; var int$javaUtilEx.LinkedList$ListItr$nextIndex0 : Field int; var javaUtilEx.LinkedList$ListItr$javaUtilEx.LinkedList$DescendingIterator$itr306 : Field ref; var javaUtilEx.LinkedList$javaUtilEx.LinkedList$DescendingIterator$this$0307 : Field ref; var javaUtilEx.AbstractList$javaUtilEx.SubList$l297 : Field ref; var java.lang.String$lp$$rp$$javaUtilEx.Random$args299 : [int]ref; var javaUtilEx.SubList$javaUtilEx.SubList$1$this$0309 : Field ref; var int$javaUtilEx.AbstractList$Itr$expectedModCount0 : Field int; var javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$ListItr$next304 : Field ref; var $fresh6 : ref; var $fresh3 : ref; var int$javaUtilEx.LinkedList$size0 : Field int; var javaUtilEx.AbstractList$javaUtilEx.AbstractList$ListItr$this$0296 : Field ref; var $fresh4 : ref; var int$javaUtilEx.AbstractList$Itr$cursor0 : Field int; var javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$next301 : Field ref; var $fresh2 : ref; var javaUtilEx.ListIterator$javaUtilEx.SubList$1$i308 : Field ref; var int$javaUtilEx.LinkedList$ListItr$expectedModCount0 : Field int; var javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$ListItr$lastReturned303 : Field ref; var int$javaUtilEx.Random$index0 : int; var int$javaUtilEx.AbstractList$Itr$lastRet0 : Field int; var int$javaUtilEx.Content$val0 : Field int; var $fresh5 : ref; var java.lang.Object$javaUtilEx.LinkedList$Entry$element300 : Field ref; var javaUtilEx.AbstractList$javaUtilEx.AbstractList$Itr$this$0295 : Field ref; var javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$header298 : Field ref; var javaUtilEx.LinkedList$javaUtilEx.LinkedList$ListItr$this$0305 : Field ref; var int$javaUtilEx.SubList$1$val$index0 : Field int; var int$javaUtilEx.AbstractList$modCount0 : Field int; var int$javaUtilEx.SubList$size0 : Field int; // procedure java.lang.Object$javaUtilEx.Iterator$next$2255(__this : ref) returns (__ret : ref); // @line: 325 // procedure javaUtilEx.ListIterator$javaUtilEx.AbstractList$listIterator$2495(__this : ref, $param_0 : int) returns (__ret : ref, $Exep0 : ref) requires ($neref((__this), ($null))==1); { var i0161 : int; var $r1162 : ref; var r0160 : ref; //temp local variables var $caughtEx1 : ref; // @line: 325 Block158: $caughtEx1 := $null; $Exep0 := $null; goto Block237; Block237: r0160 := __this; i0161 := $param_0; assert ($neref((r0160), ($null))==1); // @line: 326 call $caughtEx1 := void$javaUtilEx.AbstractList$rangeCheckForAdd$2500((r0160), (i0161)); goto Block238, Block240; Block238: assume ($neref(($caughtEx1), ($null))==1); goto Block239; Block240: assume ($eqref(($caughtEx1), ($null))==1); goto Block241; Block239: $Exep0 := $caughtEx1; return; Block241: // @line: 328 $r1162 := $newvariable((242)); assume ($neref(($newvariable((242))), ($null))==1); assert ($neref(($r1162), ($null))==1); // @line: 328 call void$javaUtilEx.AbstractList$ListItr$$la$init$ra$$2542(($r1162), (r0160), (i0161)); // @line: 328 __ret := $r1162; return; } // procedure is generated by joogie. function {:inline true} $realarrtoref($param00 : [int]realVar) returns (__ret : ref); // @line: 676 // procedure boolean$javaUtilEx.SubList$addAll$2556(__this : ref, $param_0 : ref) returns (__ret : int, $Exep1 : ref, $Exep0 : ref, $Exep2 : ref) requires ($neref((__this), ($null))==1); { var $i0376 : int; var r1375 : ref; var $z0377 : int; var r0374 : ref; //temp local variables var $caughtEx5 : ref; var $caughtEx4 : ref; var $caughtEx3 : ref; // @line: 676 Block578: $caughtEx5 := $null; $caughtEx4 := $null; $caughtEx3 := $null; $Exep2 := $null; $Exep1 := $null; $Exep0 := $null; goto Block579; Block579: r0374 := __this; r1375 := $param_0; assert ($neref((r0374), ($null))==1); // @line: 677 $i0376 := $HeapVar[r0374, int$javaUtilEx.SubList$size0]; assert ($neref((r0374), ($null))==1); // @line: 677 call $z0377, $caughtEx3, $caughtEx4, $caughtEx5 := boolean$javaUtilEx.SubList$addAll$2557((r0374), ($i0376), (r1375)); goto Block580, Block582; Block580: assume ($neref(($caughtEx3), ($null))==1); goto Block581; Block582: assume ($eqref(($caughtEx3), ($null))==1); goto Block583; Block581: $Exep1 := $caughtEx3; return; Block583: goto Block586, Block584; Block586: assume ($eqref(($caughtEx4), ($null))==1); goto Block587; Block584: assume ($neref(($caughtEx4), ($null))==1); goto Block585; Block587: goto Block588, Block590; Block585: $Exep0 := $caughtEx4; return; Block588: assume ($neref(($caughtEx5), ($null))==1); goto Block589; Block590: assume ($eqref(($caughtEx5), ($null))==1); goto Block591; Block589: $Exep2 := $caughtEx5; return; Block591: // @line: 677 __ret := $z0377; return; } // procedure is generated by joogie. function {:inline true} $leref($param00 : ref, $param11 : ref) returns (__ret : int); // @line: 32 // procedure int$javaUtilEx.Content$hashCode$2587(__this : ref) returns (__ret : int) requires ($neref((__this), ($null))==1); { var $i1499 : int; var r0497 : ref; var $i0498 : int; Block738: r0497 := __this; assert ($neref((r0497), ($null))==1); // @line: 33 $i0498 := $HeapVar[r0497, int$javaUtilEx.Content$val0]; // @line: 33 $i1499 := $xorint(($i0498), (31)); // @line: 33 __ret := $i1499; return; } // @line: 4 // ()> procedure void$javaUtilEx.Random$$la$clinit$ra$$2675() modifies int$javaUtilEx.Random$index0; { // @line: 5 Block1152: // @line: 5 int$javaUtilEx.Random$index0 := 0; return; } // procedure void$javaUtilEx.ListIterator$remove$2531(__this : ref); // procedure is generated by joogie. function {:inline true} $inttoreal($param00 : int) returns (__ret : realVar); // @line: 561 // procedure java.lang.Object$javaUtilEx.LinkedList$pop$2661(__this : ref) returns (__ret : ref, $Exep0 : ref) requires ($neref((__this), ($null))==1); { var r0700 : ref; var $r1701 : ref; //temp local variables var $caughtEx1 : ref; // @line: 561 Block1061: $caughtEx1 := $null; $Exep0 := $null; goto Block1062; Block1062: r0700 := __this; assert ($neref((r0700), ($null))==1); // @line: 562 call $r1701, $caughtEx1 := java.lang.Object$javaUtilEx.LinkedList$removeFirst$2633((r0700)); goto Block1065, Block1063; Block1065: assume ($eqref(($caughtEx1), ($null))==1); goto Block1066; Block1063: assume ($neref(($caughtEx1), ($null))==1); goto Block1064; Block1066: // @line: 562 __ret := $r1701; return; Block1064: $Exep0 := $caughtEx1; return; } // procedure java.lang.String$java.lang.StringBuilder$toString$2299(__this : ref) returns (__ret : ref); // @line: 107 // procedure boolean$javaUtilEx.AbstractList$add$2484(__this : ref, $param_0 : ref) returns (__ret : int, $Exep0 : ref) requires ($neref((__this), ($null))==1); { var r0105 : ref; var $i0106 : int; var r1107 : ref; //temp local variables var $caughtEx1 : ref; // @line: 107 Block140: $caughtEx1 := $null; $Exep0 := $null; goto Block141; Block141: r0105 := __this; r1107 := $param_0; assert ($neref((r0105), ($null))==1); // @line: 108 call $i0106 := int$javaUtilEx.AbstractCollection$size$2230((r0105)); assert ($neref((r0105), ($null))==1); // @line: 108 call $caughtEx1 := void$javaUtilEx.AbstractList$add$2487((r0105), ($i0106), (r1107)); goto Block144, Block142; Block144: assume ($eqref(($caughtEx1), ($null))==1); goto Block145; Block142: assume ($neref(($caughtEx1), ($null))==1); goto Block143; Block145: // @line: 109 __ret := 1; return; Block143: $Exep0 := $caughtEx1; return; } // procedure int$javaUtilEx.ListIterator$nextIndex$2529(__this : ref) returns (__ret : int); // @line: 693 // procedure javaUtilEx.Iterator$javaUtilEx.SubList$iterator$2558(__this : ref) returns (__ret : ref, $Exep0 : ref) requires ($neref((__this), ($null))==1); { var $r1392 : ref; var r0391 : ref; //temp local variables var $caughtEx1 : ref; // @line: 693 Block614: $caughtEx1 := $null; $Exep0 := $null; goto Block615; Block615: r0391 := __this; assert ($neref((r0391), ($null))==1); // @line: 694 call $r1392, $caughtEx1 := javaUtilEx.ListIterator$javaUtilEx.AbstractList$listIterator$2494((r0391)); goto Block618, Block616; Block618: assume ($eqref(($caughtEx1), ($null))==1); goto Block619; Block616: assume ($neref(($caughtEx1), ($null))==1); goto Block617; Block619: // @line: 694 __ret := $r1392; return; Block617: $Exep0 := $caughtEx1; return; } // @line: 351 // procedure boolean$javaUtilEx.AbstractList$Itr$hasNext$2535(__this : ref) returns (__ret : int) requires ($neref((__this), ($null))==1); { var $i1225 : int; var r0222 : ref; var $z0227 : int; var $i0224 : int; var $r1223 : ref; Block348: r0222 := __this; assert ($neref((r0222), ($null))==1); // @line: 352 $i0224 := $HeapVar[r0222, int$javaUtilEx.AbstractList$Itr$cursor0]; assert ($neref((r0222), ($null))==1); // @line: 352 $r1223 := $HeapVar[r0222, javaUtilEx.AbstractList$javaUtilEx.AbstractList$Itr$this$0295]; assert ($neref(($r1223), ($null))==1); // @line: 352 call $i1225 := int$javaUtilEx.AbstractCollection$size$2230(($r1223)); goto Block349; // @line: 352 Block349: goto Block352, Block350; // @line: 352 Block352: // @line: 352 assume ($negInt(($eqint(($i0224), ($i1225))))==1); // @line: 352 $z0227 := 1; goto Block353; // @line: 352 Block350: assume ($eqint(($i0224), ($i1225))==1); goto Block351; // @line: 352 Block353: // @line: 352 __ret := $z0227; return; // @line: 352 Block351: // @line: 352 $z0227 := 0; goto Block353; } // procedure is generated by joogie. function {:inline true} $mulref($param00 : ref, $param11 : ref) returns (__ret : ref); // @line: 276 // procedure java.lang.Object$javaUtilEx.LinkedList$get$2642(__this : ref, $param_0 : int) returns (__ret : ref, $Exep0 : ref) requires ($neref((__this), ($null))==1); { var $r2612 : ref; var r0609 : ref; var $r1611 : ref; var i0610 : int; //temp local variables var $caughtEx1 : ref; // @line: 276 Block755: $caughtEx1 := $null; $Exep0 := $null; goto Block870; Block870: r0609 := __this; i0610 := $param_0; assert ($neref((r0609), ($null))==1); // @line: 277 call $r1611, $caughtEx1 := javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$entry$2646((r0609), (i0610)); goto Block873, Block871; Block873: assume ($eqref(($caughtEx1), ($null))==1); goto Block874; Block871: assume ($neref(($caughtEx1), ($null))==1); goto Block872; Block874: assert ($neref(($r1611), ($null))==1); // @line: 277 $r2612 := $HeapVar[$r1611, java.lang.Object$javaUtilEx.LinkedList$Entry$element300]; // @line: 277 __ret := $r2612; return; Block872: $Exep0 := $caughtEx1; return; } // @line: 766 // procedure java.lang.String$javaUtilEx.SubList$outOfBoundsMsg$2563(__this : ref, $param_0 : int) returns (__ret : ref) modifies $stringSize; requires ($neref((__this), ($null))==1); { var r0410 : ref; var i0411 : int; Block669: r0410 := __this; i0411 := $param_0; $stringSize[$fresh2] := 0; // @line: 767 __ret := $fresh2; return; } // @line: 73 // ()> procedure void$javaUtilEx.AbstractSequentialList$$la$init$ra$$2578(__this : ref) requires ($neref((__this), ($null))==1); { var r0443 : ref; Block690: r0443 := __this; assert ($neref((r0443), ($null))==1); // @line: 74 call void$javaUtilEx.AbstractList$$la$init$ra$$2483((r0443)); return; } // procedure is generated by joogie. function {:inline true} $reftorefarr($param00 : ref) returns (__ret : [int]ref); // procedure is generated by joogie. function {:inline true} $reftoint($param00 : ref) returns (__ret : int); // @line: 177 // procedure int$javaUtilEx.AbstractList$indexOf$2489(__this : ref, $param_0 : ref) returns (__ret : int, $Exep0 : ref) requires ($neref((__this), ($null))==1); { var r0119 : ref; var $i0126 : int; var $z0123 : int; var $z2127 : int; var $i1129 : int; var $r3124 : ref; var $z1125 : int; var r1122 : ref; var $r4128 : ref; var r2121 : ref; //temp local variables var $caughtEx1 : ref; // @line: 177 Block160: $caughtEx1 := $null; $Exep0 := $null; goto Block161; Block161: r0119 := __this; r1122 := $param_0; assert ($neref((r0119), ($null))==1); // @line: 178 call r2121, $caughtEx1 := javaUtilEx.ListIterator$javaUtilEx.AbstractList$listIterator$2494((r0119)); goto Block164, Block162; Block164: assume ($eqref(($caughtEx1), ($null))==1); goto Block165; Block162: assume ($neref(($caughtEx1), ($null))==1); goto Block163; Block165: goto Block166; Block163: $Exep0 := $caughtEx1; return; // @line: 179 Block166: goto Block169, Block167; // @line: 179 Block169: // @line: 179 assume ($negInt(($neref((r1122), ($null))))==1); goto Block170; // @line: 179 Block167: assume ($neref((r1122), ($null))==1); goto Block168; // @line: 180 Block170: assert ($neref((r2121), ($null))==1); // @line: 180 call $z2127 := boolean$javaUtilEx.ListIterator$hasNext$2525((r2121)); goto Block171; // @line: 184 Block168: assert ($neref((r2121), ($null))==1); // @line: 184 call $z0123 := boolean$javaUtilEx.ListIterator$hasNext$2525((r2121)); goto Block178; // @line: 180 Block171: goto Block174, Block172; // @line: 184 Block178: goto Block180, Block179; // @line: 180 Block174: // @line: 180 assume ($negInt(($eqint(($z2127), (0))))==1); assert ($neref((r2121), ($null))==1); // @line: 181 call $r4128 := java.lang.Object$javaUtilEx.ListIterator$next$2526((r2121)); goto Block175; // @line: 180 Block172: assume ($eqint(($z2127), (0))==1); goto Block173; // @line: 184 Block180: // @line: 184 assume ($negInt(($eqint(($z0123), (0))))==1); assert ($neref((r2121), ($null))==1); // @line: 185 call $r3124 := java.lang.Object$javaUtilEx.ListIterator$next$2526((r2121)); assert ($neref((r1122), ($null))==1); // @line: 185 call $z1125 := boolean$java.lang.Object$equals$32((r1122), ($r3124)); goto Block181; // @line: 184 Block179: assume ($eqint(($z0123), (0))==1); goto Block173; // @line: 181 Block175: goto Block177, Block176; // @line: 188 Block173: // @line: 188 __ret := -1; return; // @line: 185 Block181: goto Block183, Block182; // @line: 181 Block177: // @line: 181 assume ($negInt(($neref(($r4128), ($null))))==1); assert ($neref((r2121), ($null))==1); // @line: 182 call $i1129 := int$javaUtilEx.ListIterator$previousIndex$2530((r2121)); // @line: 182 __ret := $i1129; return; // @line: 181 Block176: assume ($neref(($r4128), ($null))==1); goto Block170; // @line: 185 Block183: // @line: 185 assume ($negInt(($eqint(($z1125), (0))))==1); assert ($neref((r2121), ($null))==1); // @line: 186 call $i0126 := int$javaUtilEx.ListIterator$previousIndex$2530((r2121)); // @line: 186 __ret := $i0126; return; // @line: 185 Block182: assume ($eqint(($z1125), (0))==1); goto Block168; } // procedure is generated by joogie. function {:inline true} $xorreal($param00 : realVar, $param11 : realVar) returns (__ret : int); // @line: 207 // procedure boolean$javaUtilEx.AbstractCollection$addAll$2236(__this : ref, $param_0 : ref) returns (__ret : int, $Exep0 : ref) requires ($neref((__this), ($null))==1); { var $r340 : ref; var z242 : int; var r237 : ref; var $z038 : int; var $z141 : int; var r135 : ref; var r039 : ref; //temp local variables var $caughtEx1 : ref; // @line: 207 Block74: $caughtEx1 := $null; $Exep0 := $null; goto Block75; Block75: r039 := __this; r135 := $param_0; // @line: 208 z242 := 0; assert ($neref((r135), ($null))==1); // @line: 209 call r237 := javaUtilEx.Iterator$javaUtilEx.Collection$iterator$2244((r135)); goto Block76; // @line: 210 Block76: assert ($neref((r237), ($null))==1); // @line: 210 call $z038 := boolean$javaUtilEx.Iterator$hasNext$2254((r237)); goto Block77; // @line: 210 Block77: goto Block80, Block78; // @line: 210 Block80: // @line: 210 assume ($negInt(($eqint(($z038), (0))))==1); assert ($neref((r237), ($null))==1); // @line: 211 call $r340 := java.lang.Object$javaUtilEx.Iterator$next$2255((r237)); assert ($neref((r039), ($null))==1); // @line: 211 call $z141, $caughtEx1 := boolean$javaUtilEx.AbstractCollection$add$2233((r039), ($r340)); goto Block81, Block83; // @line: 210 Block78: assume ($eqint(($z038), (0))==1); goto Block79; // @line: 210 Block81: assume ($neref(($caughtEx1), ($null))==1); goto Block82; // @line: 210 Block83: assume ($eqref(($caughtEx1), ($null))==1); goto Block84; // @line: 214 Block79: // @line: 214 __ret := z242; return; // @line: 210 Block82: $Exep0 := $caughtEx1; return; // @line: 210 Block84: goto Block85; // @line: 211 Block85: goto Block86, Block87; // @line: 211 Block86: assume ($eqint(($z141), (0))==1); goto Block76; // @line: 211 Block87: // @line: 211 assume ($negInt(($eqint(($z141), (0))))==1); // @line: 212 z242 := 1; goto Block76; } // procedure is generated by joogie. function {:inline true} $andref($param00 : ref, $param11 : ref) returns (__ret : int); // @line: 98 // procedure boolean$javaUtilEx.AbstractCollection$contains$2232(__this : ref, $param_0 : ref) returns (__ret : int) requires ($neref((__this), ($null))==1); { var r28 : ref; var $z213 : int; var $r414 : ref; var $z112 : int; var r19 : ref; var $z010 : int; var $r311 : ref; var r06 : ref; Block23: r06 := __this; r19 := $param_0; assert ($neref((r06), ($null))==1); // @line: 99 call r28 := javaUtilEx.Iterator$javaUtilEx.AbstractCollection$iterator$2229((r06)); goto Block24; // @line: 100 Block24: goto Block25, Block27; // @line: 100 Block25: assume ($neref((r19), ($null))==1); goto Block26; // @line: 100 Block27: // @line: 100 assume ($negInt(($neref((r19), ($null))))==1); goto Block28; // @line: 105 Block26: assert ($neref((r28), ($null))==1); // @line: 105 call $z010 := boolean$javaUtilEx.Iterator$hasNext$2254((r28)); goto Block36; // @line: 101 Block28: assert ($neref((r28), ($null))==1); // @line: 101 call $z213 := boolean$javaUtilEx.Iterator$hasNext$2254((r28)); goto Block29; // @line: 105 Block36: goto Block37, Block38; // @line: 101 Block29: goto Block30, Block32; // @line: 105 Block37: assume ($eqint(($z010), (0))==1); goto Block31; // @line: 105 Block38: // @line: 105 assume ($negInt(($eqint(($z010), (0))))==1); assert ($neref((r28), ($null))==1); // @line: 106 call $r311 := java.lang.Object$javaUtilEx.Iterator$next$2255((r28)); assert ($neref((r19), ($null))==1); // @line: 106 call $z112 := boolean$java.lang.Object$equals$32((r19), ($r311)); goto Block39; // @line: 101 Block30: assume ($eqint(($z213), (0))==1); goto Block31; // @line: 101 Block32: // @line: 101 assume ($negInt(($eqint(($z213), (0))))==1); assert ($neref((r28), ($null))==1); // @line: 102 call $r414 := java.lang.Object$javaUtilEx.Iterator$next$2255((r28)); goto Block33; // @line: 109 Block31: // @line: 109 __ret := 0; return; // @line: 106 Block39: goto Block40, Block41; // @line: 102 Block33: goto Block35, Block34; // @line: 106 Block40: assume ($eqint(($z112), (0))==1); goto Block26; // @line: 106 Block41: // @line: 106 assume ($negInt(($eqint(($z112), (0))))==1); // @line: 107 __ret := 1; return; // @line: 102 Block35: // @line: 102 assume ($negInt(($neref(($r414), ($null))))==1); // @line: 103 __ret := 1; return; // @line: 102 Block34: assume ($neref(($r414), ($null))==1); goto Block28; } // @line: 517 // procedure java.lang.Object$javaUtilEx.LinkedList$pollFirst$2658(__this : ref) returns (__ret : ref, $Exep0 : ref) requires ($neref((__this), ($null))==1); { var $i0693 : int; var $r1694 : ref; var r0692 : ref; //temp local variables var $caughtEx1 : ref; // @line: 517 Block1038: $caughtEx1 := $null; $Exep0 := $null; goto Block1039; Block1039: r0692 := __this; assert ($neref((r0692), ($null))==1); // @line: 518 $i0693 := $HeapVar[r0692, int$javaUtilEx.LinkedList$size0]; goto Block1040; // @line: 518 Block1040: goto Block1041, Block1043; // @line: 518 Block1041: assume ($neint(($i0693), (0))==1); goto Block1042; // @line: 518 Block1043: // @line: 518 assume ($negInt(($neint(($i0693), (0))))==1); // @line: 519 __ret := $null; return; // @line: 520 Block1042: assert ($neref((r0692), ($null))==1); // @line: 520 call $r1694, $caughtEx1 := java.lang.Object$javaUtilEx.LinkedList$removeFirst$2633((r0692)); goto Block1044, Block1046; // @line: 520 Block1044: assume ($neref(($caughtEx1), ($null))==1); goto Block1045; // @line: 520 Block1046: assume ($eqref(($caughtEx1), ($null))==1); goto Block1047; // @line: 520 Block1045: $Exep0 := $caughtEx1; return; // @line: 520 Block1047: goto Block1048; // @line: 520 Block1048: // @line: 520 __ret := $r1694; return; } // procedure is generated by joogie. function {:inline true} $cmpreal(x : realVar, y : realVar) returns (__ret : int) { if ($ltreal((x), (y)) == 1) then 1 else if ($eqreal((x), (y)) == 1) then 0 else -1 } // @line: 330 // (javaUtilEx.AbstractList,javaUtilEx.AbstractList$1)> procedure void$javaUtilEx.AbstractList$Itr$$la$init$ra$$2539(__this : ref, $param_0 : ref, $param_1 : ref) requires ($neref((__this), ($null))==1); { var r0258 : ref; var r2260 : ref; var r1259 : ref; Block403: r0258 := __this; r1259 := $param_0; r2260 := $param_1; assert ($neref((r0258), ($null))==1); // @line: 331 call void$javaUtilEx.AbstractList$Itr$$la$init$ra$$2534((r0258), (r1259)); return; } // procedure is generated by joogie. function {:inline true} $ltint(x : int, y : int) returns (__ret : int) { if (x < y) then 1 else 0 } // @line: 752 // procedure javaUtilEx.List$javaUtilEx.SubList$subList$2560(__this : ref, $param_0 : int, $param_1 : int) returns (__ret : ref, $Exep1 : ref, $Exep0 : ref) requires ($neref((__this), ($null))==1); { var i1399 : int; var $r1396 : ref; var i0398 : int; var r0397 : ref; //temp local variables var $caughtEx3 : ref; var $caughtEx2 : ref; // @line: 752 Block636: $caughtEx3 := $null; $caughtEx2 := $null; $Exep1 := $null; $Exep0 := $null; goto Block637; Block637: r0397 := __this; i0398 := $param_0; i1399 := $param_1; // @line: 753 $r1396 := $newvariable((638)); assume ($neref(($newvariable((638))), ($null))==1); assert ($neref(($r1396), ($null))==1); // @line: 753 call $caughtEx2, $caughtEx3 := void$javaUtilEx.SubList$$la$init$ra$$2549(($r1396), (r0397), (i0398), (i1399)); goto Block639, Block641; Block639: assume ($neref(($caughtEx2), ($null))==1); goto Block640; Block641: assume ($eqref(($caughtEx2), ($null))==1); goto Block642; Block640: $Exep1 := $caughtEx2; return; Block642: goto Block643, Block645; Block643: assume ($neref(($caughtEx3), ($null))==1); goto Block644; Block645: assume ($eqref(($caughtEx3), ($null))==1); goto Block646; Block644: $Exep0 := $caughtEx3; return; Block646: // @line: 753 __ret := $r1396; return; } // @line: 90 // procedure javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$access$300$2672($param_0 : ref, $param_1 : ref, $param_2 : ref) returns (__ret : ref) { var r2770 : ref; var r0768 : ref; var $r3771 : ref; var r1769 : ref; Block1149: r0768 := $param_0; r1769 := $param_1; r2770 := $param_2; assert ($neref((r0768), ($null))==1); // @line: 91 call $r3771 := javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$addBefore$2665((r0768), (r1769), (r2770)); // @line: 91 __ret := $r3771; return; } // @line: 391 // (javaUtilEx.AbstractList,int)> procedure void$javaUtilEx.AbstractList$ListItr$$la$init$ra$$2542(__this : ref, $param_0 : ref, $param_1 : int) modifies $HeapVar; requires ($neref((__this), ($null))==1); { var r0269 : ref; var r1270 : ref; var i0271 : int; Block424: r0269 := __this; r1270 := $param_0; i0271 := $param_1; assert ($neref((r0269), ($null))==1); // @line: 392 $HeapVar[r0269, javaUtilEx.AbstractList$javaUtilEx.AbstractList$ListItr$this$0296] := r1270; assert ($neref((r0269), ($null))==1); // @line: 392 call void$javaUtilEx.AbstractList$Itr$$la$init$ra$$2539((r0269), (r1270), ($null)); assert ($neref((r0269), ($null))==1); // @line: 393 $HeapVar[r0269, int$javaUtilEx.AbstractList$Itr$cursor0] := i0271; return; } // @line: 730 // procedure int$javaUtilEx.SubList$1$previousIndex$2699(__this : ref) returns (__ret : int) requires ($neref((__this), ($null))==1); { var $r2940 : ref; var $r1938 : ref; var $i1941 : int; var $i0939 : int; var $i2942 : int; var r0937 : ref; Block1338: r0937 := __this; assert ($neref((r0937), ($null))==1); // @line: 731 $r1938 := $HeapVar[r0937, javaUtilEx.ListIterator$javaUtilEx.SubList$1$i308]; assert ($neref(($r1938), ($null))==1); // @line: 731 call $i0939 := int$javaUtilEx.ListIterator$previousIndex$2530(($r1938)); assert ($neref((r0937), ($null))==1); // @line: 731 $r2940 := $HeapVar[r0937, javaUtilEx.SubList$javaUtilEx.SubList$1$this$0309]; // @line: 731 call $i1941 := int$javaUtilEx.SubList$access$000$2565(($r2940)); // @line: 731 $i2942 := $subint(($i0939), ($i1941)); // @line: 731 __ret := $i2942; return; } // procedure is generated by joogie. function {:inline true} $mulint($param00 : int, $param11 : int) returns (__ret : int); // procedure is generated by joogie. function {:inline true} $ltref($param00 : ref, $param11 : ref) returns (__ret : int); // procedure is generated by joogie. function {:inline true} $mulreal($param00 : realVar, $param11 : realVar) returns (__ret : realVar); // procedure boolean$javaUtilEx.Collection$contains$2243(__this : ref, $param_0 : ref) returns (__ret : int); // @line: 652 // procedure void$javaUtilEx.SubList$add$2553(__this : ref, $param_0 : int, $param_1 : ref) returns ($Exep1 : ref, $Exep0 : ref, $Exep2 : ref) modifies $HeapVar; requires ($neref((__this), ($null))==1); { var $i3347 : int; var r1343 : ref; var $r3346 : ref; var $i4348 : int; var $i1342 : int; var i0341 : int; var $i5349 : int; var $i2344 : int; var r0340 : ref; var $r2345 : ref; //temp local variables var $caughtEx4 : ref; var $caughtEx5 : ref; var $caughtEx3 : ref; // @line: 652 Block539: $caughtEx5 := $null; $caughtEx4 := $null; $caughtEx3 := $null; $Exep2 := $null; $Exep1 := $null; $Exep0 := $null; goto Block540; Block540: r0340 := __this; i0341 := $param_0; r1343 := $param_1; assert ($neref((r0340), ($null))==1); // @line: 653 call $caughtEx3 := void$javaUtilEx.SubList$rangeCheckForAdd$2562((r0340), (i0341)); goto Block541, Block543; Block541: assume ($neref(($caughtEx3), ($null))==1); goto Block542; Block543: assume ($eqref(($caughtEx3), ($null))==1); goto Block544; Block542: $Exep0 := $caughtEx3; return; Block544: assert ($neref((r0340), ($null))==1); // @line: 654 call $caughtEx4 := void$javaUtilEx.SubList$checkForComodification$2564((r0340)); goto Block545, Block547; Block545: assume ($neref(($caughtEx4), ($null))==1); goto Block546; Block547: assume ($eqref(($caughtEx4), ($null))==1); goto Block548; Block546: $Exep1 := $caughtEx4; return; Block548: assert ($neref((r0340), ($null))==1); // @line: 655 $r2345 := $HeapVar[r0340, javaUtilEx.AbstractList$javaUtilEx.SubList$l297]; assert ($neref((r0340), ($null))==1); // @line: 655 $i1342 := $HeapVar[r0340, int$javaUtilEx.SubList$offset0]; // @line: 655 $i2344 := $addint((i0341), ($i1342)); assert ($neref(($r2345), ($null))==1); // @line: 655 call $caughtEx5 := void$javaUtilEx.AbstractList$add$2487(($r2345), ($i2344), (r1343)); goto Block551, Block549; Block551: assume ($eqref(($caughtEx5), ($null))==1); goto Block552; Block549: assume ($neref(($caughtEx5), ($null))==1); goto Block550; Block552: assert ($neref((r0340), ($null))==1); // @line: 656 $r3346 := $HeapVar[r0340, javaUtilEx.AbstractList$javaUtilEx.SubList$l297]; assert ($neref(($r3346), ($null))==1); // @line: 656 $i3347 := $HeapVar[$r3346, int$javaUtilEx.AbstractList$modCount0]; assert ($neref((r0340), ($null))==1); // @line: 656 $HeapVar[r0340, int$javaUtilEx.AbstractList$modCount0] := $i3347; assert ($neref((r0340), ($null))==1); // @line: 657 $i4348 := $HeapVar[r0340, int$javaUtilEx.SubList$size0]; // @line: 657 $i5349 := $addint(($i4348), (1)); assert ($neref((r0340), ($null))==1); // @line: 657 $HeapVar[r0340, int$javaUtilEx.SubList$size0] := $i5349; return; Block550: $Exep2 := $caughtEx5; return; } // procedure is generated by joogie. function {:inline true} $ushrreal($param00 : realVar, $param11 : realVar) returns (__ret : int); // @line: 484 // procedure javaUtilEx.List$javaUtilEx.AbstractList$subList$2496(__this : ref, $param_0 : int, $param_1 : int) returns (__ret : ref, $Exep1 : ref, $Exep0 : ref) requires ($neref((__this), ($null))==1); { var $r1169 : ref; var i1167 : int; var r3171 : ref; var r0163 : ref; var i0166 : int; var r2170 : ref; var $z0164 : int; //temp local variables var $caughtEx2 : ref; var $caughtEx3 : ref; // @line: 484 Block245: $caughtEx3 := $null; $caughtEx2 := $null; $Exep1 := $null; $Exep0 := $null; goto Block246; Block246: r0163 := __this; i0166 := $param_0; i1167 := $param_1; // @line: 485 $z0164 := $instanceof((r0163), (javaUtilEx.RandomAccess)); goto Block247; // @line: 485 Block247: goto Block248, Block250; // @line: 485 Block248: assume ($eqint(($z0164), (0))==1); goto Block249; // @line: 485 Block250: // @line: 485 assume ($negInt(($eqint(($z0164), (0))))==1); // @line: 485 r2170 := $newvariable((251)); assume ($neref(($newvariable((251))), ($null))==1); $r1169 := r2170; assert ($neref((r2170), ($null))==1); // @line: 485 call $caughtEx2, $caughtEx3 := void$javaUtilEx.RandomAccessSubList$$la$init$ra$$2540((r2170), (r0163), (i0166), (i1167)); goto Block252, Block254; // @line: 485 Block249: // @line: 485 r3171 := $newvariable((261)); assume ($neref(($newvariable((261))), ($null))==1); goto Block262; // @line: 485 Block252: assume ($neref(($caughtEx2), ($null))==1); goto Block253; // @line: 485 Block254: assume ($eqref(($caughtEx2), ($null))==1); goto Block255; Block262: $r1169 := r3171; assert ($neref((r3171), ($null))==1); // @line: 485 call $caughtEx2, $caughtEx3 := void$javaUtilEx.SubList$$la$init$ra$$2549((r3171), (r0163), (i0166), (i1167)); goto Block265, Block263; // @line: 485 Block253: $Exep1 := $caughtEx2; return; // @line: 485 Block255: goto Block256, Block258; Block265: assume ($eqref(($caughtEx2), ($null))==1); goto Block266; Block263: assume ($neref(($caughtEx2), ($null))==1); goto Block264; // @line: 485 Block256: assume ($neref(($caughtEx3), ($null))==1); goto Block257; // @line: 485 Block258: assume ($eqref(($caughtEx3), ($null))==1); goto Block259; Block266: goto Block269, Block267; Block264: $Exep1 := $caughtEx2; return; // @line: 485 Block257: $Exep0 := $caughtEx3; return; // @line: 485 Block259: goto Block260; Block269: assume ($eqref(($caughtEx3), ($null))==1); goto Block270; Block267: assume ($neref(($caughtEx3), ($null))==1); goto Block268; // @line: 485 Block260: // @line: 485 __ret := $r1169; return; Block270: goto Block260; Block268: $Exep0 := $caughtEx3; return; } // @line: 607 // procedure void$javaUtilEx.AbstractList$rangeCheckForAdd$2500(__this : ref, $param_0 : int) returns ($Exep0 : ref) modifies $stringSize; requires ($neref((__this), ($null))==1); { var i0211 : int; var r0213 : ref; var $r1212 : ref; var $r2214 : ref; var $i1215 : int; //temp local variables // @line: 607 Block157: $Exep0 := $null; goto Block335; Block335: r0213 := __this; i0211 := $param_0; goto Block336; // @line: 608 Block336: goto Block337, Block339; // @line: 608 Block337: assume ($ltint((i0211), (0))==1); goto Block338; // @line: 608 Block339: // @line: 608 assume ($negInt(($ltint((i0211), (0))))==1); assert ($neref((r0213), ($null))==1); // @line: 609 call $i1215 := int$javaUtilEx.AbstractCollection$size$2230((r0213)); goto Block340; // @line: 609 Block338: // @line: 609 $r1212 := $newvariable((344)); assume ($neref(($newvariable((344))), ($null))==1); assert ($neref((r0213), ($null))==1); // @line: 609 call $r2214 := java.lang.String$javaUtilEx.AbstractList$outOfBoundsMsg$2501((r0213), (i0211)); assert ($neref(($r1212), ($null))==1); // @line: 609 call void$java.lang.IndexOutOfBoundsException$$la$init$ra$$2076(($r1212), ($r2214)); goto Block345; // @line: 609 Block340: goto Block341, Block343; // @line: 609 Block345: $Exep0 := $r1212; return; // @line: 609 Block341: assume ($leint((i0211), ($i1215))==1); goto Block342; // @line: 609 Block343: // @line: 609 assume ($negInt(($leint((i0211), ($i1215))))==1); goto Block338; // @line: 610 Block342: return; } // @line: 539 // procedure int$javaUtilEx.AbstractList$hashCode$2498(__this : ref) returns (__ret : int) requires ($neref((__this), ($null))==1); { var i1200 : int; var $i0198 : int; var r0192 : ref; var r2197 : ref; var r1194 : ref; var $z0195 : int; var $i2201 : int; Block314: r0192 := __this; // @line: 540 i1200 := 1; assert ($neref((r0192), ($null))==1); // @line: 541 call r1194 := javaUtilEx.Iterator$javaUtilEx.AbstractList$iterator$2493((r0192)); goto Block315; // @line: 542 Block315: assert ($neref((r1194), ($null))==1); // @line: 542 call $z0195 := boolean$javaUtilEx.Iterator$hasNext$2254((r1194)); goto Block316; // @line: 542 Block316: goto Block319, Block317; // @line: 542 Block319: // @line: 542 assume ($negInt(($eqint(($z0195), (0))))==1); assert ($neref((r1194), ($null))==1); // @line: 543 call r2197 := java.lang.Object$javaUtilEx.Iterator$next$2255((r1194)); // @line: 544 $i0198 := $mulint((31), (i1200)); goto Block320; // @line: 542 Block317: assume ($eqint(($z0195), (0))==1); goto Block318; // @line: 544 Block320: goto Block321, Block323; // @line: 546 Block318: // @line: 546 __ret := i1200; return; // @line: 544 Block321: assume ($neref((r2197), ($null))==1); goto Block322; // @line: 544 Block323: // @line: 544 assume ($negInt(($neref((r2197), ($null))))==1); // @line: 542 $i2201 := 0; goto Block324; // @line: 544 Block322: assert ($neref((r2197), ($null))==1); // @line: 544 call $i2201 := int$java.lang.Object$hashCode$31((r2197)); goto Block324; // @line: 544 Block324: // @line: 544 i1200 := $addint(($i0198), ($i2201)); goto Block325; // @line: 545 Block325: goto Block315; } // @line: 704 // procedure void$javaUtilEx.LinkedList$ListItr$set$2685(__this : ref, $param_0 : ref) returns ($Exep1 : ref, $Exep0 : ref) modifies $HeapVar; requires ($neref((__this), ($null))==1); { var $r6867 : ref; var r0861 : ref; var $r2862 : ref; var r1865 : ref; var $r4864 : ref; var $r3863 : ref; var $r5866 : ref; //temp local variables var $caughtEx2 : ref; // @line: 704 Block1244: $caughtEx2 := $null; $Exep1 := $null; $Exep0 := $null; goto Block1245; Block1245: r0861 := __this; r1865 := $param_0; assert ($neref((r0861), ($null))==1); // @line: 705 $r3863 := $HeapVar[r0861, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$ListItr$lastReturned303]; assert ($neref((r0861), ($null))==1); // @line: 705 $r2862 := $HeapVar[r0861, javaUtilEx.LinkedList$javaUtilEx.LinkedList$ListItr$this$0305]; // @line: 705 call $r4864 := javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$access$000$2669(($r2862)); goto Block1246; // @line: 705 Block1246: goto Block1249, Block1247; // @line: 705 Block1249: // @line: 705 assume ($negInt(($neref(($r3863), ($r4864))))==1); // @line: 706 $r6867 := $newvariable((1250)); assume ($neref(($newvariable((1250))), ($null))==1); assert ($neref(($r6867), ($null))==1); // @line: 706 call void$javaUtilEx.IllegalStateException$$la$init$ra$$2574(($r6867)); goto Block1251; // @line: 705 Block1247: assume ($neref(($r3863), ($r4864))==1); goto Block1248; // @line: 705 Block1251: $Exep0 := $r6867; return; // @line: 707 Block1248: assert ($neref((r0861), ($null))==1); // @line: 707 call $caughtEx2 := void$javaUtilEx.LinkedList$ListItr$checkForComodification$2687((r0861)); goto Block1252, Block1254; // @line: 707 Block1252: assume ($neref(($caughtEx2), ($null))==1); goto Block1253; // @line: 707 Block1254: assume ($eqref(($caughtEx2), ($null))==1); goto Block1255; // @line: 707 Block1253: $Exep1 := $caughtEx2; return; // @line: 707 Block1255: goto Block1256; // @line: 708 Block1256: assert ($neref((r0861), ($null))==1); // @line: 708 $r5866 := $HeapVar[r0861, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$ListItr$lastReturned303]; assert ($neref(($r5866), ($null))==1); // @line: 708 $HeapVar[$r5866, java.lang.Object$javaUtilEx.LinkedList$Entry$element300] := r1865; return; } // procedure is generated by joogie. function {:inline true} $cmpref(x : ref, y : ref) returns (__ret : int) { if ($ltref((x), (y)) == 1) then 1 else if ($eqref((x), (y)) == 1) then 0 else -1 } // procedure java.lang.StringBuilder$java.lang.StringBuilder$append$2265(__this : ref, $param_0 : ref) returns (__ret : ref); // @line: 770 // procedure void$javaUtilEx.SubList$checkForComodification$2564(__this : ref) returns ($Exep0 : ref) requires ($neref((__this), ($null))==1); { var $r2416 : ref; var r0412 : ref; var $r1413 : ref; var $i1415 : int; var $i0414 : int; //temp local variables // @line: 770 Block508: $Exep0 := $null; goto Block670; Block670: r0412 := __this; assert ($neref((r0412), ($null))==1); // @line: 771 $i1415 := $HeapVar[r0412, int$javaUtilEx.AbstractList$modCount0]; assert ($neref((r0412), ($null))==1); // @line: 771 $r1413 := $HeapVar[r0412, javaUtilEx.AbstractList$javaUtilEx.SubList$l297]; assert ($neref(($r1413), ($null))==1); // @line: 771 $i0414 := $HeapVar[$r1413, int$javaUtilEx.AbstractList$modCount0]; goto Block671; // @line: 771 Block671: goto Block672, Block674; // @line: 771 Block672: assume ($eqint(($i1415), ($i0414))==1); goto Block673; // @line: 771 Block674: // @line: 771 assume ($negInt(($eqint(($i1415), ($i0414))))==1); // @line: 772 $r2416 := $newvariable((675)); assume ($neref(($newvariable((675))), ($null))==1); assert ($neref(($r2416), ($null))==1); // @line: 772 call void$javaUtilEx.ConcurrentModificationException$$la$init$ra$$2570(($r2416)); goto Block676; // @line: 773 Block673: return; // @line: 771 Block676: $Exep0 := $r2416; return; } // @line: 232 // procedure boolean$javaUtilEx.LinkedList$remove$2640(__this : ref, $param_0 : ref) returns (__ret : int, $Exep0 : ref) requires ($neref((__this), ($null))==1); { var r11596 : ref; var $r3587 : ref; var r1583 : ref; var $r2585 : ref; var $r7592 : ref; var r0584 : ref; var $r6591 : ref; var r10595 : ref; var $r8593 : ref; var $z0589 : int; var $r4588 : ref; //temp local variables var $caughtEx1 : ref; var $freshlocal3 : ref; var $freshlocal2 : ref; // @line: 232 Block828: $caughtEx1 := $null; $Exep0 := $null; goto Block829; Block829: r0584 := __this; r1583 := $param_0; goto Block830; // @line: 233 Block830: goto Block833, Block831; // @line: 233 Block833: // @line: 233 assume ($negInt(($neref((r1583), ($null))))==1); assert ($neref((r0584), ($null))==1); // @line: 234 $r6591 := $HeapVar[r0584, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$header298]; assert ($neref(($r6591), ($null))==1); // @line: 234 r10595 := $HeapVar[$r6591, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$next301]; goto Block834; // @line: 233 Block831: assume ($neref((r1583), ($null))==1); goto Block832; // @line: 234 Block834: assert ($neref((r0584), ($null))==1); // @line: 234 $r7592 := $HeapVar[r0584, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$header298]; goto Block835; // @line: 241 Block832: assert ($neref((r0584), ($null))==1); // @line: 241 $r2585 := $HeapVar[r0584, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$header298]; goto Block849; // @line: 234 Block835: goto Block836, Block838; // @line: 241 Block849: assert ($neref(($r2585), ($null))==1); // @line: 241 r11596 := $HeapVar[$r2585, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$next301]; goto Block850; // @line: 234 Block836: assume ($eqref((r10595), ($r7592))==1); goto Block837; // @line: 234 Block838: // @line: 234 assume ($negInt(($eqref((r10595), ($r7592))))==1); assert ($neref((r10595), ($null))==1); // @line: 235 $r8593 := $HeapVar[r10595, java.lang.Object$javaUtilEx.LinkedList$Entry$element300]; goto Block839; // @line: 241 Block850: assert ($neref((r0584), ($null))==1); // @line: 241 $r3587 := $HeapVar[r0584, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$header298]; goto Block851; // @line: 234 Block837: goto Block848; // @line: 235 Block839: goto Block840, Block842; // @line: 241 Block851: goto Block852, Block853; // @line: 248 Block848: // @line: 248 __ret := 0; return; // @line: 235 Block840: assume ($neref(($r8593), ($null))==1); goto Block841; // @line: 235 Block842: // @line: 235 assume ($negInt(($neref(($r8593), ($null))))==1); assert ($neref((r0584), ($null))==1); // @line: 236 call $freshlocal2, $caughtEx1 := java.lang.Object$javaUtilEx.LinkedList$remove$2666((r0584), (r10595)); goto Block843, Block845; // @line: 241 Block852: assume ($eqref((r11596), ($r3587))==1); goto Block848; // @line: 241 Block853: // @line: 241 assume ($negInt(($eqref((r11596), ($r3587))))==1); assert ($neref((r11596), ($null))==1); // @line: 242 $r4588 := $HeapVar[r11596, java.lang.Object$javaUtilEx.LinkedList$Entry$element300]; assert ($neref((r1583), ($null))==1); // @line: 242 call $z0589 := boolean$java.lang.Object$equals$32((r1583), ($r4588)); goto Block854; // @line: 234 Block841: assert ($neref((r10595), ($null))==1); // @line: 234 r10595 := $HeapVar[r10595, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$next301]; goto Block847; // @line: 235 Block843: assume ($neref(($caughtEx1), ($null))==1); goto Block844; // @line: 235 Block845: assume ($eqref(($caughtEx1), ($null))==1); goto Block846; // @line: 242 Block854: goto Block857, Block855; // @line: 234 Block847: goto Block834; // @line: 235 Block844: $Exep0 := $caughtEx1; return; // @line: 235 Block846: // @line: 237 __ret := 1; return; // @line: 242 Block857: // @line: 242 assume ($negInt(($eqint(($z0589), (0))))==1); assert ($neref((r0584), ($null))==1); // @line: 243 call $freshlocal3, $caughtEx1 := java.lang.Object$javaUtilEx.LinkedList$remove$2666((r0584), (r11596)); goto Block858, Block860; // @line: 242 Block855: assume ($eqint(($z0589), (0))==1); goto Block856; // @line: 242 Block858: assume ($neref(($caughtEx1), ($null))==1); goto Block859; // @line: 242 Block860: assume ($eqref(($caughtEx1), ($null))==1); goto Block861; // @line: 241 Block856: assert ($neref((r11596), ($null))==1); // @line: 241 r11596 := $HeapVar[r11596, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$next301]; goto Block862; // @line: 242 Block859: $Exep0 := $caughtEx1; return; // @line: 242 Block861: // @line: 244 __ret := 1; return; // @line: 241 Block862: goto Block850; } // @line: 74 // (java.lang.String,java.lang.Throwable)> procedure void$javaUtilEx.IllegalStateException$$la$init$ra$$2576(__this : ref, $param_0 : ref, $param_1 : ref) requires ($neref((__this), ($null))==1); { var r1439 : ref; var r2440 : ref; var r0438 : ref; Block688: r0438 := __this; r1439 := $param_0; r2440 := $param_1; assert ($neref((r0438), ($null))==1); // @line: 75 call void$java.lang.RuntimeException$$la$init$ra$$762((r0438), (r1439), (r2440)); return; } // @line: 27 // (int)> procedure void$javaUtilEx.Content$$la$init$ra$$2586(__this : ref, $param_0 : int) modifies $HeapVar; requires ($neref((__this), ($null))==1); { var i0496 : int; var r0495 : ref; Block737: r0495 := __this; i0496 := $param_0; assert ($neref((r0495), ($null))==1); // @line: 28 call void$java.lang.Object$$la$init$ra$$28((r0495)); assert ($neref((r0495), ($null))==1); // @line: 29 $HeapVar[r0495, int$javaUtilEx.Content$val0] := i0496; return; } // @line: 651 // procedure boolean$javaUtilEx.LinkedList$ListItr$hasNext$2678(__this : ref) returns (__ret : int) requires ($neref((__this), ($null))==1); { var $i0810 : int; var $i1811 : int; var $r1809 : ref; var $z0813 : int; var r0808 : ref; Block1180: r0808 := __this; assert ($neref((r0808), ($null))==1); // @line: 652 $i0810 := $HeapVar[r0808, int$javaUtilEx.LinkedList$ListItr$nextIndex0]; assert ($neref((r0808), ($null))==1); // @line: 652 $r1809 := $HeapVar[r0808, javaUtilEx.LinkedList$javaUtilEx.LinkedList$ListItr$this$0305]; // @line: 652 call $i1811 := int$javaUtilEx.LinkedList$access$100$2670(($r1809)); goto Block1181; // @line: 652 Block1181: goto Block1182, Block1184; // @line: 652 Block1182: assume ($eqint(($i0810), ($i1811))==1); goto Block1183; // @line: 652 Block1184: // @line: 652 assume ($negInt(($eqint(($i0810), ($i1811))))==1); // @line: 652 $z0813 := 1; goto Block1185; // @line: 652 Block1183: // @line: 652 $z0813 := 0; goto Block1185; // @line: 652 Block1185: // @line: 652 __ret := $z0813; return; } // @line: 131 // procedure java.lang.Object$javaUtilEx.AbstractList$set$2486(__this : ref, $param_0 : int, $param_1 : ref) returns (__ret : ref, $Exep0 : ref) requires ($neref((__this), ($null))==1); { var r0109 : ref; var i0110 : int; var $r2108 : ref; var r1111 : ref; //temp local variables // @line: 131 Block146: $Exep0 := $null; goto Block147; Block147: r0109 := __this; i0110 := $param_0; r1111 := $param_1; // @line: 132 $r2108 := $newvariable((148)); assume ($neref(($newvariable((148))), ($null))==1); assert ($neref(($r2108), ($null))==1); // @line: 132 call void$javaUtilEx.UnsupportedOperationException$$la$init$ra$$2257(($r2108)); goto Block149; Block149: $Exep0 := $r2108; return; } // @line: 100 // ()> procedure void$javaUtilEx.LinkedList$$la$init$ra$$2629(__this : ref) modifies $HeapVar; requires ($neref((__this), ($null))==1); { var $r2537 : ref; var r0535 : ref; var $r3538 : ref; var $r4539 : ref; var $r1536 : ref; Block780: r0535 := __this; assert ($neref((r0535), ($null))==1); // @line: 101 call void$javaUtilEx.AbstractSequentialList$$la$init$ra$$2578((r0535)); // @line: 95 $r1536 := $newvariable((781)); assume ($neref(($newvariable((781))), ($null))==1); assert ($neref(($r1536), ($null))==1); // @line: 95 call void$javaUtilEx.LinkedList$Entry$$la$init$ra$$2676(($r1536), ($null), ($null), ($null)); assert ($neref((r0535), ($null))==1); // @line: 95 $HeapVar[r0535, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$header298] := $r1536; assert ($neref((r0535), ($null))==1); // @line: 96 $HeapVar[r0535, int$javaUtilEx.LinkedList$size0] := 0; assert ($neref((r0535), ($null))==1); // @line: 102 $r4539 := $HeapVar[r0535, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$header298]; assert ($neref((r0535), ($null))==1); // @line: 102 $r3538 := $HeapVar[r0535, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$header298]; assert ($neref((r0535), ($null))==1); // @line: 102 $r2537 := $HeapVar[r0535, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$header298]; assert ($neref(($r3538), ($null))==1); // @line: 102 $HeapVar[$r3538, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$previous302] := $r2537; assert ($neref(($r4539), ($null))==1); // @line: 102 $HeapVar[$r4539, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$next301] := $r2537; return; } // @line: 489 // procedure java.lang.Object$javaUtilEx.LinkedList$peekFirst$2656(__this : ref) returns (__ret : ref, $Exep0 : ref) requires ($neref((__this), ($null))==1); { var r0686 : ref; var $r1688 : ref; var $i0687 : int; //temp local variables var $caughtEx1 : ref; // @line: 489 Block1016: $caughtEx1 := $null; $Exep0 := $null; goto Block1017; Block1017: r0686 := __this; assert ($neref((r0686), ($null))==1); // @line: 490 $i0687 := $HeapVar[r0686, int$javaUtilEx.LinkedList$size0]; goto Block1018; // @line: 490 Block1018: goto Block1021, Block1019; // @line: 490 Block1021: // @line: 490 assume ($negInt(($neint(($i0687), (0))))==1); // @line: 491 __ret := $null; return; // @line: 490 Block1019: assume ($neint(($i0687), (0))==1); goto Block1020; // @line: 492 Block1020: assert ($neref((r0686), ($null))==1); // @line: 492 call $r1688, $caughtEx1 := java.lang.Object$javaUtilEx.LinkedList$getFirst$2631((r0686)); goto Block1022, Block1024; // @line: 492 Block1022: assume ($neref(($caughtEx1), ($null))==1); goto Block1023; // @line: 492 Block1024: assume ($eqref(($caughtEx1), ($null))==1); goto Block1025; // @line: 492 Block1023: $Exep0 := $caughtEx1; return; // @line: 492 Block1025: goto Block1026; // @line: 492 Block1026: // @line: 492 __ret := $r1688; return; } // @line: 150 // procedure java.lang.Object$javaUtilEx.LinkedList$removeFirst$2633(__this : ref) returns (__ret : ref, $Exep0 : ref) requires ($neref((__this), ($null))==1); { var $r2557 : ref; var r0555 : ref; var $r1556 : ref; var $r3558 : ref; //temp local variables var $caughtEx1 : ref; // @line: 150 Block806: $caughtEx1 := $null; $Exep0 := $null; goto Block807; Block807: r0555 := __this; assert ($neref((r0555), ($null))==1); // @line: 151 $r1556 := $HeapVar[r0555, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$header298]; assert ($neref(($r1556), ($null))==1); // @line: 151 $r2557 := $HeapVar[$r1556, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$next301]; assert ($neref((r0555), ($null))==1); // @line: 151 call $r3558, $caughtEx1 := java.lang.Object$javaUtilEx.LinkedList$remove$2666((r0555), ($r2557)); goto Block808, Block810; Block808: assume ($neref(($caughtEx1), ($null))==1); goto Block809; Block810: assume ($eqref(($caughtEx1), ($null))==1); goto Block811; Block809: $Exep0 := $caughtEx1; return; Block811: // @line: 151 __ret := $r3558; return; } // procedure is generated by joogie. function {:inline true} $eqintarray($param00 : [int]int, $param11 : [int]int) returns (__ret : int); // procedure is generated by joogie. function {:inline true} $lereal($param00 : realVar, $param11 : realVar) returns (__ret : int); // @line: 353 // procedure int$javaUtilEx.LinkedList$indexOf$2647(__this : ref, $param_0 : ref) returns (__ret : int) requires ($neref((__this), ($null))==1); { var $r5649 : ref; var $r3646 : ref; var $r4647 : ref; var $z0648 : int; var r0643 : ref; var i0652 : int; var $r2644 : ref; var r1642 : ref; var r8653 : ref; var $r7651 : ref; var r9654 : ref; var $r6650 : ref; Block927: r0643 := __this; r1642 := $param_0; // @line: 354 i0652 := 0; goto Block928; // @line: 355 Block928: goto Block931, Block929; // @line: 355 Block931: // @line: 355 assume ($negInt(($neref((r1642), ($null))))==1); assert ($neref((r0643), ($null))==1); // @line: 356 $r5649 := $HeapVar[r0643, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$header298]; assert ($neref(($r5649), ($null))==1); // @line: 356 r8653 := $HeapVar[$r5649, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$next301]; goto Block932; // @line: 355 Block929: assume ($neref((r1642), ($null))==1); goto Block930; // @line: 356 Block932: assert ($neref((r0643), ($null))==1); // @line: 356 $r6650 := $HeapVar[r0643, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$header298]; goto Block933; // @line: 362 Block930: assert ($neref((r0643), ($null))==1); // @line: 362 $r2644 := $HeapVar[r0643, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$header298]; goto Block943; // @line: 356 Block933: goto Block934, Block936; // @line: 362 Block943: assert ($neref(($r2644), ($null))==1); // @line: 362 r9654 := $HeapVar[$r2644, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$next301]; goto Block944; // @line: 356 Block934: assume ($eqref((r8653), ($r6650))==1); goto Block935; // @line: 356 Block936: // @line: 356 assume ($negInt(($eqref((r8653), ($r6650))))==1); assert ($neref((r8653), ($null))==1); // @line: 357 $r7651 := $HeapVar[r8653, java.lang.Object$javaUtilEx.LinkedList$Entry$element300]; goto Block937; // @line: 362 Block944: assert ($neref((r0643), ($null))==1); // @line: 362 $r3646 := $HeapVar[r0643, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$header298]; goto Block945; // @line: 356 Block935: goto Block942; // @line: 357 Block937: goto Block938, Block940; // @line: 362 Block945: goto Block947, Block946; // @line: 368 Block942: // @line: 368 __ret := -1; return; // @line: 357 Block938: assume ($neref(($r7651), ($null))==1); goto Block939; // @line: 357 Block940: // @line: 357 assume ($negInt(($neref(($r7651), ($null))))==1); // @line: 358 __ret := i0652; return; // @line: 362 Block947: // @line: 362 assume ($negInt(($eqref((r9654), ($r3646))))==1); assert ($neref((r9654), ($null))==1); // @line: 363 $r4647 := $HeapVar[r9654, java.lang.Object$javaUtilEx.LinkedList$Entry$element300]; assert ($neref((r1642), ($null))==1); // @line: 363 call $z0648 := boolean$java.lang.Object$equals$32((r1642), ($r4647)); goto Block948; // @line: 362 Block946: assume ($eqref((r9654), ($r3646))==1); goto Block942; // @line: 359 Block939: // @line: 359 i0652 := $addint((i0652), (1)); goto Block941; // @line: 363 Block948: goto Block951, Block949; // @line: 356 Block941: assert ($neref((r8653), ($null))==1); // @line: 356 r8653 := $HeapVar[r8653, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$next301]; goto Block932; // @line: 363 Block951: // @line: 363 assume ($negInt(($eqint(($z0648), (0))))==1); // @line: 364 __ret := i0652; return; // @line: 363 Block949: assume ($eqint(($z0648), (0))==1); goto Block950; // @line: 365 Block950: // @line: 365 i0652 := $addint((i0652), (1)); goto Block952; // @line: 362 Block952: assert ($neref((r9654), ($null))==1); // @line: 362 r9654 := $HeapVar[r9654, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$next301]; goto Block944; } // procedure is generated by joogie. function {:inline true} $xorref($param00 : ref, $param11 : ref) returns (__ret : int); // @line: 92 // (java.lang.Throwable)> procedure void$javaUtilEx.IllegalStateException$$la$init$ra$$2577(__this : ref, $param_0 : ref) requires ($neref((__this), ($null))==1); { var r1442 : ref; var r0441 : ref; Block689: r0441 := __this; r1442 := $param_0; assert ($neref((r0441), ($null))==1); // @line: 93 call void$java.lang.RuntimeException$$la$init$ra$$763((r0441), (r1442)); return; } // @line: 719 // procedure java.lang.Object$javaUtilEx.SubList$1$previous$2697(__this : ref) returns (__ret : ref, $Exep0 : ref) requires ($neref((__this), ($null))==1); { var r0926 : ref; var $r2929 : ref; var $r3930 : ref; var $r1928 : ref; var $z0927 : int; //temp local variables // @line: 719 Block1328: $Exep0 := $null; goto Block1329; Block1329: r0926 := __this; assert ($neref((r0926), ($null))==1); // @line: 720 call $z0927 := boolean$javaUtilEx.SubList$1$hasPrevious$2696((r0926)); goto Block1330; // @line: 720 Block1330: goto Block1333, Block1331; // @line: 720 Block1333: // @line: 720 assume ($negInt(($eqint(($z0927), (0))))==1); assert ($neref((r0926), ($null))==1); // @line: 721 $r2929 := $HeapVar[r0926, javaUtilEx.ListIterator$javaUtilEx.SubList$1$i308]; assert ($neref(($r2929), ($null))==1); // @line: 721 call $r3930 := java.lang.Object$javaUtilEx.ListIterator$previous$2528(($r2929)); // @line: 721 __ret := $r3930; return; // @line: 720 Block1331: assume ($eqint(($z0927), (0))==1); goto Block1332; // @line: 723 Block1332: // @line: 723 $r1928 := $newvariable((1334)); assume ($neref(($newvariable((1334))), ($null))==1); goto Block1335; // @line: 723 Block1335: assert ($neref(($r1928), ($null))==1); // @line: 723 call void$javaUtilEx.NoSuchElementException$$la$init$ra$$2572(($r1928)); goto Block1336; // @line: 723 Block1336: $Exep0 := $r1928; return; } // procedure is generated by joogie. function {:inline true} $intarrtoref($param00 : [int]int) returns (__ret : ref); // procedure is generated by joogie. function {:inline true} $subreal($param00 : realVar, $param11 : realVar) returns (__ret : realVar); // @line: 330 // (javaUtilEx.AbstractList)> procedure void$javaUtilEx.AbstractList$Itr$$la$init$ra$$2534(__this : ref, $param_0 : ref) modifies $HeapVar; requires ($neref((__this), ($null))==1); { var r0218 : ref; var r1219 : ref; var $i0221 : int; var $r2220 : ref; Block347: r0218 := __this; r1219 := $param_0; assert ($neref((r0218), ($null))==1); // @line: 331 $HeapVar[r0218, javaUtilEx.AbstractList$javaUtilEx.AbstractList$Itr$this$0295] := r1219; assert ($neref((r0218), ($null))==1); // @line: 331 call void$java.lang.Object$$la$init$ra$$28((r0218)); assert ($neref((r0218), ($null))==1); // @line: 335 $HeapVar[r0218, int$javaUtilEx.AbstractList$Itr$cursor0] := 0; assert ($neref((r0218), ($null))==1); // @line: 342 $HeapVar[r0218, int$javaUtilEx.AbstractList$Itr$lastRet0] := -1; assert ($neref((r0218), ($null))==1); // @line: 349 $r2220 := $HeapVar[r0218, javaUtilEx.AbstractList$javaUtilEx.AbstractList$Itr$this$0295]; assert ($neref(($r2220), ($null))==1); // @line: 349 $i0221 := $HeapVar[$r2220, int$javaUtilEx.AbstractList$modCount0]; assert ($neref((r0218), ($null))==1); // @line: 349 $HeapVar[r0218, int$javaUtilEx.AbstractList$Itr$expectedModCount0] := $i0221; return; } // @line: 147 // procedure void$javaUtilEx.AbstractList$add$2487(__this : ref, $param_0 : int, $param_1 : ref) returns ($Exep0 : ref) requires ($neref((__this), ($null))==1); { var i0114 : int; var r0113 : ref; var r1115 : ref; var $r2112 : ref; //temp local variables // @line: 147 Block139: $Exep0 := $null; goto Block150; Block150: r0113 := __this; i0114 := $param_0; r1115 := $param_1; // @line: 148 $r2112 := $newvariable((151)); assume ($neref(($newvariable((151))), ($null))==1); assert ($neref(($r2112), ($null))==1); // @line: 148 call void$javaUtilEx.UnsupportedOperationException$$la$init$ra$$2257(($r2112)); goto Block152; Block152: $Exep0 := $r2112; return; } // procedure int$javaUtilEx.ListIterator$previousIndex$2530(__this : ref) returns (__ret : int); // @line: 55 // (java.lang.String)> procedure void$javaUtilEx.NoSuchElementException$$la$init$ra$$2573(__this : ref, $param_0 : ref) requires ($neref((__this), ($null))==1); { var r0433 : ref; var r1434 : ref; Block685: r0433 := __this; r1434 := $param_0; assert ($neref((r0433), ($null))==1); // @line: 56 call void$java.lang.RuntimeException$$la$init$ra$$761((r0433), (r1434)); return; } // @line: 781 // procedure javaUtilEx.List$javaUtilEx.RandomAccessSubList$subList$2541(__this : ref, $param_0 : int, $param_1 : int) returns (__ret : ref, $Exep1 : ref, $Exep0 : ref) requires ($neref((__this), ($null))==1); { var r0266 : ref; var i1268 : int; var $r1265 : ref; var i0267 : int; //temp local variables var $caughtEx3 : ref; var $caughtEx2 : ref; // @line: 781 Block413: $caughtEx3 := $null; $caughtEx2 := $null; $Exep1 := $null; $Exep0 := $null; goto Block414; Block414: r0266 := __this; i0267 := $param_0; i1268 := $param_1; // @line: 782 $r1265 := $newvariable((415)); assume ($neref(($newvariable((415))), ($null))==1); assert ($neref(($r1265), ($null))==1); // @line: 782 call $caughtEx2, $caughtEx3 := void$javaUtilEx.RandomAccessSubList$$la$init$ra$$2540(($r1265), (r0266), (i0267), (i1268)); goto Block418, Block416; Block418: assume ($eqref(($caughtEx2), ($null))==1); goto Block419; Block416: assume ($neref(($caughtEx2), ($null))==1); goto Block417; Block419: goto Block420, Block422; Block417: $Exep1 := $caughtEx2; return; Block420: assume ($neref(($caughtEx3), ($null))==1); goto Block421; Block422: assume ($eqref(($caughtEx3), ($null))==1); goto Block423; Block421: $Exep0 := $caughtEx3; return; Block423: // @line: 782 __ret := $r1265; return; } // @line: 616 // procedure javaUtilEx.AbstractList$javaUtilEx.SubList$access$100$2566($param_0 : ref) returns (__ret : ref) { var r0419 : ref; var $r1420 : ref; Block678: r0419 := $param_0; assert ($neref((r0419), ($null))==1); // @line: 617 $r1420 := $HeapVar[r0419, javaUtilEx.AbstractList$javaUtilEx.SubList$l297]; // @line: 617 __ret := $r1420; return; } // @line: 711 // procedure void$javaUtilEx.LinkedList$ListItr$add$2686(__this : ref, $param_0 : ref) returns ($Exep0 : ref) modifies $HeapVar; requires ($neref((__this), ($null))==1); { var $r5873 : ref; var $r3870 : ref; var $i0875 : int; var r0868 : ref; var $i2877 : int; var $r2869 : ref; var $i1876 : int; var r1871 : ref; var $r4872 : ref; var $i3878 : int; //temp local variables var $caughtEx1 : ref; var $freshlocal2 : ref; // @line: 711 Block1257: $caughtEx1 := $null; $Exep0 := $null; goto Block1258; Block1258: r0868 := __this; r1871 := $param_0; assert ($neref((r0868), ($null))==1); // @line: 712 call $caughtEx1 := void$javaUtilEx.LinkedList$ListItr$checkForComodification$2687((r0868)); goto Block1259, Block1261; Block1259: assume ($neref(($caughtEx1), ($null))==1); goto Block1260; Block1261: assume ($eqref(($caughtEx1), ($null))==1); goto Block1262; Block1260: $Exep0 := $caughtEx1; return; Block1262: assert ($neref((r0868), ($null))==1); // @line: 713 $r2869 := $HeapVar[r0868, javaUtilEx.LinkedList$javaUtilEx.LinkedList$ListItr$this$0305]; // @line: 713 call $r3870 := javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$access$000$2669(($r2869)); assert ($neref((r0868), ($null))==1); // @line: 713 $HeapVar[r0868, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$ListItr$lastReturned303] := $r3870; assert ($neref((r0868), ($null))==1); // @line: 714 $r5873 := $HeapVar[r0868, javaUtilEx.LinkedList$javaUtilEx.LinkedList$ListItr$this$0305]; assert ($neref((r0868), ($null))==1); // @line: 714 $r4872 := $HeapVar[r0868, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$ListItr$next304]; // @line: 714 call $freshlocal2 := javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$access$300$2672(($r5873), (r1871), ($r4872)); assert ($neref((r0868), ($null))==1); // @line: 715 $i0875 := $HeapVar[r0868, int$javaUtilEx.LinkedList$ListItr$nextIndex0]; // @line: 715 $i1876 := $addint(($i0875), (1)); assert ($neref((r0868), ($null))==1); // @line: 715 $HeapVar[r0868, int$javaUtilEx.LinkedList$ListItr$nextIndex0] := $i1876; assert ($neref((r0868), ($null))==1); // @line: 716 $i2877 := $HeapVar[r0868, int$javaUtilEx.LinkedList$ListItr$expectedModCount0]; // @line: 716 $i3878 := $addint(($i2877), (1)); assert ($neref((r0868), ($null))==1); // @line: 716 $HeapVar[r0868, int$javaUtilEx.LinkedList$ListItr$expectedModCount0] := $i3878; return; } // procedure is generated by joogie. function {:inline true} $cmpint(x : int, y : int) returns (__ret : int) { if (x < y) then 1 else if (x == y) then 0 else -1 } // @line: 746 // procedure java.lang.Object$javaUtilEx.LinkedList$remove$2666(__this : ref, $param_0 : ref) returns (__ret : ref, $Exep0 : ref) modifies $HeapVar; requires ($neref((__this), ($null))==1); { var $i1744 : int; var $i0743 : int; var $r3736 : ref; var $r4738 : ref; var $r5739 : ref; var r0735 : ref; var $r8747 : ref; var $r6740 : ref; var $i3746 : int; var r2737 : ref; var $i2745 : int; var $r7741 : ref; var r1734 : ref; //temp local variables // @line: 746 Block757: $Exep0 := $null; goto Block1117; Block1117: r0735 := __this; r1734 := $param_0; assert ($neref((r0735), ($null))==1); // @line: 747 $r3736 := $HeapVar[r0735, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$header298]; goto Block1118; // @line: 747 Block1118: goto Block1119, Block1121; // @line: 747 Block1119: assume ($neref((r1734), ($r3736))==1); goto Block1120; // @line: 747 Block1121: // @line: 747 assume ($negInt(($neref((r1734), ($r3736))))==1); // @line: 748 $r8747 := $newvariable((1122)); assume ($neref(($newvariable((1122))), ($null))==1); assert ($neref(($r8747), ($null))==1); // @line: 748 call void$javaUtilEx.NoSuchElementException$$la$init$ra$$2572(($r8747)); goto Block1123; // @line: 750 Block1120: assert ($neref((r1734), ($null))==1); // @line: 750 r2737 := $HeapVar[r1734, java.lang.Object$javaUtilEx.LinkedList$Entry$element300]; goto Block1124; // @line: 747 Block1123: $Exep0 := $r8747; return; // @line: 751 Block1124: assert ($neref((r1734), ($null))==1); // @line: 751 $r5739 := $HeapVar[r1734, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$previous302]; assert ($neref((r1734), ($null))==1); // @line: 751 $r4738 := $HeapVar[r1734, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$next301]; assert ($neref(($r5739), ($null))==1); // @line: 751 $HeapVar[$r5739, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$next301] := $r4738; assert ($neref((r1734), ($null))==1); // @line: 752 $r7741 := $HeapVar[r1734, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$next301]; assert ($neref((r1734), ($null))==1); // @line: 752 $r6740 := $HeapVar[r1734, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$previous302]; assert ($neref(($r7741), ($null))==1); // @line: 752 $HeapVar[$r7741, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$previous302] := $r6740; assert ($neref((r1734), ($null))==1); // @line: 753 $HeapVar[r1734, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$previous302] := $null; assert ($neref((r1734), ($null))==1); // @line: 753 $HeapVar[r1734, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$next301] := $null; assert ($neref((r1734), ($null))==1); // @line: 754 $HeapVar[r1734, java.lang.Object$javaUtilEx.LinkedList$Entry$element300] := $null; assert ($neref((r0735), ($null))==1); // @line: 755 $i0743 := $HeapVar[r0735, int$javaUtilEx.LinkedList$size0]; // @line: 755 $i1744 := $subint(($i0743), (1)); assert ($neref((r0735), ($null))==1); // @line: 755 $HeapVar[r0735, int$javaUtilEx.LinkedList$size0] := $i1744; assert ($neref((r0735), ($null))==1); // @line: 756 $i2745 := $HeapVar[r0735, int$javaUtilEx.AbstractList$modCount0]; // @line: 756 $i3746 := $addint(($i2745), (1)); assert ($neref((r0735), ($null))==1); // @line: 756 $HeapVar[r0735, int$javaUtilEx.AbstractList$modCount0] := $i3746; // @line: 757 __ret := r2737; return; } // ()> procedure void$java.lang.RuntimeException$$la$init$ra$$760(__this : ref); // (java.lang.Throwable)> procedure void$java.lang.RuntimeException$$la$init$ra$$763(__this : ref, $param_0 : ref); // procedure is generated by joogie. function {:inline true} $subint(x : int, y : int) returns (__ret : int) { (x - y) } // procedure is generated by joogie. function {:inline true} $neref(x : ref, y : ref) returns (__ret : int) { if (x != y) then 1 else 0 } // @line: 75 // ()> procedure void$javaUtilEx.AbstractList$$la$init$ra$$2483(__this : ref) modifies $HeapVar; requires ($neref((__this), ($null))==1); { var r0104 : ref; Block138: r0104 := __this; assert ($neref((r0104), ($null))==1); // @line: 76 call void$javaUtilEx.AbstractCollection$$la$init$ra$$2228((r0104)); assert ($neref((r0104), ($null))==1); // @line: 605 $HeapVar[r0104, int$javaUtilEx.AbstractList$modCount0] := 0; return; } // @line: 621 // (javaUtilEx.AbstractList,int,int)> procedure void$javaUtilEx.SubList$$la$init$ra$$2549(__this : ref, $param_0 : ref, $param_1 : int, $param_2 : int) returns ($Exep1 : ref, $Exep0 : ref) modifies $HeapVar; requires ($neref((__this), ($null))==1); { var i0315 : int; var $i4321 : int; var $i2318 : int; var $i3319 : int; var $r5324 : ref; var r0314 : ref; var $r4323 : ref; var r1317 : ref; var i1316 : int; var $r3322 : ref; var $r2320 : ref; //temp local variables // @line: 621 Block243: $Exep1 := $null; $Exep0 := $null; goto Block486; Block486: r0314 := __this; r1317 := $param_0; i0315 := $param_1; i1316 := $param_2; assert ($neref((r0314), ($null))==1); // @line: 622 call void$javaUtilEx.AbstractList$$la$init$ra$$2483((r0314)); goto Block487; // @line: 623 Block487: goto Block490, Block488; // @line: 623 Block490: // @line: 623 assume ($negInt(($geint((i0315), (0))))==1); // @line: 624 $r5324 := $newvariable((491)); assume ($neref(($newvariable((491))), ($null))==1); assert ($neref(($r5324), ($null))==1); // @line: 624 call void$java.lang.IndexOutOfBoundsException$$la$init$ra$$2075(($r5324)); goto Block492; // @line: 623 Block488: assume ($geint((i0315), (0))==1); goto Block489; // @line: 623 Block492: $Exep0 := $r5324; return; // @line: 625 Block489: assert ($neref((r1317), ($null))==1); // @line: 625 call $i2318 := int$javaUtilEx.AbstractCollection$size$2230((r1317)); goto Block493; // @line: 625 Block493: goto Block496, Block494; // @line: 625 Block496: // @line: 625 assume ($negInt(($leint((i1316), ($i2318))))==1); // @line: 626 $r4323 := $newvariable((497)); assume ($neref(($newvariable((497))), ($null))==1); assert ($neref(($r4323), ($null))==1); // @line: 626 call void$java.lang.IndexOutOfBoundsException$$la$init$ra$$2075(($r4323)); goto Block498; // @line: 625 Block494: assume ($leint((i1316), ($i2318))==1); goto Block495; // @line: 625 Block498: $Exep0 := $r4323; return; // @line: 627 Block495: goto Block501, Block499; // @line: 627 Block501: // @line: 627 assume ($negInt(($leint((i0315), (i1316))))==1); goto Block502; // @line: 627 Block499: assume ($leint((i0315), (i1316))==1); goto Block500; // @line: 628 Block502: // @line: 628 $r3322 := $newvariable((503)); assume ($neref(($newvariable((503))), ($null))==1); assert ($neref(($r3322), ($null))==1); // @line: 628 call void$javaUtilEx.IllegalArgumentException$$la$init$ra$$2622(($r3322)); goto Block504; // @line: 629 Block500: assert ($neref((r0314), ($null))==1); // @line: 629 $HeapVar[r0314, javaUtilEx.AbstractList$javaUtilEx.SubList$l297] := r1317; goto Block505; // @line: 628 Block504: $Exep1 := $r3322; return; // @line: 630 Block505: assert ($neref((r0314), ($null))==1); // @line: 630 $HeapVar[r0314, int$javaUtilEx.SubList$offset0] := i0315; // @line: 631 $i3319 := $subint((i1316), (i0315)); assert ($neref((r0314), ($null))==1); // @line: 631 $HeapVar[r0314, int$javaUtilEx.SubList$size0] := $i3319; assert ($neref((r0314), ($null))==1); // @line: 632 $r2320 := $HeapVar[r0314, javaUtilEx.AbstractList$javaUtilEx.SubList$l297]; assert ($neref(($r2320), ($null))==1); // @line: 632 $i4321 := $HeapVar[$r2320, int$javaUtilEx.AbstractList$modCount0]; assert ($neref((r0314), ($null))==1); // @line: 632 $HeapVar[r0314, int$javaUtilEx.AbstractList$modCount0] := $i4321; return; } // procedure is generated by joogie. function {:inline true} $modint($param00 : int, $param11 : int) returns (__ret : int); // @line: 503 // procedure java.lang.Object$javaUtilEx.LinkedList$peekLast$2657(__this : ref) returns (__ret : ref, $Exep0 : ref) requires ($neref((__this), ($null))==1); { var $i0690 : int; var r0689 : ref; var $r1691 : ref; //temp local variables var $caughtEx1 : ref; // @line: 503 Block1027: $caughtEx1 := $null; $Exep0 := $null; goto Block1028; Block1028: r0689 := __this; assert ($neref((r0689), ($null))==1); // @line: 504 $i0690 := $HeapVar[r0689, int$javaUtilEx.LinkedList$size0]; goto Block1029; // @line: 504 Block1029: goto Block1030, Block1032; // @line: 504 Block1030: assume ($neint(($i0690), (0))==1); goto Block1031; // @line: 504 Block1032: // @line: 504 assume ($negInt(($neint(($i0690), (0))))==1); // @line: 505 __ret := $null; return; // @line: 506 Block1031: assert ($neref((r0689), ($null))==1); // @line: 506 call $r1691, $caughtEx1 := java.lang.Object$javaUtilEx.LinkedList$getLast$2632((r0689)); goto Block1033, Block1035; // @line: 506 Block1033: assume ($neref(($caughtEx1), ($null))==1); goto Block1034; // @line: 506 Block1035: assume ($eqref(($caughtEx1), ($null))==1); goto Block1036; // @line: 506 Block1034: $Exep0 := $caughtEx1; return; // @line: 506 Block1036: goto Block1037; // @line: 506 Block1037: // @line: 506 __ret := $r1691; return; } // @line: 704 // procedure boolean$javaUtilEx.SubList$1$hasNext$2694(__this : ref) returns (__ret : int) requires ($neref((__this), ($null))==1); { var r0911 : ref; var $i1914 : int; var $i0912 : int; var $r1913 : ref; var $z0916 : int; Block1307: r0911 := __this; assert ($neref((r0911), ($null))==1); // @line: 705 call $i0912 := int$javaUtilEx.SubList$1$nextIndex$2698((r0911)); assert ($neref((r0911), ($null))==1); // @line: 705 $r1913 := $HeapVar[r0911, javaUtilEx.SubList$javaUtilEx.SubList$1$this$0309]; // @line: 705 call $i1914 := int$javaUtilEx.SubList$access$200$2567(($r1913)); goto Block1308; // @line: 705 Block1308: goto Block1309, Block1311; // @line: 705 Block1309: assume ($geint(($i0912), ($i1914))==1); goto Block1310; // @line: 705 Block1311: // @line: 705 assume ($negInt(($geint(($i0912), ($i1914))))==1); // @line: 705 $z0916 := 1; goto Block1312; // @line: 705 Block1310: // @line: 705 $z0916 := 0; goto Block1312; // @line: 705 Block1312: // @line: 705 __ret := $z0916; return; } // procedure java.lang.Object$javaUtilEx.ListIterator$next$2526(__this : ref) returns (__ret : ref); // @line: 2 // ()> procedure void$javaUtilEx.juLinkedListCreateRemoveLastOccurrence$$la$init$ra$$2626(__this : ref) requires ($neref((__this), ($null))==1); { var r0516 : ref; Block753: r0516 := __this; assert ($neref((r0516), ($null))==1); // @line: 3 call void$java.lang.Object$$la$init$ra$$28((r0516)); return; } // @line: 85 // procedure boolean$javaUtilEx.AbstractCollection$isEmpty$2231(__this : ref) returns (__ret : int) requires ($neref((__this), ($null))==1); { var r02 : ref; var $i03 : int; var $z05 : int; Block17: r02 := __this; assert ($neref((r02), ($null))==1); // @line: 86 call $i03 := int$javaUtilEx.AbstractCollection$size$2230((r02)); goto Block18; // @line: 86 Block18: goto Block19, Block21; // @line: 86 Block19: assume ($neint(($i03), (0))==1); goto Block20; // @line: 86 Block21: // @line: 86 assume ($negInt(($neint(($i03), (0))))==1); // @line: 86 $z05 := 1; goto Block22; // @line: 86 Block20: // @line: 86 $z05 := 0; goto Block22; // @line: 86 Block22: // @line: 86 __ret := $z05; return; } // @line: 318 // procedure java.lang.Object$javaUtilEx.LinkedList$remove$2645(__this : ref, $param_0 : int) returns (__ret : ref, $Exep0 : ref, $Exep1 : ref) requires ($neref((__this), ($null))==1); { var i0627 : int; var $r1628 : ref; var r0626 : ref; var $r2629 : ref; //temp local variables var $caughtEx2 : ref; var $caughtEx3 : ref; // @line: 318 Block893: $caughtEx3 := $null; $caughtEx2 := $null; $Exep1 := $null; $Exep0 := $null; goto Block894; Block894: r0626 := __this; i0627 := $param_0; assert ($neref((r0626), ($null))==1); // @line: 319 call $r1628, $caughtEx2 := javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$entry$2646((r0626), (i0627)); goto Block895, Block897; Block895: assume ($neref(($caughtEx2), ($null))==1); goto Block896; Block897: assume ($eqref(($caughtEx2), ($null))==1); goto Block898; Block896: $Exep0 := $caughtEx2; return; Block898: assert ($neref((r0626), ($null))==1); // @line: 319 call $r2629, $caughtEx3 := java.lang.Object$javaUtilEx.LinkedList$remove$2666((r0626), ($r1628)); goto Block901, Block899; Block901: assume ($eqref(($caughtEx3), ($null))==1); goto Block902; Block899: assume ($neref(($caughtEx3), ($null))==1); goto Block900; Block902: // @line: 319 __ret := $r2629; return; Block900: $Exep1 := $caughtEx3; return; } // procedure is generated by joogie. function {:inline true} $eqrealarray($param00 : [int]realVar, $param11 : [int]realVar) returns (__ret : int); // procedure is generated by joogie. function {:inline true} $shrint($param00 : int, $param11 : int) returns (__ret : int); // procedure is generated by joogie. function {:inline true} $ushrint($param00 : int, $param11 : int) returns (__ret : int); // procedure int$java.lang.String$length$59(__this : ref) returns (__ret : int); // @line: 36 // procedure boolean$javaUtilEx.Content$equals$2588(__this : ref, $param_0 : ref) returns (__ret : int) requires ($neref((__this), ($null))==1); { var $z0501 : int; var $i1505 : int; var $i0504 : int; var r1500 : ref; var $z1507 : int; var r0502 : ref; var $r2503 : ref; Block739: r0502 := __this; r1500 := $param_0; // @line: 37 $z0501 := $instanceof((r1500), (javaUtilEx.Content)); goto Block740; // @line: 37 Block740: goto Block741, Block743; // @line: 37 Block741: assume ($eqint(($z0501), (0))==1); goto Block742; // @line: 37 Block743: // @line: 37 assume ($negInt(($eqint(($z0501), (0))))==1); assert ($neref((r0502), ($null))==1); // @line: 38 $i1505 := $HeapVar[r0502, int$javaUtilEx.Content$val0]; // @line: 38 $r2503 := r1500; assert ($neref(($r2503), ($null))==1); // @line: 38 $i0504 := $HeapVar[$r2503, int$javaUtilEx.Content$val0]; goto Block744; // @line: 40 Block742: // @line: 40 __ret := 0; return; // @line: 38 Block744: goto Block745, Block747; // @line: 38 Block745: assume ($neint(($i1505), ($i0504))==1); goto Block746; // @line: 38 Block747: // @line: 38 assume ($negInt(($neint(($i1505), ($i0504))))==1); // @line: 38 $z1507 := 1; goto Block748; // @line: 38 Block746: // @line: 38 $z1507 := 0; goto Block748; // @line: 38 Block748: // @line: 38 __ret := $z1507; return; } // @line: 428 // procedure java.lang.Object$javaUtilEx.LinkedList$poll$2651(__this : ref) returns (__ret : ref, $Exep0 : ref) requires ($neref((__this), ($null))==1); { var $i0675 : int; var $r1676 : ref; var r0674 : ref; //temp local variables var $caughtEx1 : ref; // @line: 428 Block996: $caughtEx1 := $null; $Exep0 := $null; goto Block997; Block997: r0674 := __this; assert ($neref((r0674), ($null))==1); // @line: 429 $i0675 := $HeapVar[r0674, int$javaUtilEx.LinkedList$size0]; goto Block998; // @line: 429 Block998: goto Block999, Block1001; // @line: 429 Block999: assume ($neint(($i0675), (0))==1); goto Block1000; // @line: 429 Block1001: // @line: 429 assume ($negInt(($neint(($i0675), (0))))==1); // @line: 430 __ret := $null; return; // @line: 431 Block1000: assert ($neref((r0674), ($null))==1); // @line: 431 call $r1676, $caughtEx1 := java.lang.Object$javaUtilEx.LinkedList$removeFirst$2633((r0674)); goto Block1002, Block1004; // @line: 431 Block1002: assume ($neref(($caughtEx1), ($null))==1); goto Block1003; // @line: 431 Block1004: assume ($eqref(($caughtEx1), ($null))==1); goto Block1005; // @line: 431 Block1003: $Exep0 := $caughtEx1; return; // @line: 431 Block1005: goto Block1006; // @line: 431 Block1006: // @line: 431 __ret := $r1676; return; } // @line: 513 // procedure boolean$javaUtilEx.AbstractList$equals$2497(__this : ref, $param_0 : ref) returns (__ret : int, $Exep0 : ref) requires ($neref((__this), ($null))==1); { var $z5189 : int; var r0173 : ref; var r2176 : ref; var $z4184 : int; var $z0174 : int; var $z6190 : int; var $z2181 : int; var $r6177 : ref; var r4186 : ref; var r5188 : ref; var r1172 : ref; var r3179 : ref; var $z1180 : int; var $z3182 : int; //temp local variables var $caughtEx1 : ref; // @line: 513 Block271: $caughtEx1 := $null; $Exep0 := $null; goto Block272; Block272: r0173 := __this; r1172 := $param_0; goto Block273; // @line: 514 Block273: goto Block276, Block274; // @line: 514 Block276: // @line: 514 assume ($negInt(($neref((r1172), (r0173))))==1); // @line: 515 __ret := 1; return; // @line: 514 Block274: assume ($neref((r1172), (r0173))==1); goto Block275; // @line: 516 Block275: // @line: 516 $z0174 := $instanceof((r1172), (javaUtilEx.List)); goto Block277; // @line: 516 Block277: goto Block280, Block278; // @line: 516 Block280: // @line: 516 assume ($negInt(($neint(($z0174), (0))))==1); // @line: 517 __ret := 0; return; // @line: 516 Block278: assume ($neint(($z0174), (0))==1); goto Block279; // @line: 519 Block279: assert ($neref((r0173), ($null))==1); // @line: 519 call r2176, $caughtEx1 := javaUtilEx.ListIterator$javaUtilEx.AbstractList$listIterator$2494((r0173)); goto Block281, Block283; // @line: 519 Block281: assume ($neref(($caughtEx1), ($null))==1); goto Block282; // @line: 519 Block283: assume ($eqref(($caughtEx1), ($null))==1); goto Block284; // @line: 519 Block282: $Exep0 := $caughtEx1; return; // @line: 519 Block284: goto Block285; // @line: 520 Block285: // @line: 520 $r6177 := r1172; assert ($neref(($r6177), ($null))==1); // @line: 520 call r3179 := javaUtilEx.ListIterator$javaUtilEx.List$listIterator$2522(($r6177)); goto Block286; // @line: 521 Block286: assert ($neref((r2176), ($null))==1); // @line: 521 call $z1180 := boolean$javaUtilEx.ListIterator$hasNext$2525((r2176)); goto Block287; // @line: 521 Block287: goto Block290, Block288; // @line: 521 Block290: // @line: 521 assume ($negInt(($eqint(($z1180), (0))))==1); assert ($neref((r3179), ($null))==1); // @line: 527 call $z4184 := boolean$javaUtilEx.ListIterator$hasNext$2525((r3179)); goto Block291; // @line: 521 Block288: assume ($eqint(($z1180), (0))==1); goto Block289; // @line: 527 Block291: goto Block292, Block293; // @line: 527 Block289: assert ($neref((r2176), ($null))==1); // @line: 527 call $z2181 := boolean$javaUtilEx.ListIterator$hasNext$2525((r2176)); goto Block306; // @line: 527 Block292: assume ($eqint(($z4184), (0))==1); goto Block289; // @line: 527 Block293: // @line: 527 assume ($negInt(($eqint(($z4184), (0))))==1); assert ($neref((r2176), ($null))==1); // @line: 522 call r4186 := java.lang.Object$javaUtilEx.ListIterator$next$2526((r2176)); assert ($neref((r3179), ($null))==1); // @line: 523 call r5188 := java.lang.Object$javaUtilEx.ListIterator$next$2526((r3179)); goto Block294; // @line: 527 Block306: goto Block309, Block307; // @line: 524 Block294: goto Block295, Block297; // @line: 527 Block309: // @line: 527 assume ($negInt(($neint(($z2181), (0))))==1); assert ($neref((r3179), ($null))==1); // @line: 527 call $z3182 := boolean$javaUtilEx.ListIterator$hasNext$2525((r3179)); goto Block310; // @line: 527 Block307: assume ($neint(($z2181), (0))==1); goto Block308; // @line: 524 Block295: assume ($neref((r4186), ($null))==1); goto Block296; // @line: 524 Block297: // @line: 524 assume ($negInt(($neref((r4186), ($null))))==1); goto Block298; // @line: 527 Block310: goto Block311, Block312; // @line: 527 Block308: // @line: 527 $z6190 := 0; goto Block313; // @line: 524 Block296: assert ($neref((r4186), ($null))==1); // @line: 524 call $z5189 := boolean$java.lang.Object$equals$32((r4186), (r5188)); goto Block303; // @line: 525 Block298: goto Block301, Block299; // @line: 527 Block311: assume ($neint(($z3182), (0))==1); goto Block308; // @line: 527 Block312: // @line: 527 assume ($negInt(($neint(($z3182), (0))))==1); // @line: 527 $z6190 := 1; goto Block313; // @line: 527 Block313: // @line: 527 __ret := $z6190; return; // @line: 524 Block303: goto Block305, Block304; // @line: 525 Block301: // @line: 525 assume ($negInt(($neref((r5188), ($null))))==1); goto Block302; // @line: 525 Block299: assume ($neref((r5188), ($null))==1); goto Block300; // @line: 524 Block305: // @line: 524 assume ($negInt(($neint(($z5189), (0))))==1); goto Block300; // @line: 524 Block304: assume ($neint(($z5189), (0))==1); goto Block302; // @line: 526 Block302: goto Block286; // @line: 525 Block300: // @line: 525 __ret := 0; return; } // @line: 421 // procedure void$javaUtilEx.AbstractList$ListItr$set$2547(__this : ref, $param_0 : ref) returns ($Exep1 : ref, $Exep0 : ref, $Exep2 : ref) modifies $HeapVar; requires ($neref((__this), ($null))==1); { var $r6299 : ref; var $i1294 : int; var $r3295 : ref; var $i2298 : int; var $i0292 : int; var $r5297 : ref; var $r7300 : ref; var $r8302 : ref; var r1293 : ref; var r0291 : ref; //temp local variables var $caughtEx3 : ref; var $caughtEx4 : ref; var $freshlocal5 : ref; var $caughtEx6 : ref; // @line: 421 Block448: $caughtEx6 := $null; $caughtEx4 := $null; $caughtEx3 := $null; $Exep2 := $null; $Exep1 := $null; $Exep0 := $null; goto Block449; Block449: r0291 := __this; r1293 := $param_0; assert ($neref((r0291), ($null))==1); // @line: 422 $i0292 := $HeapVar[r0291, int$javaUtilEx.AbstractList$Itr$lastRet0]; goto Block450; // @line: 422 Block450: goto Block451, Block453; // @line: 422 Block451: assume ($geint(($i0292), (0))==1); goto Block452; // @line: 422 Block453: // @line: 422 assume ($negInt(($geint(($i0292), (0))))==1); // @line: 423 $r6299 := $newvariable((454)); assume ($neref(($newvariable((454))), ($null))==1); assert ($neref(($r6299), ($null))==1); // @line: 423 call void$javaUtilEx.IllegalStateException$$la$init$ra$$2574(($r6299)); goto Block455; // @line: 424 Block452: assert ($neref((r0291), ($null))==1); // @line: 424 call $caughtEx3 := void$javaUtilEx.AbstractList$Itr$checkForComodification$2538((r0291)); goto Block458, Block456; // @line: 422 Block455: $Exep0 := $r6299; return; // @line: 424 Block458: assume ($eqref(($caughtEx3), ($null))==1); goto Block459; // @line: 424 Block456: assume ($neref(($caughtEx3), ($null))==1); goto Block457; // @line: 424 Block459: goto Block460; // @line: 424 Block457: $Exep1 := $caughtEx3; return; // @line: 427 Block460: assert ($neref((r0291), ($null))==1); // @line: 427 $r3295 := $HeapVar[r0291, javaUtilEx.AbstractList$javaUtilEx.AbstractList$ListItr$this$0296]; assert ($neref((r0291), ($null))==1); // @line: 427 $i1294 := $HeapVar[r0291, int$javaUtilEx.AbstractList$Itr$lastRet0]; assert ($neref(($r3295), ($null))==1); // @line: 427 call $freshlocal5, $caughtEx4 := java.lang.Object$javaUtilEx.AbstractList$set$2486(($r3295), ($i1294), (r1293)); goto Block461, Block463; // @line: 427 Block461: assume ($neref(($caughtEx4), ($null))==1); goto Block462; // @line: 427 Block463: assume ($eqref(($caughtEx4), ($null))==1); goto Block464; // @line: 427 Block462: $Exep2 := $caughtEx4; return; // @line: 427 Block464: assert ($neref((r0291), ($null))==1); // @line: 428 $r5297 := $HeapVar[r0291, javaUtilEx.AbstractList$javaUtilEx.AbstractList$ListItr$this$0296]; assert ($neref(($r5297), ($null))==1); // @line: 428 $i2298 := $HeapVar[$r5297, int$javaUtilEx.AbstractList$modCount0]; assert ($neref((r0291), ($null))==1); // @line: 428 $HeapVar[r0291, int$javaUtilEx.AbstractList$Itr$expectedModCount0] := $i2298; goto Block465; // @line: 431 Block465: goto Block466; // @line: 432 Block466: return; } // procedure is generated by joogie. function {:inline true} $gtint(x : int, y : int) returns (__ret : int) { if (x > y) then 1 else 0 } // @line: 145 // procedure void$javaUtilEx.AbstractSequentialList$add$2581(__this : ref, $param_0 : int, $param_1 : ref) returns ($Exep0 : ref) requires ($neref((__this), ($null))==1); { var $r5468 : ref; var $r3464 : ref; var i0463 : int; var $r4466 : ref; var r0462 : ref; var r1465 : ref; //temp local variables var $caughtEx1 : ref; // @line: 145 Block705: $caughtEx1 := $null; $Exep0 := $null; goto Block706; Block706: r0462 := __this; i0463 := $param_0; r1465 := $param_1; goto Block707; // @line: 146 Block707: assert ($neref((r0462), ($null))==1); // @line: 146 call $r3464 := javaUtilEx.ListIterator$javaUtilEx.AbstractSequentialList$listIterator$2585((r0462), (i0463)); assert ($neref(($r3464), ($null))==1); // @line: 146 call void$javaUtilEx.ListIterator$add$2533(($r3464), (r1465)); goto Block708; // @line: 149 Block708: goto Block709; // @line: 150 Block709: return; } // @line: 288 // procedure javaUtilEx.Iterator$javaUtilEx.AbstractList$iterator$2493(__this : ref) returns (__ret : ref) requires ($neref((__this), ($null))==1); { var r0157 : ref; var $r1156 : ref; Block230: r0157 := __this; // @line: 289 $r1156 := $newvariable((231)); assume ($neref(($newvariable((231))), ($null))==1); assert ($neref(($r1156), ($null))==1); // @line: 289 call void$javaUtilEx.AbstractList$Itr$$la$init$ra$$2539(($r1156), (r0157), ($null)); // @line: 289 __ret := $r1156; return; } // @line: 734 // procedure void$javaUtilEx.SubList$1$remove$2700(__this : ref) modifies $HeapVar; requires ($neref((__this), ($null))==1); { var $i0948 : int; var $r5949 : ref; var r0943 : ref; var $r1944 : ref; var $r4947 : ref; var $r3946 : ref; var $r2945 : ref; //temp local variables var $freshlocal0 : int; Block1339: r0943 := __this; assert ($neref((r0943), ($null))==1); // @line: 735 $r1944 := $HeapVar[r0943, javaUtilEx.ListIterator$javaUtilEx.SubList$1$i308]; assert ($neref(($r1944), ($null))==1); // @line: 735 call void$javaUtilEx.ListIterator$remove$2531(($r1944)); assert ($neref((r0943), ($null))==1); // @line: 736 $r3946 := $HeapVar[r0943, javaUtilEx.SubList$javaUtilEx.SubList$1$this$0309]; assert ($neref((r0943), ($null))==1); // @line: 736 $r2945 := $HeapVar[r0943, javaUtilEx.SubList$javaUtilEx.SubList$1$this$0309]; // @line: 736 call $r4947 := javaUtilEx.AbstractList$javaUtilEx.SubList$access$100$2566(($r2945)); assert ($neref(($r4947), ($null))==1); // @line: 736 $i0948 := $HeapVar[$r4947, int$javaUtilEx.AbstractList$modCount0]; assert ($neref(($r3946), ($null))==1); // @line: 736 $HeapVar[$r3946, int$javaUtilEx.AbstractList$modCount0] := $i0948; assert ($neref((r0943), ($null))==1); // @line: 737 $r5949 := $HeapVar[r0943, javaUtilEx.SubList$javaUtilEx.SubList$1$this$0309]; // @line: 737 call $freshlocal0 := int$javaUtilEx.SubList$access$210$2568(($r5949)); return; } // procedure is generated by joogie. function {:inline true} $eqreal(x : realVar, y : realVar) returns (__ret : int) { if (x == y) then 1 else 0 } // @line: 71 // (java.lang.String,java.lang.Throwable)> procedure void$javaUtilEx.UnsupportedOperationException$$la$init$ra$$2259(__this : ref, $param_0 : ref, $param_1 : ref) requires ($neref((__this), ($null))==1); { var r1100 : ref; var r2101 : ref; var r099 : ref; Block136: r099 := __this; r1100 := $param_0; r2101 := $param_1; assert ($neref((r099), ($null))==1); // @line: 72 call void$java.lang.RuntimeException$$la$init$ra$$762((r099), (r1100), (r2101)); return; } // @line: 770 // procedure boolean$javaUtilEx.LinkedList$DescendingIterator$hasNext$2689(__this : ref) returns (__ret : int) requires ($neref((__this), ($null))==1); { var $z0892 : int; var r0890 : ref; var $r1891 : ref; Block1276: r0890 := __this; assert ($neref((r0890), ($null))==1); // @line: 771 $r1891 := $HeapVar[r0890, javaUtilEx.LinkedList$ListItr$javaUtilEx.LinkedList$DescendingIterator$itr306]; assert ($neref(($r1891), ($null))==1); // @line: 771 call $z0892 := boolean$javaUtilEx.LinkedList$ListItr$hasPrevious$2680(($r1891)); // @line: 771 __ret := $z0892; return; } // @line: 700 // (javaUtilEx.SubList,int)> procedure void$javaUtilEx.SubList$1$$la$init$ra$$2693(__this : ref, $param_0 : ref, $param_1 : int) returns ($Exep0 : ref) modifies $HeapVar; requires ($neref((__this), ($null))==1); { var $r2904 : ref; var $i3909 : int; var $r5910 : ref; var $i1907 : int; var $r3905 : ref; var r1902 : ref; var r0901 : ref; var $i2908 : int; var i0903 : int; var $r4906 : ref; //temp local variables var $caughtEx1 : ref; // @line: 700 Block621: $caughtEx1 := $null; $Exep0 := $null; goto Block1302; Block1302: r0901 := __this; r1902 := $param_0; i0903 := $param_1; assert ($neref((r0901), ($null))==1); // @line: 701 $HeapVar[r0901, javaUtilEx.SubList$javaUtilEx.SubList$1$this$0309] := r1902; assert ($neref((r0901), ($null))==1); // @line: 701 $HeapVar[r0901, int$javaUtilEx.SubList$1$val$index0] := i0903; assert ($neref((r0901), ($null))==1); // @line: 701 call void$java.lang.Object$$la$init$ra$$28((r0901)); assert ($neref((r0901), ($null))==1); // @line: 702 $r2904 := $HeapVar[r0901, javaUtilEx.SubList$javaUtilEx.SubList$1$this$0309]; // @line: 702 call $r3905 := javaUtilEx.AbstractList$javaUtilEx.SubList$access$100$2566(($r2904)); assert ($neref((r0901), ($null))==1); // @line: 702 $i1907 := $HeapVar[r0901, int$javaUtilEx.SubList$1$val$index0]; assert ($neref((r0901), ($null))==1); // @line: 702 $r4906 := $HeapVar[r0901, javaUtilEx.SubList$javaUtilEx.SubList$1$this$0309]; // @line: 702 call $i2908 := int$javaUtilEx.SubList$access$000$2565(($r4906)); // @line: 702 $i3909 := $addint(($i1907), ($i2908)); assert ($neref(($r3905), ($null))==1); // @line: 702 call $r5910, $caughtEx1 := javaUtilEx.ListIterator$javaUtilEx.AbstractList$listIterator$2495(($r3905), ($i3909)); goto Block1303, Block1305; Block1303: assume ($neref(($caughtEx1), ($null))==1); goto Block1304; Block1305: assume ($eqref(($caughtEx1), ($null))==1); goto Block1306; Block1304: $Exep0 := $caughtEx1; return; Block1306: assert ($neref((r0901), ($null))==1); // @line: 702 $HeapVar[r0901, javaUtilEx.ListIterator$javaUtilEx.SubList$1$i308] := $r5910; return; } // @line: 737 // procedure javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$addBefore$2665(__this : ref, $param_0 : ref, $param_1 : ref) returns (__ret : ref) modifies $HeapVar; requires ($neref((__this), ($null))==1); { var r2724 : ref; var $r6727 : ref; var $i2732 : int; var r1723 : ref; var $i3733 : int; var $r5725 : ref; var r3726 : ref; var $r7728 : ref; var $i1731 : int; var $i0730 : int; var r0729 : ref; var $r4722 : ref; Block1115: r0729 := __this; r1723 := $param_0; r2724 := $param_1; // @line: 738 $r4722 := $newvariable((1116)); assume ($neref(($newvariable((1116))), ($null))==1); assert ($neref((r2724), ($null))==1); // @line: 738 $r5725 := $HeapVar[r2724, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$previous302]; assert ($neref(($r4722), ($null))==1); // @line: 738 call void$javaUtilEx.LinkedList$Entry$$la$init$ra$$2676(($r4722), (r1723), (r2724), ($r5725)); // @line: 738 r3726 := $r4722; assert ($neref((r3726), ($null))==1); // @line: 739 $r6727 := $HeapVar[r3726, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$previous302]; assert ($neref(($r6727), ($null))==1); // @line: 739 $HeapVar[$r6727, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$next301] := r3726; assert ($neref((r3726), ($null))==1); // @line: 740 $r7728 := $HeapVar[r3726, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$next301]; assert ($neref(($r7728), ($null))==1); // @line: 740 $HeapVar[$r7728, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$previous302] := r3726; assert ($neref((r0729), ($null))==1); // @line: 741 $i0730 := $HeapVar[r0729, int$javaUtilEx.LinkedList$size0]; // @line: 741 $i1731 := $addint(($i0730), (1)); assert ($neref((r0729), ($null))==1); // @line: 741 $HeapVar[r0729, int$javaUtilEx.LinkedList$size0] := $i1731; assert ($neref((r0729), ($null))==1); // @line: 742 $i2732 := $HeapVar[r0729, int$javaUtilEx.AbstractList$modCount0]; // @line: 742 $i3733 := $addint(($i2732), (1)); assert ($neref((r0729), ($null))==1); // @line: 742 $HeapVar[r0729, int$javaUtilEx.AbstractList$modCount0] := $i3733; // @line: 743 __ret := r3726; return; } // ()> procedure void$java.lang.Object$$la$init$ra$$28(__this : ref); // @line: 90 // procedure java.lang.Object$javaUtilEx.LinkedList$access$200$2671($param_0 : ref, $param_1 : ref) returns (__ret : ref, $Exep0 : ref) { var r0765 : ref; var $r2767 : ref; var r1766 : ref; //temp local variables var $caughtEx1 : ref; // @line: 90 Block1143: $caughtEx1 := $null; $Exep0 := $null; goto Block1144; Block1144: r0765 := $param_0; r1766 := $param_1; assert ($neref((r0765), ($null))==1); // @line: 91 call $r2767, $caughtEx1 := java.lang.Object$javaUtilEx.LinkedList$remove$2666((r0765), (r1766)); goto Block1145, Block1147; Block1145: assume ($neref(($caughtEx1), ($null))==1); goto Block1146; Block1147: assume ($eqref(($caughtEx1), ($null))==1); goto Block1148; Block1146: $Exep0 := $caughtEx1; return; Block1148: // @line: 91 __ret := $r2767; return; } // @line: 680 // procedure int$javaUtilEx.LinkedList$ListItr$nextIndex$2682(__this : ref) returns (__ret : int) requires ($neref((__this), ($null))==1); { var r0839 : ref; var $i0840 : int; Block1219: r0839 := __this; assert ($neref((r0839), ($null))==1); // @line: 681 $i0840 := $HeapVar[r0839, int$javaUtilEx.LinkedList$ListItr$nextIndex0]; // @line: 681 __ret := $i0840; return; } // procedure is generated by joogie. function {:inline true} $divint($param00 : int, $param11 : int) returns (__ret : int); // procedure is generated by joogie. function {:inline true} $leint(x : int, y : int) returns (__ret : int) { if (x <= y) then 1 else 0 } // @line: 708 // procedure java.lang.Object$javaUtilEx.SubList$1$next$2695(__this : ref) returns (__ret : ref, $Exep0 : ref) requires ($neref((__this), ($null))==1); { var r0917 : ref; var $r3921 : ref; var $z0918 : int; var $r2920 : ref; var $r1919 : ref; //temp local variables // @line: 708 Block1313: $Exep0 := $null; goto Block1314; Block1314: r0917 := __this; assert ($neref((r0917), ($null))==1); // @line: 709 call $z0918 := boolean$javaUtilEx.SubList$1$hasNext$2694((r0917)); goto Block1315; // @line: 709 Block1315: goto Block1316, Block1318; // @line: 709 Block1316: assume ($eqint(($z0918), (0))==1); goto Block1317; // @line: 709 Block1318: // @line: 709 assume ($negInt(($eqint(($z0918), (0))))==1); assert ($neref((r0917), ($null))==1); // @line: 710 $r2920 := $HeapVar[r0917, javaUtilEx.ListIterator$javaUtilEx.SubList$1$i308]; assert ($neref(($r2920), ($null))==1); // @line: 710 call $r3921 := java.lang.Object$javaUtilEx.ListIterator$next$2526(($r2920)); // @line: 710 __ret := $r3921; return; // @line: 712 Block1317: // @line: 712 $r1919 := $newvariable((1319)); assume ($neref(($newvariable((1319))), ($null))==1); goto Block1320; // @line: 712 Block1320: assert ($neref(($r1919), ($null))==1); // @line: 712 call void$javaUtilEx.NoSuchElementException$$la$init$ra$$2572(($r1919)); goto Block1321; // @line: 712 Block1321: $Exep0 := $r1919; return; } // @line: 253 // procedure void$javaUtilEx.LinkedList$clear$2641(__this : ref) modifies $HeapVar; requires ($neref((__this), ($null))==1); { var r1606 : ref; var r0597 : ref; var $i1605 : int; var $r4601 : ref; var $r6603 : ref; var $r2598 : ref; var $r3600 : ref; var $r5602 : ref; var $i0604 : int; var r7608 : ref; Block863: r0597 := __this; assert ($neref((r0597), ($null))==1); // @line: 254 $r2598 := $HeapVar[r0597, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$header298]; assert ($neref(($r2598), ($null))==1); // @line: 254 r7608 := $HeapVar[$r2598, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$next301]; goto Block864; // @line: 255 Block864: assert ($neref((r0597), ($null))==1); // @line: 255 $r3600 := $HeapVar[r0597, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$header298]; goto Block865; // @line: 255 Block865: goto Block866, Block868; // @line: 255 Block866: assume ($eqref((r7608), ($r3600))==1); goto Block867; // @line: 255 Block868: // @line: 255 assume ($negInt(($eqref((r7608), ($r3600))))==1); assert ($neref((r7608), ($null))==1); // @line: 256 r1606 := $HeapVar[r7608, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$next301]; assert ($neref((r7608), ($null))==1); // @line: 257 $HeapVar[r7608, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$previous302] := $null; assert ($neref((r7608), ($null))==1); // @line: 257 $HeapVar[r7608, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$next301] := $null; assert ($neref((r7608), ($null))==1); // @line: 258 $HeapVar[r7608, java.lang.Object$javaUtilEx.LinkedList$Entry$element300] := $null; // @line: 259 r7608 := r1606; goto Block864; // @line: 261 Block867: assert ($neref((r0597), ($null))==1); // @line: 261 $r6603 := $HeapVar[r0597, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$header298]; goto Block869; // @line: 261 Block869: assert ($neref((r0597), ($null))==1); // @line: 261 $r5602 := $HeapVar[r0597, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$header298]; assert ($neref((r0597), ($null))==1); // @line: 261 $r4601 := $HeapVar[r0597, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$header298]; assert ($neref(($r5602), ($null))==1); // @line: 261 $HeapVar[$r5602, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$previous302] := $r4601; assert ($neref(($r6603), ($null))==1); // @line: 261 $HeapVar[$r6603, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$next301] := $r4601; assert ($neref((r0597), ($null))==1); // @line: 262 $HeapVar[r0597, int$javaUtilEx.LinkedList$size0] := 0; assert ($neref((r0597), ($null))==1); // @line: 263 $i0604 := $HeapVar[r0597, int$javaUtilEx.AbstractList$modCount0]; // @line: 263 $i1605 := $addint(($i0604), (1)); assert ($neref((r0597), ($null))==1); // @line: 263 $HeapVar[r0597, int$javaUtilEx.AbstractList$modCount0] := $i1605; return; } // procedure is generated by joogie. function {:inline true} $shrreal($param00 : realVar, $param11 : realVar) returns (__ret : int); // procedure is generated by joogie. function {:inline true} $orint($param00 : int, $param11 : int) returns (__ret : int); // procedure is generated by joogie. function {:inline true} $reftorealarr($param00 : ref) returns (__ret : [int]realVar); // @line: 73 // ()> procedure void$javaUtilEx.ConcurrentModificationException$$la$init$ra$$2570(__this : ref) requires ($neref((__this), ($null))==1); { var r0429 : ref; Block682: r0429 := __this; assert ($neref((r0429), ($null))==1); // @line: 74 call void$java.lang.RuntimeException$$la$init$ra$$760((r0429)); return; } // @line: 52 // (java.lang.String)> procedure void$javaUtilEx.IllegalArgumentException$$la$init$ra$$2623(__this : ref, $param_0 : ref) requires ($neref((__this), ($null))==1); { var r0509 : ref; var r1510 : ref; Block750: r0509 := __this; r1510 := $param_0; assert ($neref((r0509), ($null))==1); // @line: 53 call void$java.lang.RuntimeException$$la$init$ra$$761((r0509), (r1510)); return; } // procedure is generated by joogie. function {:inline true} $orreal($param00 : realVar, $param11 : realVar) returns (__ret : int); // @line: 305 // procedure void$javaUtilEx.LinkedList$add$2644(__this : ref, $param_0 : int, $param_1 : ref) returns ($Exep0 : ref) requires ($neref((__this), ($null))==1); { var $r3625 : ref; var r0619 : ref; var $i1622 : int; var i0621 : int; var r1620 : ref; //temp local variables var $caughtEx1 : ref; var $freshlocal2 : ref; // @line: 305 Block881: $caughtEx1 := $null; $Exep0 := $null; goto Block882; Block882: r0619 := __this; i0621 := $param_0; r1620 := $param_1; assert ($neref((r0619), ($null))==1); // @line: 306 $i1622 := $HeapVar[r0619, int$javaUtilEx.LinkedList$size0]; goto Block883; // @line: 306 Block883: goto Block884, Block886; // @line: 306 Block884: assume ($neint((i0621), ($i1622))==1); goto Block885; // @line: 306 Block886: // @line: 306 assume ($negInt(($neint((i0621), ($i1622))))==1); assert ($neref((r0619), ($null))==1); // @line: 307 $r3625 := $HeapVar[r0619, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$header298]; goto Block887; // @line: 306 Block885: assert ($neref((r0619), ($null))==1); // @line: 306 call $r3625, $caughtEx1 := javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$entry$2646((r0619), (i0621)); goto Block890, Block888; // @line: 306 Block887: assert ($neref((r0619), ($null))==1); // @line: 306 call $freshlocal2 := javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$addBefore$2665((r0619), (r1620), ($r3625)); goto Block892; // @line: 306 Block890: assume ($eqref(($caughtEx1), ($null))==1); goto Block891; // @line: 306 Block888: assume ($neref(($caughtEx1), ($null))==1); goto Block889; // @line: 307 Block892: return; // @line: 306 Block891: goto Block887; // @line: 306 Block889: $Exep0 := $caughtEx1; return; } // @line: 641 // procedure java.lang.Object$javaUtilEx.SubList$get$2551(__this : ref, $param_0 : int) returns (__ret : ref, $Exep1 : ref, $Exep0 : ref) requires ($neref((__this), ($null))==1); { var $i2335 : int; var $r1336 : ref; var r0332 : ref; var i0333 : int; var $i1334 : int; var $r2337 : ref; //temp local variables var $caughtEx3 : ref; var $caughtEx2 : ref; // @line: 641 Block522: $caughtEx3 := $null; $caughtEx2 := $null; $Exep1 := $null; $Exep0 := $null; goto Block523; Block523: r0332 := __this; i0333 := $param_0; assert ($neref((r0332), ($null))==1); // @line: 642 call $caughtEx2 := void$javaUtilEx.SubList$rangeCheck$2561((r0332), (i0333)); goto Block524, Block526; Block524: assume ($neref(($caughtEx2), ($null))==1); goto Block525; Block526: assume ($eqref(($caughtEx2), ($null))==1); goto Block527; Block525: $Exep0 := $caughtEx2; return; Block527: assert ($neref((r0332), ($null))==1); // @line: 643 call $caughtEx3 := void$javaUtilEx.SubList$checkForComodification$2564((r0332)); goto Block528, Block530; Block528: assume ($neref(($caughtEx3), ($null))==1); goto Block529; Block530: assume ($eqref(($caughtEx3), ($null))==1); goto Block531; Block529: $Exep1 := $caughtEx3; return; Block531: assert ($neref((r0332), ($null))==1); // @line: 644 $r1336 := $HeapVar[r0332, javaUtilEx.AbstractList$javaUtilEx.SubList$l297]; assert ($neref((r0332), ($null))==1); // @line: 644 $i1334 := $HeapVar[r0332, int$javaUtilEx.SubList$offset0]; // @line: 644 $i2335 := $addint((i0333), ($i1334)); assert ($neref(($r1336), ($null))==1); // @line: 644 call $r2337 := java.lang.Object$javaUtilEx.AbstractList$get$2485(($r1336), ($i2335)); // @line: 644 __ret := $r2337; return; } // procedure is generated by joogie. function {:inline true} $ushrref($param00 : ref, $param11 : ref) returns (__ret : int); // @line: 688 // procedure void$javaUtilEx.LinkedList$ListItr$remove$2684(__this : ref) returns ($Exep0 : ref, $Exep1 : ref) modifies $HeapVar; requires ($neref((__this), ($null))==1); { var r0844 : ref; var $i3857 : int; var $i0852 : int; var $i1853 : int; var r1846 : ref; var $r10855 : ref; var $i2856 : int; var $r3845 : ref; var $r8851 : ref; var $r12860 : ref; var $r4847 : ref; var $r11858 : ref; var $r5848 : ref; var $r7850 : ref; var $r9854 : ref; //temp local variables var $caughtEx5 : ref; var $caughtEx2 : ref; var $caughtEx3 : ref; var $freshlocal4 : ref; // @line: 688 Block1221: $caughtEx5 := $null; $caughtEx3 := $null; $caughtEx2 := $null; $Exep1 := $null; $Exep0 := $null; goto Block1222; Block1222: r0844 := __this; assert ($neref((r0844), ($null))==1); // @line: 689 call $caughtEx2 := void$javaUtilEx.LinkedList$ListItr$checkForComodification$2687((r0844)); goto Block1223, Block1225; Block1223: assume ($neref(($caughtEx2), ($null))==1); goto Block1224; Block1225: assume ($eqref(($caughtEx2), ($null))==1); goto Block1226; Block1224: $Exep0 := $caughtEx2; return; Block1226: assert ($neref((r0844), ($null))==1); // @line: 690 $r3845 := $HeapVar[r0844, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$ListItr$lastReturned303]; assert ($neref(($r3845), ($null))==1); // @line: 690 r1846 := $HeapVar[$r3845, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$next301]; goto Block1227; // @line: 692 Block1227: assert ($neref((r0844), ($null))==1); // @line: 692 $r5848 := $HeapVar[r0844, javaUtilEx.LinkedList$javaUtilEx.LinkedList$ListItr$this$0305]; assert ($neref((r0844), ($null))==1); // @line: 692 $r4847 := $HeapVar[r0844, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$ListItr$lastReturned303]; // @line: 692 call $freshlocal4, $caughtEx3 := java.lang.Object$javaUtilEx.LinkedList$access$200$2671(($r5848), ($r4847)); goto Block1230, Block1228; // @line: 692 Block1230: assume ($eqref(($caughtEx3), ($null))==1); goto Block1231; // @line: 692 Block1228: assume ($neref(($caughtEx3), ($null))==1); $caughtEx5 := $caughtEx3; goto Block1229; // @line: 692 Block1231: goto Block1232; // @line: 702 Block1229: // @line: 702 $r11858 := $caughtEx5; goto Block1234; // @line: 695 Block1232: goto Block1233; // @line: 694 Block1234: // @line: 694 $r12860 := $newvariable((1235)); assume ($neref(($newvariable((1235))), ($null))==1); assert ($neref(($r12860), ($null))==1); // @line: 694 call void$javaUtilEx.IllegalStateException$$la$init$ra$$2574(($r12860)); goto Block1236; // @line: 696 Block1233: assert ($neref((r0844), ($null))==1); // @line: 696 $r8851 := $HeapVar[r0844, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$ListItr$next304]; goto Block1237; // @line: 694 Block1236: $Exep1 := $r12860; return; // @line: 696 Block1237: assert ($neref((r0844), ($null))==1); // @line: 696 $r7850 := $HeapVar[r0844, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$ListItr$lastReturned303]; goto Block1238; // @line: 696 Block1238: goto Block1239, Block1241; // @line: 696 Block1239: assume ($neref(($r8851), ($r7850))==1); goto Block1240; // @line: 696 Block1241: // @line: 696 assume ($negInt(($neref(($r8851), ($r7850))))==1); assert ($neref((r0844), ($null))==1); // @line: 697 $HeapVar[r0844, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$ListItr$next304] := r1846; goto Block1242; // @line: 699 Block1240: assert ($neref((r0844), ($null))==1); // @line: 699 $i0852 := $HeapVar[r0844, int$javaUtilEx.LinkedList$ListItr$nextIndex0]; goto Block1243; // @line: 700 Block1242: assert ($neref((r0844), ($null))==1); // @line: 700 $r9854 := $HeapVar[r0844, javaUtilEx.LinkedList$javaUtilEx.LinkedList$ListItr$this$0305]; // @line: 700 call $r10855 := javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$access$000$2669(($r9854)); assert ($neref((r0844), ($null))==1); // @line: 700 $HeapVar[r0844, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$ListItr$lastReturned303] := $r10855; assert ($neref((r0844), ($null))==1); // @line: 701 $i2856 := $HeapVar[r0844, int$javaUtilEx.LinkedList$ListItr$expectedModCount0]; // @line: 701 $i3857 := $addint(($i2856), (1)); assert ($neref((r0844), ($null))==1); // @line: 701 $HeapVar[r0844, int$javaUtilEx.LinkedList$ListItr$expectedModCount0] := $i3857; return; // @line: 699 Block1243: // @line: 699 $i1853 := $subint(($i0852), (1)); assert ($neref((r0844), ($null))==1); // @line: 699 $HeapVar[r0844, int$javaUtilEx.LinkedList$ListItr$nextIndex0] := $i1853; goto Block1242; } // ()> procedure void$java.lang.StringBuilder$$la$init$ra$$2261(__this : ref); // procedure java.lang.Object$javaUtilEx.AbstractList$get$2485(__this : ref, $param_0 : int) returns (__ret : ref); // @line: 90 // (java.lang.Throwable)> procedure void$javaUtilEx.IllegalArgumentException$$la$init$ra$$2625(__this : ref, $param_0 : ref) requires ($neref((__this), ($null))==1); { var r0514 : ref; var r1515 : ref; Block752: r0514 := __this; r1515 := $param_0; assert ($neref((r0514), ($null))==1); // @line: 91 call void$java.lang.RuntimeException$$la$init$ra$$763((r0514), (r1515)); return; } // procedure is generated by joogie. function {:inline true} $modref($param00 : ref, $param11 : ref) returns (__ret : ref); // @line: 761 // procedure void$javaUtilEx.SubList$rangeCheckForAdd$2562(__this : ref, $param_0 : int) returns ($Exep0 : ref) modifies $stringSize; requires ($neref((__this), ($null))==1); { var $r1406 : ref; var i0405 : int; var $r2408 : ref; var r0407 : ref; var $i1409 : int; //temp local variables // @line: 761 Block538: $Exep0 := $null; goto Block658; Block658: r0407 := __this; i0405 := $param_0; goto Block659; // @line: 762 Block659: goto Block660, Block662; // @line: 762 Block660: assume ($ltint((i0405), (0))==1); goto Block661; // @line: 762 Block662: // @line: 762 assume ($negInt(($ltint((i0405), (0))))==1); assert ($neref((r0407), ($null))==1); // @line: 763 $i1409 := $HeapVar[r0407, int$javaUtilEx.SubList$size0]; goto Block663; // @line: 763 Block661: // @line: 763 $r1406 := $newvariable((667)); assume ($neref(($newvariable((667))), ($null))==1); assert ($neref((r0407), ($null))==1); // @line: 763 call $r2408 := java.lang.String$javaUtilEx.SubList$outOfBoundsMsg$2563((r0407), (i0405)); assert ($neref(($r1406), ($null))==1); // @line: 763 call void$java.lang.IndexOutOfBoundsException$$la$init$ra$$2076(($r1406), ($r2408)); goto Block668; // @line: 763 Block663: goto Block664, Block666; // @line: 763 Block668: $Exep0 := $r1406; return; // @line: 763 Block664: assume ($leint((i0405), ($i1409))==1); goto Block665; // @line: 763 Block666: // @line: 763 assume ($negInt(($leint((i0405), ($i1409))))==1); goto Block661; // @line: 764 Block665: return; } // procedure is generated by joogie. function {:inline true} $nereal(x : realVar, y : realVar) returns (__ret : int) { if (x != y) then 1 else 0 } // @line: 298 // procedure void$javaUtilEx.AbstractCollection$clear$2239(__this : ref) requires ($neref((__this), ($null))==1); { var r061 : ref; var r163 : ref; var $z064 : int; //temp local variables var $freshlocal0 : ref; Block106: r061 := __this; assert ($neref((r061), ($null))==1); // @line: 299 call r163 := javaUtilEx.Iterator$javaUtilEx.AbstractCollection$iterator$2229((r061)); goto Block107; // @line: 300 Block107: assert ($neref((r163), ($null))==1); // @line: 300 call $z064 := boolean$javaUtilEx.Iterator$hasNext$2254((r163)); goto Block108; // @line: 300 Block108: goto Block109, Block111; // @line: 300 Block109: assume ($eqint(($z064), (0))==1); goto Block110; // @line: 300 Block111: // @line: 300 assume ($negInt(($eqint(($z064), (0))))==1); assert ($neref((r163), ($null))==1); // @line: 301 call $freshlocal0 := java.lang.Object$javaUtilEx.Iterator$next$2255((r163)); assert ($neref((r163), ($null))==1); // @line: 302 call void$javaUtilEx.Iterator$remove$2256((r163)); goto Block107; // @line: 304 Block110: return; } // procedure is generated by joogie. function {:inline true} $orref($param00 : ref, $param11 : ref) returns (__ret : int); // procedure is generated by joogie. function {:inline true} $shlreal($param00 : realVar, $param11 : realVar) returns (__ret : int); // @line: 756 // procedure void$javaUtilEx.SubList$rangeCheck$2561(__this : ref, $param_0 : int) returns ($Exep0 : ref) modifies $stringSize; requires ($neref((__this), ($null))==1); { var $r1401 : ref; var $i1404 : int; var r0402 : ref; var $r2403 : ref; var i0400 : int; //temp local variables // @line: 756 Block506: $Exep0 := $null; goto Block647; Block647: r0402 := __this; i0400 := $param_0; goto Block648; // @line: 757 Block648: goto Block649, Block651; // @line: 757 Block649: assume ($ltint((i0400), (0))==1); goto Block650; // @line: 757 Block651: // @line: 757 assume ($negInt(($ltint((i0400), (0))))==1); assert ($neref((r0402), ($null))==1); // @line: 758 $i1404 := $HeapVar[r0402, int$javaUtilEx.SubList$size0]; goto Block652; // @line: 758 Block650: // @line: 758 $r1401 := $newvariable((656)); assume ($neref(($newvariable((656))), ($null))==1); assert ($neref((r0402), ($null))==1); // @line: 758 call $r2403 := java.lang.String$javaUtilEx.SubList$outOfBoundsMsg$2563((r0402), (i0400)); assert ($neref(($r1401), ($null))==1); // @line: 758 call void$java.lang.IndexOutOfBoundsException$$la$init$ra$$2076(($r1401), ($r2403)); goto Block657; // @line: 758 Block652: goto Block655, Block653; // @line: 758 Block657: $Exep0 := $r1401; return; // @line: 758 Block655: // @line: 758 assume ($negInt(($ltint((i0400), ($i1404))))==1); goto Block650; // @line: 758 Block653: assume ($ltint((i0400), ($i1404))==1); goto Block654; // @line: 759 Block654: return; } // @line: 795 // procedure java.lang.Object$lp$$rp$$javaUtilEx.LinkedList$toArray$2668(__this : ref) returns (__ret : [int]ref) modifies $refArrSize; requires ($neref((__this), ($null))==1); { var $i1757 : int; var r5760 : ref; var $r3756 : ref; var $i0751 : int; var r0750 : ref; var i2759 : int; var $r4758 : ref; var r1752 : [int]ref; var $r2754 : ref; Block1134: r0750 := __this; assert ($neref((r0750), ($null))==1); // @line: 796 $i0751 := $HeapVar[r0750, int$javaUtilEx.LinkedList$size0]; // @line: 796 r1752 := $reftorefarr(($newvariable((1135)))); $refArrSize[$reftorefarr(($newvariable((1135))))[$arrSizeIdx]] := $i0751; assume ($negInt(($eqrefarray(($reftorefarr(($newvariable((1135))))), ($refArrNull))))==1); // @line: 797 i2759 := 0; assert ($neref((r0750), ($null))==1); // @line: 798 $r2754 := $HeapVar[r0750, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$header298]; assert ($neref(($r2754), ($null))==1); // @line: 798 r5760 := $HeapVar[$r2754, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$next301]; goto Block1136; // @line: 798 Block1136: assert ($neref((r0750), ($null))==1); // @line: 798 $r3756 := $HeapVar[r0750, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$header298]; goto Block1137; // @line: 798 Block1137: goto Block1138, Block1140; // @line: 798 Block1138: assume ($eqref((r5760), ($r3756))==1); goto Block1139; // @line: 798 Block1140: // @line: 798 assume ($negInt(($eqref((r5760), ($r3756))))==1); // @line: 799 $i1757 := i2759; // @line: 799 i2759 := $addint((i2759), (1)); assert ($neref((r5760), ($null))==1); // @line: 799 $r4758 := $HeapVar[r5760, java.lang.Object$javaUtilEx.LinkedList$Entry$element300]; assert ($geint(($i1757), (0))==1); assert ($ltint(($i1757), ($refArrSize[r1752[$arrSizeIdx]]))==1); // @line: 799 r1752[$i1757] := $r4758; assert ($neref((r5760), ($null))==1); // @line: 798 r5760 := $HeapVar[r5760, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$next301]; goto Block1136; // @line: 800 Block1139: // @line: 800 __ret := r1752; return; } // @line: 181 // procedure boolean$javaUtilEx.AbstractCollection$containsAll$2235(__this : ref, $param_0 : ref) returns (__ret : int) requires ($neref((__this), ($null))==1); { var r229 : ref; var r127 : ref; var $z030 : int; var r031 : ref; var $r332 : ref; var $z133 : int; Block65: r031 := __this; r127 := $param_0; assert ($neref((r127), ($null))==1); // @line: 182 call r229 := javaUtilEx.Iterator$javaUtilEx.Collection$iterator$2244((r127)); goto Block66; // @line: 183 Block66: assert ($neref((r229), ($null))==1); // @line: 183 call $z030 := boolean$javaUtilEx.Iterator$hasNext$2254((r229)); goto Block67; // @line: 183 Block67: goto Block70, Block68; // @line: 183 Block70: // @line: 183 assume ($negInt(($eqint(($z030), (0))))==1); assert ($neref((r229), ($null))==1); // @line: 184 call $r332 := java.lang.Object$javaUtilEx.Iterator$next$2255((r229)); assert ($neref((r031), ($null))==1); // @line: 184 call $z133 := boolean$javaUtilEx.AbstractCollection$contains$2232((r031), ($r332)); goto Block71; // @line: 183 Block68: assume ($eqint(($z030), (0))==1); goto Block69; // @line: 184 Block71: goto Block72, Block73; // @line: 186 Block69: // @line: 186 __ret := 1; return; // @line: 184 Block72: assume ($neint(($z133), (0))==1); goto Block66; // @line: 184 Block73: // @line: 184 assume ($negInt(($neint(($z133), (0))))==1); // @line: 185 __ret := 0; return; } // @line: 160 // procedure java.lang.Object$javaUtilEx.AbstractList$remove$2488(__this : ref, $param_0 : int) returns (__ret : ref, $Exep0 : ref) requires ($neref((__this), ($null))==1); { var $r1116 : ref; var r0117 : ref; var i0118 : int; //temp local variables // @line: 160 Block153: $Exep0 := $null; goto Block154; Block154: r0117 := __this; i0118 := $param_0; // @line: 161 $r1116 := $newvariable((155)); assume ($neref(($newvariable((155))), ($null))==1); assert ($neref(($r1116), ($null))==1); // @line: 161 call void$javaUtilEx.UnsupportedOperationException$$la$init$ra$$2257(($r1116)); goto Block156; Block156: $Exep0 := $r1116; return; } // @line: 396 // procedure boolean$javaUtilEx.AbstractList$ListItr$hasPrevious$2543(__this : ref) returns (__ret : int) requires ($neref((__this), ($null))==1); { var $i0273 : int; var r0272 : ref; var $z0275 : int; Block425: r0272 := __this; assert ($neref((r0272), ($null))==1); // @line: 397 $i0273 := $HeapVar[r0272, int$javaUtilEx.AbstractList$Itr$cursor0]; goto Block426; // @line: 397 Block426: goto Block427, Block429; // @line: 397 Block427: assume ($eqint(($i0273), (0))==1); goto Block428; // @line: 397 Block429: // @line: 397 assume ($negInt(($eqint(($i0273), (0))))==1); // @line: 397 $z0275 := 1; goto Block430; // @line: 397 Block428: // @line: 397 $z0275 := 0; goto Block430; // @line: 397 Block430: // @line: 397 __ret := $z0275; return; } // @line: 767 // (javaUtilEx.LinkedList,javaUtilEx.LinkedList$1)> procedure void$javaUtilEx.LinkedList$DescendingIterator$$la$init$ra$$2692(__this : ref, $param_0 : ref, $param_1 : ref) returns ($Exep0 : ref) requires ($neref((__this), ($null))==1); { var r0898 : ref; var r1899 : ref; var r2900 : ref; //temp local variables var $caughtEx1 : ref; // @line: 767 Block1126: $caughtEx1 := $null; $Exep0 := $null; goto Block1297; Block1297: r0898 := __this; r1899 := $param_0; r2900 := $param_1; assert ($neref((r0898), ($null))==1); // @line: 768 call $caughtEx1 := void$javaUtilEx.LinkedList$DescendingIterator$$la$init$ra$$2688((r0898), (r1899)); goto Block1298, Block1300; Block1298: assume ($neref(($caughtEx1), ($null))==1); goto Block1299; Block1300: assume ($eqref(($caughtEx1), ($null))==1); goto Block1301; Block1299: $Exep0 := $caughtEx1; return; Block1301: return; } // procedure boolean$java.lang.Object$equals$32(__this : ref, $param_0 : ref) returns (__ret : int); // @line: 7 // procedure int$javaUtilEx.Random$random$2674() returns (__ret : int) modifies int$javaUtilEx.Random$index0, $stringSize; { var $i2777 : int; var r0775 : ref; var $i3778 : int; var $i0773 : int; var $i1776 : int; var $r1774 : [int]ref; // @line: 8 Block1151: // @line: 8 $r1774 := java.lang.String$lp$$rp$$javaUtilEx.Random$args299; // @line: 8 $i0773 := int$javaUtilEx.Random$index0; assert ($geint(($i0773), (0))==1); assert ($ltint(($i0773), ($refArrSize[$r1774[$arrSizeIdx]]))==1); // @line: 8 r0775 := $r1774[$i0773]; // @line: 9 $i1776 := int$javaUtilEx.Random$index0; // @line: 9 $i2777 := $addint(($i1776), (1)); // @line: 9 int$javaUtilEx.Random$index0 := $i2777; $i3778 := $stringSize[r0775]; // @line: 10 __ret := $i3778; return; } // @line: 669 // procedure void$javaUtilEx.SubList$removeRange$2555(__this : ref, $param_0 : int, $param_1 : int) returns ($Exep0 : ref, $Exep1 : ref) modifies $HeapVar; requires ($neref((__this), ($null))==1); { var r0361 : ref; var i1364 : int; var $i7371 : int; var i0362 : int; var $r1368 : ref; var $i2363 : int; var $i8372 : int; var $i4366 : int; var $i6370 : int; var $i3365 : int; var $r2369 : ref; var $i9373 : int; var $i5367 : int; //temp local variables var $caughtEx3 : ref; var $caughtEx2 : ref; // @line: 669 Block567: $caughtEx3 := $null; $caughtEx2 := $null; $Exep1 := $null; $Exep0 := $null; goto Block568; Block568: r0361 := __this; i0362 := $param_0; i1364 := $param_1; assert ($neref((r0361), ($null))==1); // @line: 670 call $caughtEx2 := void$javaUtilEx.SubList$checkForComodification$2564((r0361)); goto Block569, Block571; Block569: assume ($neref(($caughtEx2), ($null))==1); goto Block570; Block571: assume ($eqref(($caughtEx2), ($null))==1); goto Block572; Block570: $Exep0 := $caughtEx2; return; Block572: assert ($neref((r0361), ($null))==1); // @line: 671 $r1368 := $HeapVar[r0361, javaUtilEx.AbstractList$javaUtilEx.SubList$l297]; assert ($neref((r0361), ($null))==1); // @line: 671 $i2363 := $HeapVar[r0361, int$javaUtilEx.SubList$offset0]; // @line: 671 $i5367 := $addint((i0362), ($i2363)); assert ($neref((r0361), ($null))==1); // @line: 671 $i3365 := $HeapVar[r0361, int$javaUtilEx.SubList$offset0]; // @line: 671 $i4366 := $addint((i1364), ($i3365)); assert ($neref(($r1368), ($null))==1); // @line: 671 call $caughtEx3 := void$javaUtilEx.AbstractList$removeRange$2499(($r1368), ($i5367), ($i4366)); goto Block573, Block575; Block573: assume ($neref(($caughtEx3), ($null))==1); goto Block574; Block575: assume ($eqref(($caughtEx3), ($null))==1); goto Block576; Block574: $Exep1 := $caughtEx3; return; Block576: assert ($neref((r0361), ($null))==1); // @line: 672 $r2369 := $HeapVar[r0361, javaUtilEx.AbstractList$javaUtilEx.SubList$l297]; assert ($neref(($r2369), ($null))==1); // @line: 672 $i6370 := $HeapVar[$r2369, int$javaUtilEx.AbstractList$modCount0]; assert ($neref((r0361), ($null))==1); // @line: 672 $HeapVar[r0361, int$javaUtilEx.AbstractList$modCount0] := $i6370; assert ($neref((r0361), ($null))==1); // @line: 673 $i8372 := $HeapVar[r0361, int$javaUtilEx.SubList$size0]; // @line: 673 $i7371 := $subint((i1364), (i0362)); // @line: 673 $i9373 := $subint(($i8372), ($i7371)); assert ($neref((r0361), ($null))==1); // @line: 673 $HeapVar[r0361, int$javaUtilEx.SubList$size0] := $i9373; return; } // procedure is generated by joogie. function {:inline true} $andreal($param00 : realVar, $param11 : realVar) returns (__ret : int); // (java.lang.String)> procedure void$java.lang.IndexOutOfBoundsException$$la$init$ra$$2076(__this : ref, $param_0 : ref); // @line: 89 // (java.lang.Throwable)> procedure void$javaUtilEx.UnsupportedOperationException$$la$init$ra$$2260(__this : ref, $param_0 : ref) requires ($neref((__this), ($null))==1); { var r1103 : ref; var r0102 : ref; Block137: r0102 := __this; r1103 := $param_0; assert ($neref((r0102), ($null))==1); // @line: 90 call void$java.lang.RuntimeException$$la$init$ra$$763((r0102), (r1103)); return; } // procedure boolean$javaUtilEx.ListIterator$hasPrevious$2527(__this : ref) returns (__ret : int); // @line: 90 // procedure int$javaUtilEx.LinkedList$access$100$2670($param_0 : ref) returns (__ret : int) { var $i0764 : int; var r0763 : ref; Block1142: r0763 := $param_0; assert ($neref((r0763), ($null))==1); // @line: 91 $i0764 := $HeapVar[r0763, int$javaUtilEx.LinkedList$size0]; // @line: 91 __ret := $i0764; return; } // procedure boolean$javaUtilEx.Iterator$hasNext$2254(__this : ref) returns (__ret : int); // @line: 355 // procedure java.lang.Object$javaUtilEx.AbstractList$Itr$next$2536(__this : ref) returns (__ret : ref, $Exep0 : ref, $Exep1 : ref) modifies $HeapVar; requires ($neref((__this), ($null))==1); { var $r3234 : ref; var $r2230 : ref; var r0228 : ref; var $i0233 : int; var i1236 : int; var r1232 : ref; var $r4235 : ref; //temp local variables var $caughtEx2 : ref; var $caughtEx3 : ref; // @line: 355 Block355: $caughtEx3 := $null; $caughtEx2 := $null; $Exep1 := $null; $Exep0 := $null; goto Block356; Block356: r0228 := __this; assert ($neref((r0228), ($null))==1); // @line: 356 call $caughtEx2 := void$javaUtilEx.AbstractList$Itr$checkForComodification$2538((r0228)); goto Block357, Block359; Block357: assume ($neref(($caughtEx2), ($null))==1); goto Block358; Block359: assume ($eqref(($caughtEx2), ($null))==1); goto Block360; Block358: $Exep0 := $caughtEx2; return; Block360: goto Block361; // @line: 358 Block361: assert ($neref((r0228), ($null))==1); // @line: 358 i1236 := $HeapVar[r0228, int$javaUtilEx.AbstractList$Itr$cursor0]; assert ($neref((r0228), ($null))==1); // @line: 359 $r2230 := $HeapVar[r0228, javaUtilEx.AbstractList$javaUtilEx.AbstractList$Itr$this$0295]; assert ($neref(($r2230), ($null))==1); // @line: 359 call r1232 := java.lang.Object$javaUtilEx.AbstractList$get$2485(($r2230), (i1236)); assert ($neref((r0228), ($null))==1); // @line: 360 $HeapVar[r0228, int$javaUtilEx.AbstractList$Itr$lastRet0] := i1236; // @line: 361 $i0233 := $addint((i1236), (1)); assert ($neref((r0228), ($null))==1); // @line: 361 $HeapVar[r0228, int$javaUtilEx.AbstractList$Itr$cursor0] := $i0233; goto Block362; // @line: 362 Block362: // @line: 362 __ret := r1232; return; } // @line: 670 // procedure java.lang.Object$javaUtilEx.LinkedList$ListItr$previous$2681(__this : ref) returns (__ret : ref, $Exep1 : ref, $Exep0 : ref) modifies $HeapVar; requires ($neref((__this), ($null))==1); { var $r1832 : ref; var $i1834 : int; var r0830 : ref; var $r5838 : ref; var $r2833 : ref; var $i0831 : int; var $i2835 : int; var $r3836 : ref; var $r4837 : ref; //temp local variables var $caughtEx2 : ref; // @line: 670 Block1206: $caughtEx2 := $null; $Exep1 := $null; $Exep0 := $null; goto Block1207; Block1207: r0830 := __this; assert ($neref((r0830), ($null))==1); // @line: 671 $i0831 := $HeapVar[r0830, int$javaUtilEx.LinkedList$ListItr$nextIndex0]; goto Block1208; // @line: 671 Block1208: goto Block1211, Block1209; // @line: 671 Block1211: // @line: 671 assume ($negInt(($neint(($i0831), (0))))==1); // @line: 672 $r5838 := $newvariable((1212)); assume ($neref(($newvariable((1212))), ($null))==1); assert ($neref(($r5838), ($null))==1); // @line: 672 call void$javaUtilEx.NoSuchElementException$$la$init$ra$$2572(($r5838)); goto Block1213; // @line: 671 Block1209: assume ($neint(($i0831), (0))==1); goto Block1210; // @line: 671 Block1213: $Exep0 := $r5838; return; // @line: 674 Block1210: assert ($neref((r0830), ($null))==1); // @line: 674 $r1832 := $HeapVar[r0830, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$ListItr$next304]; goto Block1214; // @line: 674 Block1214: assert ($neref(($r1832), ($null))==1); // @line: 674 $r2833 := $HeapVar[$r1832, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$previous302]; assert ($neref((r0830), ($null))==1); // @line: 674 $HeapVar[r0830, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$ListItr$next304] := $r2833; assert ($neref((r0830), ($null))==1); // @line: 674 $HeapVar[r0830, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$ListItr$lastReturned303] := $r2833; assert ($neref((r0830), ($null))==1); // @line: 675 $i1834 := $HeapVar[r0830, int$javaUtilEx.LinkedList$ListItr$nextIndex0]; // @line: 675 $i2835 := $subint(($i1834), (1)); assert ($neref((r0830), ($null))==1); // @line: 675 $HeapVar[r0830, int$javaUtilEx.LinkedList$ListItr$nextIndex0] := $i2835; assert ($neref((r0830), ($null))==1); // @line: 676 call $caughtEx2 := void$javaUtilEx.LinkedList$ListItr$checkForComodification$2687((r0830)); goto Block1215, Block1217; // @line: 674 Block1215: assume ($neref(($caughtEx2), ($null))==1); goto Block1216; // @line: 674 Block1217: assume ($eqref(($caughtEx2), ($null))==1); goto Block1218; // @line: 674 Block1216: $Exep1 := $caughtEx2; return; // @line: 674 Block1218: assert ($neref((r0830), ($null))==1); // @line: 677 $r3836 := $HeapVar[r0830, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$ListItr$lastReturned303]; assert ($neref(($r3836), ($null))==1); // @line: 677 $r4837 := $HeapVar[$r3836, java.lang.Object$javaUtilEx.LinkedList$Entry$element300]; // @line: 677 __ret := $r4837; return; } // @line: 719 // procedure void$javaUtilEx.LinkedList$ListItr$checkForComodification$2687(__this : ref) returns ($Exep0 : ref) requires ($neref((__this), ($null))==1); { var r0879 : ref; var $i0881 : int; var $r2883 : ref; var $r1880 : ref; var $i1882 : int; //temp local variables // @line: 719 Block1186: $Exep0 := $null; goto Block1263; Block1263: r0879 := __this; assert ($neref((r0879), ($null))==1); // @line: 720 $r1880 := $HeapVar[r0879, javaUtilEx.LinkedList$javaUtilEx.LinkedList$ListItr$this$0305]; assert ($neref(($r1880), ($null))==1); // @line: 720 $i1882 := $HeapVar[$r1880, int$javaUtilEx.AbstractList$modCount0]; assert ($neref((r0879), ($null))==1); // @line: 720 $i0881 := $HeapVar[r0879, int$javaUtilEx.LinkedList$ListItr$expectedModCount0]; goto Block1264; // @line: 720 Block1264: goto Block1265, Block1267; // @line: 720 Block1265: assume ($eqint(($i1882), ($i0881))==1); goto Block1266; // @line: 720 Block1267: // @line: 720 assume ($negInt(($eqint(($i1882), ($i0881))))==1); // @line: 721 $r2883 := $newvariable((1268)); assume ($neref(($newvariable((1268))), ($null))==1); assert ($neref(($r2883), ($null))==1); // @line: 721 call void$javaUtilEx.ConcurrentModificationException$$la$init$ra$$2570(($r2883)); goto Block1269; // @line: 722 Block1266: return; // @line: 720 Block1269: $Exep0 := $r2883; return; } // procedure is generated by joogie. function {:inline true} $addint(x : int, y : int) returns (__ret : int) { (x + y) } // procedure is generated by joogie. function {:inline true} $subref($param00 : ref, $param11 : ref) returns (__ret : ref); // @line: 546 // procedure void$javaUtilEx.LinkedList$push$2660(__this : ref, $param_0 : ref) requires ($neref((__this), ($null))==1); { var r0698 : ref; var r1699 : ref; Block1060: r0698 := __this; r1699 := $param_0; assert ($neref((r0698), ($null))==1); // @line: 547 call void$javaUtilEx.LinkedList$addFirst$2635((r0698), (r1699)); return; } // @line: 636 // (javaUtilEx.LinkedList,int)> procedure void$javaUtilEx.LinkedList$ListItr$$la$init$ra$$2677(__this : ref, $param_0 : ref, $param_1 : int) returns ($Exep0 : ref) modifies $HeapVar; requires ($neref((__this), ($null))==1); { var $r11804 : ref; var $r2785 : ref; var $r10802 : ref; var $r8798 : ref; var $i3792 : int; var $i4793 : int; var $i7799 : int; var $r12805 : ref; var $i1788 : int; var $r5790 : ref; var $i10806 : int; var $r7797 : ref; var i0789 : int; var $i9803 : int; var $r9801 : ref; var r1784 : ref; var $i11807 : int; var $i5795 : int; var $i6796 : int; var $r4787 : ref; var r0783 : ref; var $r6794 : ref; var $i8800 : int; var $r3786 : ref; var $i2791 : int; //temp local variables // @line: 636 Block1107: $Exep0 := $null; goto Block1154; Block1154: r0783 := __this; r1784 := $param_0; i0789 := $param_1; assert ($neref((r0783), ($null))==1); // @line: 637 $HeapVar[r0783, javaUtilEx.LinkedList$javaUtilEx.LinkedList$ListItr$this$0305] := r1784; assert ($neref((r0783), ($null))==1); // @line: 637 call void$java.lang.Object$$la$init$ra$$28((r0783)); assert ($neref((r0783), ($null))==1); // @line: 632 $r2785 := $HeapVar[r0783, javaUtilEx.LinkedList$javaUtilEx.LinkedList$ListItr$this$0305]; // @line: 632 call $r3786 := javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$access$000$2669(($r2785)); assert ($neref((r0783), ($null))==1); // @line: 632 $HeapVar[r0783, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$ListItr$lastReturned303] := $r3786; assert ($neref((r0783), ($null))==1); // @line: 635 $r4787 := $HeapVar[r0783, javaUtilEx.LinkedList$javaUtilEx.LinkedList$ListItr$this$0305]; assert ($neref(($r4787), ($null))==1); // @line: 635 $i1788 := $HeapVar[$r4787, int$javaUtilEx.AbstractList$modCount0]; assert ($neref((r0783), ($null))==1); // @line: 635 $HeapVar[r0783, int$javaUtilEx.LinkedList$ListItr$expectedModCount0] := $i1788; goto Block1155; // @line: 638 Block1155: goto Block1158, Block1156; // @line: 638 Block1158: // @line: 638 assume ($negInt(($ltint((i0789), (0))))==1); // @line: 639 call $i2791 := int$javaUtilEx.LinkedList$access$100$2670((r1784)); goto Block1159; // @line: 638 Block1156: assume ($ltint((i0789), (0))==1); goto Block1157; // @line: 639 Block1159: goto Block1162, Block1160; // @line: 639 Block1157: // @line: 639 $r5790 := $newvariable((1163)); assume ($neref(($newvariable((1163))), ($null))==1); assert ($neref(($r5790), ($null))==1); // @line: 639 call void$java.lang.IndexOutOfBoundsException$$la$init$ra$$2075(($r5790)); goto Block1164; // @line: 639 Block1162: // @line: 639 assume ($negInt(($leint((i0789), ($i2791))))==1); goto Block1157; // @line: 639 Block1160: assume ($leint((i0789), ($i2791))==1); goto Block1161; // @line: 639 Block1164: $Exep0 := $r5790; return; // @line: 640 Block1161: // @line: 640 call $i3792 := int$javaUtilEx.LinkedList$access$100$2670((r1784)); goto Block1165; // @line: 640 Block1165: // @line: 640 $i4793 := $shrint(($i3792), (1)); goto Block1166; // @line: 640 Block1166: goto Block1169, Block1167; // @line: 640 Block1169: // @line: 640 assume ($negInt(($geint((i0789), ($i4793))))==1); // @line: 641 call $r9801 := javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$access$000$2669((r1784)); assert ($neref(($r9801), ($null))==1); // @line: 641 $r10802 := $HeapVar[$r9801, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$next301]; assert ($neref((r0783), ($null))==1); // @line: 641 $HeapVar[r0783, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$ListItr$next304] := $r10802; assert ($neref((r0783), ($null))==1); // @line: 642 $HeapVar[r0783, int$javaUtilEx.LinkedList$ListItr$nextIndex0] := 0; goto Block1170; // @line: 640 Block1167: assume ($geint((i0789), ($i4793))==1); goto Block1168; // @line: 642 Block1170: assert ($neref((r0783), ($null))==1); // @line: 642 $i9803 := $HeapVar[r0783, int$javaUtilEx.LinkedList$ListItr$nextIndex0]; goto Block1171; // @line: 645 Block1168: // @line: 645 call $r6794 := javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$access$000$2669((r1784)); goto Block1175; // @line: 642 Block1171: goto Block1174, Block1172; // @line: 645 Block1175: assert ($neref((r0783), ($null))==1); // @line: 645 $HeapVar[r0783, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$ListItr$next304] := $r6794; // @line: 646 call $i5795 := int$javaUtilEx.LinkedList$access$100$2670((r1784)); assert ($neref((r0783), ($null))==1); // @line: 646 $HeapVar[r0783, int$javaUtilEx.LinkedList$ListItr$nextIndex0] := $i5795; goto Block1176; // @line: 642 Block1174: // @line: 642 assume ($negInt(($geint(($i9803), (i0789))))==1); assert ($neref((r0783), ($null))==1); // @line: 643 $r11804 := $HeapVar[r0783, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$ListItr$next304]; assert ($neref(($r11804), ($null))==1); // @line: 643 $r12805 := $HeapVar[$r11804, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$next301]; assert ($neref((r0783), ($null))==1); // @line: 643 $HeapVar[r0783, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$ListItr$next304] := $r12805; assert ($neref((r0783), ($null))==1); // @line: 642 $i10806 := $HeapVar[r0783, int$javaUtilEx.LinkedList$ListItr$nextIndex0]; // @line: 642 $i11807 := $addint(($i10806), (1)); assert ($neref((r0783), ($null))==1); // @line: 642 $HeapVar[r0783, int$javaUtilEx.LinkedList$ListItr$nextIndex0] := $i11807; goto Block1170; // @line: 642 Block1172: assume ($geint(($i9803), (i0789))==1); goto Block1173; // @line: 646 Block1176: assert ($neref((r0783), ($null))==1); // @line: 646 $i6796 := $HeapVar[r0783, int$javaUtilEx.LinkedList$ListItr$nextIndex0]; goto Block1177; // @line: 649 Block1173: return; // @line: 646 Block1177: goto Block1178, Block1179; // @line: 646 Block1178: assume ($leint(($i6796), (i0789))==1); goto Block1173; // @line: 646 Block1179: // @line: 646 assume ($negInt(($leint(($i6796), (i0789))))==1); assert ($neref((r0783), ($null))==1); // @line: 647 $r7797 := $HeapVar[r0783, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$ListItr$next304]; assert ($neref(($r7797), ($null))==1); // @line: 647 $r8798 := $HeapVar[$r7797, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$previous302]; assert ($neref((r0783), ($null))==1); // @line: 647 $HeapVar[r0783, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$ListItr$next304] := $r8798; assert ($neref((r0783), ($null))==1); // @line: 646 $i7799 := $HeapVar[r0783, int$javaUtilEx.LinkedList$ListItr$nextIndex0]; // @line: 646 $i8800 := $subint(($i7799), (1)); assert ($neref((r0783), ($null))==1); // @line: 646 $HeapVar[r0783, int$javaUtilEx.LinkedList$ListItr$nextIndex0] := $i8800; goto Block1176; } // @line: 43 // ()> procedure void$javaUtilEx.IllegalStateException$$la$init$ra$$2574(__this : ref) requires ($neref((__this), ($null))==1); { var r0435 : ref; Block686: r0435 := __this; assert ($neref((r0435), ($null))==1); // @line: 44 call void$java.lang.RuntimeException$$la$init$ra$$760((r0435)); return; } // procedure is generated by joogie. function {:inline true} $divref($param00 : ref, $param11 : ref) returns (__ret : ref); // @line: 202 // procedure int$javaUtilEx.AbstractList$lastIndexOf$2490(__this : ref, $param_0 : ref) returns (__ret : int, $Exep0 : ref) requires ($neref((__this), ($null))==1); { var r1134 : ref; var r2133 : ref; var $i1138 : int; var $r4140 : ref; var $i0131 : int; var $z2139 : int; var $z1137 : int; var r0130 : ref; var $r3136 : ref; var $i2141 : int; var $z0135 : int; //temp local variables var $caughtEx1 : ref; // @line: 202 Block184: $caughtEx1 := $null; $Exep0 := $null; goto Block185; Block185: r0130 := __this; r1134 := $param_0; assert ($neref((r0130), ($null))==1); // @line: 203 call $i0131 := int$javaUtilEx.AbstractCollection$size$2230((r0130)); assert ($neref((r0130), ($null))==1); // @line: 203 call r2133, $caughtEx1 := javaUtilEx.ListIterator$javaUtilEx.AbstractList$listIterator$2495((r0130), ($i0131)); goto Block186, Block188; Block186: assume ($neref(($caughtEx1), ($null))==1); goto Block187; Block188: assume ($eqref(($caughtEx1), ($null))==1); goto Block189; Block187: $Exep0 := $caughtEx1; return; Block189: goto Block190; // @line: 204 Block190: goto Block193, Block191; // @line: 204 Block193: // @line: 204 assume ($negInt(($neref((r1134), ($null))))==1); goto Block194; // @line: 204 Block191: assume ($neref((r1134), ($null))==1); goto Block192; // @line: 205 Block194: assert ($neref((r2133), ($null))==1); // @line: 205 call $z2139 := boolean$javaUtilEx.ListIterator$hasPrevious$2527((r2133)); goto Block195; // @line: 209 Block192: assert ($neref((r2133), ($null))==1); // @line: 209 call $z0135 := boolean$javaUtilEx.ListIterator$hasPrevious$2527((r2133)); goto Block202; // @line: 205 Block195: goto Block196, Block198; // @line: 209 Block202: goto Block203, Block204; // @line: 205 Block196: assume ($eqint(($z2139), (0))==1); goto Block197; // @line: 205 Block198: // @line: 205 assume ($negInt(($eqint(($z2139), (0))))==1); assert ($neref((r2133), ($null))==1); // @line: 206 call $r4140 := java.lang.Object$javaUtilEx.ListIterator$previous$2528((r2133)); goto Block199; // @line: 209 Block203: assume ($eqint(($z0135), (0))==1); goto Block197; // @line: 209 Block204: // @line: 209 assume ($negInt(($eqint(($z0135), (0))))==1); assert ($neref((r2133), ($null))==1); // @line: 210 call $r3136 := java.lang.Object$javaUtilEx.ListIterator$previous$2528((r2133)); assert ($neref((r1134), ($null))==1); // @line: 210 call $z1137 := boolean$java.lang.Object$equals$32((r1134), ($r3136)); goto Block205; // @line: 213 Block197: // @line: 213 __ret := -1; return; // @line: 206 Block199: goto Block201, Block200; // @line: 210 Block205: goto Block206, Block207; // @line: 206 Block201: // @line: 206 assume ($negInt(($neref(($r4140), ($null))))==1); assert ($neref((r2133), ($null))==1); // @line: 207 call $i2141 := int$javaUtilEx.ListIterator$nextIndex$2529((r2133)); // @line: 207 __ret := $i2141; return; // @line: 206 Block200: assume ($neref(($r4140), ($null))==1); goto Block194; // @line: 210 Block206: assume ($eqint(($z1137), (0))==1); goto Block192; // @line: 210 Block207: // @line: 210 assume ($negInt(($eqint(($z1137), (0))))==1); assert ($neref((r2133), ($null))==1); // @line: 211 call $i1138 := int$javaUtilEx.ListIterator$nextIndex$2529((r2133)); // @line: 211 __ret := $i1138; return; } // procedure int$javaUtilEx.Collection$size$2241(__this : ref) returns (__ret : int); // procedure is generated by joogie. function {:inline true} $neint(x : int, y : int) returns (__ret : int) { if (x != y) then 1 else 0 } // @line: 51 // (java.lang.String)> procedure void$javaUtilEx.UnsupportedOperationException$$la$init$ra$$2258(__this : ref, $param_0 : ref) requires ($neref((__this), ($null))==1); { var r097 : ref; var r198 : ref; Block135: r097 := __this; r198 := $param_0; assert ($neref((r097), ($null))==1); // @line: 52 call void$java.lang.RuntimeException$$la$init$ra$$761((r097), (r198)); return; } // @line: 233 // procedure void$javaUtilEx.AbstractList$clear$2491(__this : ref) returns ($Exep0 : ref) requires ($neref((__this), ($null))==1); { var r0142 : ref; var $i0144 : int; //temp local variables var $caughtEx1 : ref; // @line: 233 Block209: $caughtEx1 := $null; $Exep0 := $null; goto Block210; Block210: r0142 := __this; assert ($neref((r0142), ($null))==1); // @line: 234 call $i0144 := int$javaUtilEx.AbstractCollection$size$2230((r0142)); assert ($neref((r0142), ($null))==1); // @line: 234 call $caughtEx1 := void$javaUtilEx.AbstractList$removeRange$2499((r0142), (0), ($i0144)); goto Block211, Block213; Block211: assume ($neref(($caughtEx1), ($null))==1); goto Block212; Block213: assume ($eqref(($caughtEx1), ($null))==1); goto Block214; Block212: $Exep0 := $caughtEx1; return; Block214: return; } // @line: 616 // procedure int$javaUtilEx.SubList$access$200$2567($param_0 : ref) returns (__ret : int) { var $i0422 : int; var r0421 : ref; Block679: r0421 := $param_0; assert ($neref((r0421), ($null))==1); // @line: 617 $i0422 := $HeapVar[r0421, int$javaUtilEx.SubList$size0]; // @line: 617 __ret := $i0422; return; } // @line: 65 // ()> procedure void$javaUtilEx.AbstractCollection$$la$init$ra$$2228(__this : ref) requires ($neref((__this), ($null))==1); { var r01 : ref; Block16: r01 := __this; assert ($neref((r01), ($null))==1); // @line: 66 call void$java.lang.Object$$la$init$ra$$28((r01)); return; } // @line: 41 // ()> procedure void$javaUtilEx.UnsupportedOperationException$$la$init$ra$$2257(__this : ref) requires ($neref((__this), ($null))==1); { var r096 : ref; Block134: r096 := __this; assert ($neref((r096), ($null))==1); // @line: 42 call void$java.lang.RuntimeException$$la$init$ra$$760((r096)); return; } // @line: 54 // (java.lang.String)> procedure void$javaUtilEx.IllegalStateException$$la$init$ra$$2575(__this : ref, $param_0 : ref) requires ($neref((__this), ($null))==1); { var r0436 : ref; var r1437 : ref; Block687: r0436 := __this; r1437 := $param_0; assert ($neref((r0436), ($null))==1); // @line: 55 call void$java.lang.RuntimeException$$la$init$ra$$761((r0436), (r1437)); return; } // @line: 587 // procedure boolean$javaUtilEx.LinkedList$removeLastOccurrence$2663(__this : ref, $param_0 : ref) returns (__ret : int, $Exep0 : ref) requires ($neref((__this), ($null))==1); { var r11718 : ref; var r1705 : ref; var $r8715 : ref; var $r6713 : ref; var r0706 : ref; var r10717 : ref; var $r7714 : ref; var $r4710 : ref; var $z0711 : int; var $r2707 : ref; var $r3709 : ref; //temp local variables var $caughtEx1 : ref; var $freshlocal3 : ref; var $freshlocal2 : ref; // @line: 587 Block758: $caughtEx1 := $null; $Exep0 := $null; goto Block1073; Block1073: r0706 := __this; r1705 := $param_0; goto Block1074; // @line: 588 Block1074: goto Block1077, Block1075; // @line: 588 Block1077: // @line: 588 assume ($negInt(($neref((r1705), ($null))))==1); assert ($neref((r0706), ($null))==1); // @line: 589 $r6713 := $HeapVar[r0706, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$header298]; assert ($neref(($r6713), ($null))==1); // @line: 589 r10717 := $HeapVar[$r6713, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$previous302]; goto Block1078; // @line: 588 Block1075: assume ($neref((r1705), ($null))==1); goto Block1076; // @line: 589 Block1078: assert ($neref((r0706), ($null))==1); // @line: 589 $r7714 := $HeapVar[r0706, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$header298]; goto Block1079; // @line: 596 Block1076: assert ($neref((r0706), ($null))==1); // @line: 596 $r2707 := $HeapVar[r0706, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$header298]; goto Block1093; // @line: 589 Block1079: goto Block1080, Block1082; // @line: 596 Block1093: assert ($neref(($r2707), ($null))==1); // @line: 596 r11718 := $HeapVar[$r2707, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$previous302]; goto Block1094; // @line: 589 Block1080: assume ($eqref((r10717), ($r7714))==1); goto Block1081; // @line: 589 Block1082: // @line: 589 assume ($negInt(($eqref((r10717), ($r7714))))==1); assert ($neref((r10717), ($null))==1); // @line: 590 $r8715 := $HeapVar[r10717, java.lang.Object$javaUtilEx.LinkedList$Entry$element300]; goto Block1083; // @line: 596 Block1094: assert ($neref((r0706), ($null))==1); // @line: 596 $r3709 := $HeapVar[r0706, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$header298]; goto Block1095; // @line: 589 Block1081: goto Block1092; // @line: 590 Block1083: goto Block1084, Block1086; // @line: 596 Block1095: goto Block1096, Block1097; // @line: 603 Block1092: // @line: 603 __ret := 0; return; // @line: 590 Block1084: assume ($neref(($r8715), ($null))==1); goto Block1085; // @line: 590 Block1086: // @line: 590 assume ($negInt(($neref(($r8715), ($null))))==1); assert ($neref((r0706), ($null))==1); // @line: 591 call $freshlocal2, $caughtEx1 := java.lang.Object$javaUtilEx.LinkedList$remove$2666((r0706), (r10717)); goto Block1087, Block1089; // @line: 596 Block1096: assume ($eqref((r11718), ($r3709))==1); goto Block1092; // @line: 596 Block1097: // @line: 596 assume ($negInt(($eqref((r11718), ($r3709))))==1); assert ($neref((r11718), ($null))==1); // @line: 597 $r4710 := $HeapVar[r11718, java.lang.Object$javaUtilEx.LinkedList$Entry$element300]; assert ($neref((r1705), ($null))==1); // @line: 597 call $z0711 := boolean$java.lang.Object$equals$32((r1705), ($r4710)); goto Block1098; // @line: 589 Block1085: assert ($neref((r10717), ($null))==1); // @line: 589 r10717 := $HeapVar[r10717, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$previous302]; goto Block1091; // @line: 590 Block1087: assume ($neref(($caughtEx1), ($null))==1); goto Block1088; // @line: 590 Block1089: assume ($eqref(($caughtEx1), ($null))==1); goto Block1090; // @line: 597 Block1098: goto Block1101, Block1099; // @line: 589 Block1091: goto Block1078; // @line: 590 Block1088: $Exep0 := $caughtEx1; return; // @line: 590 Block1090: // @line: 592 __ret := 1; return; // @line: 597 Block1101: // @line: 597 assume ($negInt(($eqint(($z0711), (0))))==1); assert ($neref((r0706), ($null))==1); // @line: 598 call $freshlocal3, $caughtEx1 := java.lang.Object$javaUtilEx.LinkedList$remove$2666((r0706), (r11718)); goto Block1102, Block1104; // @line: 597 Block1099: assume ($eqint(($z0711), (0))==1); goto Block1100; // @line: 597 Block1102: assume ($neref(($caughtEx1), ($null))==1); goto Block1103; // @line: 597 Block1104: assume ($eqref(($caughtEx1), ($null))==1); goto Block1105; // @line: 596 Block1100: assert ($neref((r11718), ($null))==1); // @line: 596 r11718 := $HeapVar[r11718, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$previous302]; goto Block1106; // @line: 597 Block1103: $Exep0 := $caughtEx1; return; // @line: 597 Block1105: // @line: 599 __ret := 1; return; // @line: 596 Block1106: goto Block1094; } // @line: 635 // procedure java.lang.Object$javaUtilEx.SubList$set$2550(__this : ref, $param_0 : int, $param_1 : ref) returns (__ret : ref, $Exep1 : ref, $Exep0 : ref, $Exep2 : ref) requires ($neref((__this), ($null))==1); { var r1328 : ref; var $i1327 : int; var $r3331 : ref; var r0325 : ref; var $i2329 : int; var $r2330 : ref; var i0326 : int; //temp local variables var $caughtEx5 : ref; var $caughtEx3 : ref; var $caughtEx4 : ref; // @line: 635 Block507: $caughtEx5 := $null; $caughtEx4 := $null; $caughtEx3 := $null; $Exep2 := $null; $Exep1 := $null; $Exep0 := $null; goto Block509; Block509: r0325 := __this; i0326 := $param_0; r1328 := $param_1; assert ($neref((r0325), ($null))==1); // @line: 636 call $caughtEx3 := void$javaUtilEx.SubList$rangeCheck$2561((r0325), (i0326)); goto Block510, Block512; Block510: assume ($neref(($caughtEx3), ($null))==1); goto Block511; Block512: assume ($eqref(($caughtEx3), ($null))==1); goto Block513; Block511: $Exep0 := $caughtEx3; return; Block513: assert ($neref((r0325), ($null))==1); // @line: 637 call $caughtEx4 := void$javaUtilEx.SubList$checkForComodification$2564((r0325)); goto Block514, Block516; Block514: assume ($neref(($caughtEx4), ($null))==1); goto Block515; Block516: assume ($eqref(($caughtEx4), ($null))==1); goto Block517; Block515: $Exep1 := $caughtEx4; return; Block517: assert ($neref((r0325), ($null))==1); // @line: 638 $r2330 := $HeapVar[r0325, javaUtilEx.AbstractList$javaUtilEx.SubList$l297]; assert ($neref((r0325), ($null))==1); // @line: 638 $i1327 := $HeapVar[r0325, int$javaUtilEx.SubList$offset0]; // @line: 638 $i2329 := $addint((i0326), ($i1327)); assert ($neref(($r2330), ($null))==1); // @line: 638 call $r3331, $caughtEx5 := java.lang.Object$javaUtilEx.AbstractList$set$2486(($r2330), ($i2329), (r1328)); goto Block518, Block520; Block518: assume ($neref(($caughtEx5), ($null))==1); goto Block519; Block520: assume ($eqref(($caughtEx5), ($null))==1); goto Block521; Block519: $Exep2 := $caughtEx5; return; Block521: // @line: 638 __ret := $r3331; return; } // @line: 385 // procedure void$javaUtilEx.AbstractList$Itr$checkForComodification$2538(__this : ref) returns ($Exep0 : ref) requires ($neref((__this), ($null))==1); { var r0253 : ref; var $r1254 : ref; var $i1256 : int; var $i0255 : int; var $r2257 : ref; //temp local variables // @line: 385 Block354: $Exep0 := $null; goto Block396; Block396: r0253 := __this; assert ($neref((r0253), ($null))==1); // @line: 386 $r1254 := $HeapVar[r0253, javaUtilEx.AbstractList$javaUtilEx.AbstractList$Itr$this$0295]; assert ($neref(($r1254), ($null))==1); // @line: 386 $i1256 := $HeapVar[$r1254, int$javaUtilEx.AbstractList$modCount0]; assert ($neref((r0253), ($null))==1); // @line: 386 $i0255 := $HeapVar[r0253, int$javaUtilEx.AbstractList$Itr$expectedModCount0]; goto Block397; // @line: 386 Block397: goto Block400, Block398; // @line: 386 Block400: // @line: 386 assume ($negInt(($eqint(($i1256), ($i0255))))==1); // @line: 387 $r2257 := $newvariable((401)); assume ($neref(($newvariable((401))), ($null))==1); assert ($neref(($r2257), ($null))==1); // @line: 387 call void$javaUtilEx.ConcurrentModificationException$$la$init$ra$$2570(($r2257)); goto Block402; // @line: 386 Block398: assume ($eqint(($i1256), ($i0255))==1); goto Block399; // @line: 386 Block402: $Exep0 := $r2257; return; // @line: 388 Block399: return; } // procedure is generated by joogie. function {:inline true} $eqrefarray($param00 : [int]ref, $param11 : [int]ref) returns (__ret : int); // @line: 434 // procedure void$javaUtilEx.AbstractList$ListItr$add$2548(__this : ref, $param_0 : ref) returns ($Exep0 : ref, $Exep1 : ref) modifies $HeapVar; requires ($neref((__this), ($null))==1); { var r1305 : ref; var i2312 : int; var $i0307 : int; var $r2306 : ref; var $r3308 : ref; var r0303 : ref; var $i1309 : int; var $r4310 : ref; var $r5311 : ref; //temp local variables var $caughtEx2 : ref; var $caughtEx4 : ref; var $caughtEx3 : ref; // @line: 434 Block470: $caughtEx4 := $null; $caughtEx3 := $null; $caughtEx2 := $null; $Exep1 := $null; $Exep0 := $null; goto Block471; Block471: r0303 := __this; r1305 := $param_0; assert ($neref((r0303), ($null))==1); // @line: 435 call $caughtEx2 := void$javaUtilEx.AbstractList$Itr$checkForComodification$2538((r0303)); goto Block472, Block474; Block472: assume ($neref(($caughtEx2), ($null))==1); goto Block473; Block474: assume ($eqref(($caughtEx2), ($null))==1); goto Block475; Block473: $Exep0 := $caughtEx2; return; Block475: goto Block476; // @line: 438 Block476: assert ($neref((r0303), ($null))==1); // @line: 438 i2312 := $HeapVar[r0303, int$javaUtilEx.AbstractList$Itr$cursor0]; assert ($neref((r0303), ($null))==1); // @line: 439 $r2306 := $HeapVar[r0303, javaUtilEx.AbstractList$javaUtilEx.AbstractList$ListItr$this$0296]; assert ($neref(($r2306), ($null))==1); // @line: 439 call $caughtEx3 := void$javaUtilEx.AbstractList$add$2487(($r2306), (i2312), (r1305)); goto Block477, Block479; // @line: 438 Block477: assume ($neref(($caughtEx3), ($null))==1); goto Block478; // @line: 438 Block479: assume ($eqref(($caughtEx3), ($null))==1); goto Block480; // @line: 438 Block478: $Exep1 := $caughtEx3; return; // @line: 438 Block480: assert ($neref((r0303), ($null))==1); // @line: 440 $HeapVar[r0303, int$javaUtilEx.AbstractList$Itr$lastRet0] := -1; // @line: 441 $i0307 := $addint((i2312), (1)); assert ($neref((r0303), ($null))==1); // @line: 441 $HeapVar[r0303, int$javaUtilEx.AbstractList$Itr$cursor0] := $i0307; assert ($neref((r0303), ($null))==1); // @line: 442 $r3308 := $HeapVar[r0303, javaUtilEx.AbstractList$javaUtilEx.AbstractList$ListItr$this$0296]; assert ($neref(($r3308), ($null))==1); // @line: 442 $i1309 := $HeapVar[$r3308, int$javaUtilEx.AbstractList$modCount0]; assert ($neref((r0303), ($null))==1); // @line: 442 $HeapVar[r0303, int$javaUtilEx.AbstractList$Itr$expectedModCount0] := $i1309; goto Block481; // @line: 445 Block481: goto Block482; // @line: 446 Block482: return; } // procedure java.lang.StringBuilder$java.lang.StringBuilder$append$2266(__this : ref, $param_0 : ref) returns (__ret : ref); // @line: 715 // procedure boolean$javaUtilEx.SubList$1$hasPrevious$2696(__this : ref) returns (__ret : int) requires ($neref((__this), ($null))==1); { var $i0923 : int; var $z0925 : int; var r0922 : ref; Block1322: r0922 := __this; assert ($neref((r0922), ($null))==1); // @line: 716 call $i0923 := int$javaUtilEx.SubList$1$previousIndex$2699((r0922)); goto Block1323; // @line: 716 Block1323: goto Block1326, Block1324; // @line: 716 Block1326: // @line: 716 assume ($negInt(($ltint(($i0923), (0))))==1); // @line: 716 $z0925 := 1; goto Block1327; // @line: 716 Block1324: assume ($ltint(($i0923), (0))==1); goto Block1325; // @line: 716 Block1327: // @line: 716 __ret := $z0925; return; // @line: 716 Block1325: // @line: 716 $z0925 := 0; goto Block1327; } // @line: 740 // procedure void$javaUtilEx.SubList$1$set$2701(__this : ref, $param_0 : ref) requires ($neref((__this), ($null))==1); { var r0951 : ref; var r1952 : ref; var $r2953 : ref; Block1340: r0951 := __this; r1952 := $param_0; assert ($neref((r0951), ($null))==1); // @line: 741 $r2953 := $HeapVar[r0951, javaUtilEx.ListIterator$javaUtilEx.SubList$1$i308]; assert ($neref(($r2953), ($null))==1); // @line: 741 call void$javaUtilEx.ListIterator$set$2532(($r2953), (r1952)); return; } // procedure is generated by joogie. function {:inline true} $shrref($param00 : ref, $param11 : ref) returns (__ret : int); // @line: 325 // procedure javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$entry$2646(__this : ref, $param_0 : int) returns (__ret : ref, $Exep0 : ref) requires ($neref((__this), ($null))==1); { var $i2635 : int; var i4639 : int; var r2638 : ref; var r0632 : ref; var $i1633 : int; var $i3636 : int; var i5640 : int; var $r1631 : ref; var i0630 : int; //temp local variables // @line: 325 Block754: $Exep0 := $null; goto Block903; Block903: r0632 := __this; i0630 := $param_0; goto Block904; // @line: 326 Block904: goto Block907, Block905; // @line: 326 Block907: // @line: 326 assume ($negInt(($ltint((i0630), (0))))==1); assert ($neref((r0632), ($null))==1); // @line: 327 $i1633 := $HeapVar[r0632, int$javaUtilEx.LinkedList$size0]; goto Block908; // @line: 326 Block905: assume ($ltint((i0630), (0))==1); goto Block906; // @line: 327 Block908: goto Block911, Block909; // @line: 327 Block906: // @line: 327 $r1631 := $newvariable((912)); assume ($neref(($newvariable((912))), ($null))==1); assert ($neref(($r1631), ($null))==1); // @line: 327 call void$java.lang.IndexOutOfBoundsException$$la$init$ra$$2075(($r1631)); goto Block913; // @line: 327 Block911: // @line: 327 assume ($negInt(($ltint((i0630), ($i1633))))==1); goto Block906; // @line: 327 Block909: assume ($ltint((i0630), ($i1633))==1); goto Block910; // @line: 327 Block913: $Exep0 := $r1631; return; // @line: 328 Block910: assert ($neref((r0632), ($null))==1); // @line: 328 r2638 := $HeapVar[r0632, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$header298]; goto Block914; // @line: 329 Block914: assert ($neref((r0632), ($null))==1); // @line: 329 $i2635 := $HeapVar[r0632, int$javaUtilEx.LinkedList$size0]; // @line: 329 $i3636 := $shrint(($i2635), (1)); goto Block915; // @line: 329 Block915: goto Block916, Block918; // @line: 329 Block916: assume ($geint((i0630), ($i3636))==1); goto Block917; // @line: 329 Block918: // @line: 329 assume ($negInt(($geint((i0630), ($i3636))))==1); // @line: 330 i4639 := 0; goto Block919; // @line: 333 Block917: assert ($neref((r0632), ($null))==1); // @line: 333 i5640 := $HeapVar[r0632, int$javaUtilEx.LinkedList$size0]; goto Block924; // @line: 330 Block919: goto Block922, Block920; // @line: 333 Block924: goto Block925, Block926; // @line: 330 Block922: // @line: 330 assume ($negInt(($gtint((i4639), (i0630))))==1); assert ($neref((r2638), ($null))==1); // @line: 331 r2638 := $HeapVar[r2638, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$next301]; // @line: 330 i4639 := $addint((i4639), (1)); goto Block919; // @line: 330 Block920: assume ($gtint((i4639), (i0630))==1); goto Block921; // @line: 333 Block925: assume ($leint((i5640), (i0630))==1); goto Block923; // @line: 333 Block926: // @line: 333 assume ($negInt(($leint((i5640), (i0630))))==1); assert ($neref((r2638), ($null))==1); // @line: 334 r2638 := $HeapVar[r2638, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$previous302]; // @line: 333 i5640 := $addint((i5640), (-1)); goto Block924; // @line: 330 Block921: goto Block923; // @line: 336 Block923: // @line: 336 __ret := r2638; return; } // procedure javaUtilEx.ListIterator$javaUtilEx.List$listIterator$2522(__this : ref) returns (__ret : ref); // @line: 299 // procedure javaUtilEx.ListIterator$javaUtilEx.AbstractList$listIterator$2494(__this : ref) returns (__ret : ref, $Exep0 : ref) requires ($neref((__this), ($null))==1); { var $r1159 : ref; var r0158 : ref; //temp local variables var $caughtEx1 : ref; // @line: 299 Block159: $caughtEx1 := $null; $Exep0 := $null; goto Block232; Block232: r0158 := __this; assert ($neref((r0158), ($null))==1); // @line: 300 call $r1159, $caughtEx1 := javaUtilEx.ListIterator$javaUtilEx.AbstractList$listIterator$2495((r0158), (0)); goto Block233, Block235; Block233: assume ($neref(($caughtEx1), ($null))==1); goto Block234; Block235: assume ($eqref(($caughtEx1), ($null))==1); goto Block236; Block234: $Exep0 := $caughtEx1; return; Block236: // @line: 300 __ret := $r1159; return; } // procedure is generated by joogie. function {:inline true} $geref($param00 : ref, $param11 : ref) returns (__ret : int); // @line: 726 // procedure int$javaUtilEx.SubList$1$nextIndex$2698(__this : ref) returns (__ret : int) requires ($neref((__this), ($null))==1); { var $i1935 : int; var $r2934 : ref; var $i2936 : int; var $r1932 : ref; var $i0933 : int; var r0931 : ref; Block1337: r0931 := __this; assert ($neref((r0931), ($null))==1); // @line: 727 $r1932 := $HeapVar[r0931, javaUtilEx.ListIterator$javaUtilEx.SubList$1$i308]; assert ($neref(($r1932), ($null))==1); // @line: 727 call $i0933 := int$javaUtilEx.ListIterator$nextIndex$2529(($r1932)); assert ($neref((r0931), ($null))==1); // @line: 727 $r2934 := $HeapVar[r0931, javaUtilEx.SubList$javaUtilEx.SubList$1$this$0309]; // @line: 727 call $i1935 := int$javaUtilEx.SubList$access$000$2565(($r2934)); // @line: 727 $i2936 := $subint(($i0933), ($i1935)); // @line: 727 __ret := $i2936; return; } // procedure is generated by joogie. function {:inline true} $eqint(x : int, y : int) returns (__ret : int) { if (x == y) then 1 else 0 } // @line: 763 // procedure javaUtilEx.Iterator$javaUtilEx.LinkedList$descendingIterator$2667(__this : ref) returns (__ret : ref, $Exep0 : ref) requires ($neref((__this), ($null))==1); { var r0749 : ref; var $r1748 : ref; //temp local variables var $caughtEx1 : ref; // @line: 763 Block1127: $caughtEx1 := $null; $Exep0 := $null; goto Block1128; Block1128: r0749 := __this; // @line: 764 $r1748 := $newvariable((1129)); assume ($neref(($newvariable((1129))), ($null))==1); assert ($neref(($r1748), ($null))==1); // @line: 764 call $caughtEx1 := void$javaUtilEx.LinkedList$DescendingIterator$$la$init$ra$$2692(($r1748), (r0749), ($null)); goto Block1132, Block1130; Block1132: assume ($eqref(($caughtEx1), ($null))==1); goto Block1133; Block1130: assume ($neref(($caughtEx1), ($null))==1); goto Block1131; Block1133: // @line: 764 __ret := $r1748; return; Block1131: $Exep0 := $caughtEx1; return; } // @line: 452 // procedure boolean$javaUtilEx.LinkedList$offer$2653(__this : ref, $param_0 : ref) returns (__ret : int) requires ($neref((__this), ($null))==1); { var r0679 : ref; var $z0681 : int; var r1680 : ref; Block1013: r0679 := __this; r1680 := $param_0; assert ($neref((r0679), ($null))==1); // @line: 453 call $z0681 := boolean$javaUtilEx.LinkedList$add$2639((r0679), (r1680)); // @line: 453 __ret := $z0681; return; } // @line: 612 // procedure java.lang.String$javaUtilEx.AbstractList$outOfBoundsMsg$2501(__this : ref, $param_0 : int) returns (__ret : ref) modifies $stringSize; requires ($neref((__this), ($null))==1); { var r0216 : ref; var i0217 : int; Block346: r0216 := __this; i0217 := $param_0; $stringSize[$fresh2] := 0; // @line: 613 __ret := $fresh2; return; } // procedure is generated by joogie. function {:inline true} $instanceof($param00 : ref, $param11 : classConst) returns (__ret : int); // @line: 114 // procedure java.lang.Object$javaUtilEx.AbstractSequentialList$set$2580(__this : ref, $param_0 : int, $param_1 : ref) returns (__ret : ref, $Exep0 : ref) requires ($neref((__this), ($null))==1); { var r2456 : ref; var r1457 : ref; var r0451 : ref; var r5460 : ref; var $r4459 : ref; var i0452 : int; var $r3458 : ref; //temp local variables var $caughtEx1 : ref; // @line: 114 Block698: $caughtEx1 := $null; $Exep0 := $null; goto Block699; Block699: r0451 := __this; i0452 := $param_0; r1457 := $param_1; goto Block700; // @line: 115 Block700: assert ($neref((r0451), ($null))==1); // @line: 115 call r5460 := javaUtilEx.ListIterator$javaUtilEx.AbstractSequentialList$listIterator$2585((r0451), (i0452)); assert ($neref((r5460), ($null))==1); // @line: 116 call r2456 := java.lang.Object$javaUtilEx.ListIterator$next$2526((r5460)); assert ($neref((r5460), ($null))==1); // @line: 117 call void$javaUtilEx.ListIterator$set$2532((r5460), (r1457)); goto Block701; // @line: 118 Block701: // @line: 118 __ret := r2456; return; } // @line: 684 // procedure int$javaUtilEx.LinkedList$ListItr$previousIndex$2683(__this : ref) returns (__ret : int) requires ($neref((__this), ($null))==1); { var $i1843 : int; var r0841 : ref; var $i0842 : int; Block1220: r0841 := __this; assert ($neref((r0841), ($null))==1); // @line: 685 $i0842 := $HeapVar[r0841, int$javaUtilEx.LinkedList$ListItr$nextIndex0]; // @line: 685 $i1843 := $subint(($i0842), (1)); // @line: 685 __ret := $i1843; return; } // procedure is generated by joogie. function {:inline true} $gereal($param00 : realVar, $param11 : realVar) returns (__ret : int); // @line: 413 // procedure int$javaUtilEx.AbstractList$ListItr$nextIndex$2545(__this : ref) returns (__ret : int) requires ($neref((__this), ($null))==1); { var r0286 : ref; var $i0287 : int; Block446: r0286 := __this; assert ($neref((r0286), ($null))==1); // @line: 414 $i0287 := $HeapVar[r0286, int$javaUtilEx.AbstractList$Itr$cursor0]; // @line: 414 __ret := $i0287; return; } // @line: 169 // procedure void$javaUtilEx.LinkedList$addFirst$2635(__this : ref, $param_0 : ref) requires ($neref((__this), ($null))==1); { var r1564 : ref; var r0563 : ref; var $r3566 : ref; var $r2565 : ref; //temp local variables var $freshlocal0 : ref; Block818: r0563 := __this; r1564 := $param_0; assert ($neref((r0563), ($null))==1); // @line: 170 $r2565 := $HeapVar[r0563, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$header298]; assert ($neref(($r2565), ($null))==1); // @line: 170 $r3566 := $HeapVar[$r2565, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$next301]; assert ($neref((r0563), ($null))==1); // @line: 170 call $freshlocal0 := javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$addBefore$2665((r0563), (r1564), ($r3566)); return; } // @line: 464 // procedure boolean$javaUtilEx.LinkedList$offerFirst$2654(__this : ref, $param_0 : ref) returns (__ret : int) requires ($neref((__this), ($null))==1); { var r1683 : ref; var r0682 : ref; Block1014: r0682 := __this; r1683 := $param_0; assert ($neref((r0682), ($null))==1); // @line: 465 call void$javaUtilEx.LinkedList$addFirst$2635((r0682), (r1683)); // @line: 466 __ret := 1; return; } // @line: 160 // procedure java.lang.Object$javaUtilEx.LinkedList$removeLast$2634(__this : ref) returns (__ret : ref, $Exep0 : ref) requires ($neref((__this), ($null))==1); { var $r2561 : ref; var r0559 : ref; var $r3562 : ref; var $r1560 : ref; //temp local variables var $caughtEx1 : ref; // @line: 160 Block812: $caughtEx1 := $null; $Exep0 := $null; goto Block813; Block813: r0559 := __this; assert ($neref((r0559), ($null))==1); // @line: 161 $r1560 := $HeapVar[r0559, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$header298]; assert ($neref(($r1560), ($null))==1); // @line: 161 $r2561 := $HeapVar[$r1560, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$previous302]; assert ($neref((r0559), ($null))==1); // @line: 161 call $r3562, $caughtEx1 := java.lang.Object$javaUtilEx.LinkedList$remove$2666((r0559), ($r2561)); goto Block816, Block814; Block816: assume ($eqref(($caughtEx1), ($null))==1); goto Block817; Block814: assume ($neref(($caughtEx1), ($null))==1); goto Block815; Block817: // @line: 161 __ret := $r3562; return; Block815: $Exep0 := $caughtEx1; return; } // procedure is generated by joogie. function {:inline true} $andint($param00 : int, $param11 : int) returns (__ret : int); // @line: 44 // ()> procedure void$javaUtilEx.NoSuchElementException$$la$init$ra$$2572(__this : ref) requires ($neref((__this), ($null))==1); { var r0432 : ref; Block684: r0432 := __this; assert ($neref((r0432), ($null))==1); // @line: 45 call void$java.lang.RuntimeException$$la$init$ra$$760((r0432)); return; } // procedure is generated by joogie. function {:inline true} $shlint($param00 : int, $param11 : int) returns (__ret : int); // @line: 767 // (javaUtilEx.LinkedList)> procedure void$javaUtilEx.LinkedList$DescendingIterator$$la$init$ra$$2688(__this : ref, $param_0 : ref) returns ($Exep0 : ref) modifies $HeapVar; requires ($neref((__this), ($null))==1); { var r1885 : ref; var $r4888 : ref; var $i0889 : int; var r0884 : ref; var $r3887 : ref; var $r2886 : ref; //temp local variables var $caughtEx1 : ref; // @line: 767 Block1125: $caughtEx1 := $null; $Exep0 := $null; goto Block1270; Block1270: r0884 := __this; r1885 := $param_0; assert ($neref((r0884), ($null))==1); // @line: 768 $HeapVar[r0884, javaUtilEx.LinkedList$javaUtilEx.LinkedList$DescendingIterator$this$0307] := r1885; assert ($neref((r0884), ($null))==1); // @line: 768 call void$java.lang.Object$$la$init$ra$$28((r0884)); // @line: 769 $r2886 := $newvariable((1271)); assume ($neref(($newvariable((1271))), ($null))==1); assert ($neref((r0884), ($null))==1); // @line: 769 $r4888 := $HeapVar[r0884, javaUtilEx.LinkedList$javaUtilEx.LinkedList$DescendingIterator$this$0307]; assert ($neref((r0884), ($null))==1); // @line: 769 $r3887 := $HeapVar[r0884, javaUtilEx.LinkedList$javaUtilEx.LinkedList$DescendingIterator$this$0307]; assert ($neref(($r3887), ($null))==1); // @line: 769 call $i0889 := int$javaUtilEx.LinkedList$size$2638(($r3887)); assert ($neref(($r2886), ($null))==1); // @line: 769 call $caughtEx1 := void$javaUtilEx.LinkedList$ListItr$$la$init$ra$$2677(($r2886), ($r4888), ($i0889)); goto Block1274, Block1272; Block1274: assume ($eqref(($caughtEx1), ($null))==1); goto Block1275; Block1272: assume ($neref(($caughtEx1), ($null))==1); goto Block1273; Block1275: assert ($neref((r0884), ($null))==1); // @line: 769 $HeapVar[r0884, javaUtilEx.LinkedList$ListItr$javaUtilEx.LinkedList$DescendingIterator$itr306] := $r2886; return; Block1273: $Exep0 := $caughtEx1; return; } // procedure is generated by joogie. function {:inline true} $xorint($param00 : int, $param11 : int) returns (__ret : int); // @line: 616 // procedure int$javaUtilEx.SubList$access$208$2569($param_0 : ref) returns (__ret : int) modifies $HeapVar; { var $i1428 : int; var r0426 : ref; var $i0427 : int; Block681: r0426 := $param_0; assert ($neref((r0426), ($null))==1); // @line: 617 $i0427 := $HeapVar[r0426, int$javaUtilEx.SubList$size0]; // @line: 617 $i1428 := $addint(($i0427), (1)); assert ($neref((r0426), ($null))==1); // @line: 617 $HeapVar[r0426, int$javaUtilEx.SubList$size0] := $i1428; // @line: 617 __ret := $i0427; return; } // @line: 137 // procedure java.lang.Object$javaUtilEx.LinkedList$getLast$2632(__this : ref) returns (__ret : ref, $Exep0 : ref) requires ($neref((__this), ($null))==1); { var $r3553 : ref; var r0549 : ref; var $i0550 : int; var $r2552 : ref; var $r1551 : ref; var $r4554 : ref; //temp local variables // @line: 137 Block797: $Exep0 := $null; goto Block798; Block798: r0549 := __this; assert ($neref((r0549), ($null))==1); // @line: 138 $i0550 := $HeapVar[r0549, int$javaUtilEx.LinkedList$size0]; goto Block799; // @line: 138 Block799: goto Block802, Block800; // @line: 138 Block802: // @line: 138 assume ($negInt(($neint(($i0550), (0))))==1); // @line: 139 $r4554 := $newvariable((803)); assume ($neref(($newvariable((803))), ($null))==1); assert ($neref(($r4554), ($null))==1); // @line: 139 call void$javaUtilEx.NoSuchElementException$$la$init$ra$$2572(($r4554)); goto Block804; // @line: 138 Block800: assume ($neint(($i0550), (0))==1); goto Block801; // @line: 138 Block804: $Exep0 := $r4554; return; // @line: 141 Block801: assert ($neref((r0549), ($null))==1); // @line: 141 $r1551 := $HeapVar[r0549, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$header298]; goto Block805; // @line: 141 Block805: assert ($neref(($r1551), ($null))==1); // @line: 141 $r2552 := $HeapVar[$r1551, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$previous302]; assert ($neref(($r2552), ($null))==1); // @line: 141 $r3553 := $HeapVar[$r2552, java.lang.Object$javaUtilEx.LinkedList$Entry$element300]; // @line: 141 __ret := $r3553; return; } // procedure javaUtilEx.Iterator$javaUtilEx.Collection$iterator$2244(__this : ref) returns (__ret : ref); // procedure is generated by joogie. function {:inline true} $modreal($param00 : realVar, $param11 : realVar) returns (__ret : realVar); // @line: 193 // procedure boolean$javaUtilEx.LinkedList$contains$2637(__this : ref, $param_0 : ref) returns (__ret : int) requires ($neref((__this), ($null))==1); { var $z0576 : int; var r1573 : ref; var r0572 : ref; var $i0574 : int; Block820: r0572 := __this; r1573 := $param_0; assert ($neref((r0572), ($null))==1); // @line: 194 call $i0574 := int$javaUtilEx.LinkedList$indexOf$2647((r0572), (r1573)); goto Block821; // @line: 194 Block821: goto Block824, Block822; // @line: 194 Block824: // @line: 194 assume ($negInt(($eqint(($i0574), (-1))))==1); // @line: 194 $z0576 := 1; goto Block825; // @line: 194 Block822: assume ($eqint(($i0574), (-1))==1); goto Block823; // @line: 194 Block825: // @line: 194 __ret := $z0576; return; // @line: 194 Block823: // @line: 194 $z0576 := 0; goto Block825; } // @line: 2 // ()> procedure void$javaUtilEx.Random$$la$init$ra$$2673(__this : ref) requires ($neref((__this), ($null))==1); { var r0772 : ref; Block1150: r0772 := __this; assert ($neref((r0772), ($null))==1); // @line: 3 call void$java.lang.Object$$la$init$ra$$28((r0772)); return; } // @line: 627 // procedure javaUtilEx.ListIterator$javaUtilEx.LinkedList$listIterator$2664(__this : ref, $param_0 : int) returns (__ret : ref, $Exep0 : ref) requires ($neref((__this), ($null))==1); { var r0720 : ref; var $r1719 : ref; var i0721 : int; //temp local variables var $caughtEx1 : ref; // @line: 627 Block1108: $caughtEx1 := $null; $Exep0 := $null; goto Block1109; Block1109: r0720 := __this; i0721 := $param_0; // @line: 628 $r1719 := $newvariable((1110)); assume ($neref(($newvariable((1110))), ($null))==1); assert ($neref(($r1719), ($null))==1); // @line: 628 call $caughtEx1 := void$javaUtilEx.LinkedList$ListItr$$la$init$ra$$2677(($r1719), (r0720), (i0721)); goto Block1113, Block1111; Block1113: assume ($eqref(($caughtEx1), ($null))==1); goto Block1114; Block1111: assume ($neref(($caughtEx1), ($null))==1); goto Block1112; Block1114: // @line: 628 __ret := $r1719; return; Block1112: $Exep0 := $caughtEx1; return; } // procedure is generated by joogie. function {:inline true} $gtref($param00 : ref, $param11 : ref) returns (__ret : int); // @line: 666 // procedure boolean$javaUtilEx.LinkedList$ListItr$hasPrevious$2680(__this : ref) returns (__ret : int) requires ($neref((__this), ($null))==1); { var r0826 : ref; var $i0827 : int; var $z0829 : int; Block1200: r0826 := __this; assert ($neref((r0826), ($null))==1); // @line: 667 $i0827 := $HeapVar[r0826, int$javaUtilEx.LinkedList$ListItr$nextIndex0]; goto Block1201; // @line: 667 Block1201: goto Block1204, Block1202; // @line: 667 Block1204: // @line: 667 assume ($negInt(($eqint(($i0827), (0))))==1); // @line: 667 $z0829 := 1; goto Block1205; // @line: 667 Block1202: assume ($eqint(($i0827), (0))==1); goto Block1203; // @line: 667 Block1205: // @line: 667 __ret := $z0829; return; // @line: 667 Block1203: // @line: 667 $z0829 := 0; goto Block1205; } // @line: 319 // procedure java.lang.String$javaUtilEx.AbstractCollection$toString$2240(__this : ref) returns (__ret : ref) modifies $stringSize; requires ($neref((__this), ($null))==1); { var r1591 : ref; var $r1286 : ref; var $r778 : ref; var $r371 : ref; var $z181 : int; var $r1083 : ref; var r1692 : ref; var $r1793 : ref; var $r1387 : ref; var r1894 : ref; var $r982 : ref; var $r1488 : ref; var r066 : ref; var $z069 : int; var $r677 : ref; var $r879 : ref; var r1995 : ref; var $r1184 : ref; var r168 : ref; var $r573 : ref; var $r472 : ref; var r276 : ref; Block112: r066 := __this; assert ($neref((r066), ($null))==1); // @line: 320 call r168 := javaUtilEx.Iterator$javaUtilEx.AbstractCollection$iterator$2229((r066)); assert ($neref((r168), ($null))==1); // @line: 321 call $z069 := boolean$javaUtilEx.Iterator$hasNext$2254((r168)); goto Block113; // @line: 321 Block113: goto Block116, Block114; // @line: 321 Block116: // @line: 321 assume ($negInt(($neint(($z069), (0))))==1); $stringSize[$fresh1] := 2; // @line: 322 __ret := $fresh1; return; // @line: 321 Block114: assume ($neint(($z069), (0))==1); goto Block115; // @line: 324 Block115: $stringSize[$fresh2] := 0; // @line: 324 r1591 := $fresh2; goto Block117; // @line: 325 Block117: // @line: 325 $r371 := $newvariable((118)); assume ($neref(($newvariable((118))), ($null))==1); assert ($neref(($r371), ($null))==1); // @line: 325 call void$java.lang.StringBuilder$$la$init$ra$$2261(($r371)); assert ($neref(($r371), ($null))==1); // @line: 325 call $r472 := java.lang.StringBuilder$java.lang.StringBuilder$append$2266(($r371), (r1591)); $stringSize[$fresh3] := 1; assert ($neref(($r472), ($null))==1); // @line: 325 call $r573 := java.lang.StringBuilder$java.lang.StringBuilder$append$2266(($r472), ($fresh3)); assert ($neref(($r573), ($null))==1); // @line: 325 call r1692 := java.lang.String$java.lang.StringBuilder$toString$2299(($r573)); goto Block119; // @line: 327 Block119: assert ($neref((r168), ($null))==1); // @line: 327 call r276 := java.lang.Object$javaUtilEx.Iterator$next$2255((r168)); // @line: 328 $r677 := $newvariable((120)); assume ($neref(($newvariable((120))), ($null))==1); assert ($neref(($r677), ($null))==1); // @line: 328 call void$java.lang.StringBuilder$$la$init$ra$$2261(($r677)); assert ($neref(($r677), ($null))==1); // @line: 328 call $r778 := java.lang.StringBuilder$java.lang.StringBuilder$append$2266(($r677), (r1692)); goto Block121; // @line: 328 Block121: goto Block122, Block124; // @line: 328 Block122: assume ($neref((r276), (r066))==1); goto Block123; // @line: 328 Block124: // @line: 328 assume ($negInt(($neref((r276), (r066))))==1); $stringSize[$fresh4] := 17; // @line: 331 $r1793 := $fresh4; goto Block125; // @line: 331 Block123: // @line: 331 $r1793 := r276; goto Block125; // @line: 328 Block125: assert ($neref(($r778), ($null))==1); // @line: 328 call $r879 := java.lang.StringBuilder$java.lang.StringBuilder$append$2265(($r778), ($r1793)); goto Block126; // @line: 328 Block126: assert ($neref(($r879), ($null))==1); // @line: 328 call r1894 := java.lang.String$java.lang.StringBuilder$toString$2299(($r879)); assert ($neref((r168), ($null))==1); // @line: 329 call $z181 := boolean$javaUtilEx.Iterator$hasNext$2254((r168)); goto Block127; // @line: 329 Block127: goto Block128, Block130; // @line: 329 Block128: assume ($neint(($z181), (0))==1); goto Block129; // @line: 329 Block130: // @line: 329 assume ($negInt(($neint(($z181), (0))))==1); // @line: 330 $r1286 := $newvariable((131)); assume ($neref(($newvariable((131))), ($null))==1); assert ($neref(($r1286), ($null))==1); // @line: 330 call void$java.lang.StringBuilder$$la$init$ra$$2261(($r1286)); assert ($neref(($r1286), ($null))==1); // @line: 330 call $r1387 := java.lang.StringBuilder$java.lang.StringBuilder$append$2266(($r1286), (r1894)); $stringSize[$fresh5] := 1; assert ($neref(($r1387), ($null))==1); // @line: 330 call $r1488 := java.lang.StringBuilder$java.lang.StringBuilder$append$2266(($r1387), ($fresh5)); assert ($neref(($r1488), ($null))==1); // @line: 330 call r1995 := java.lang.String$java.lang.StringBuilder$toString$2299(($r1488)); // @line: 331 __ret := r1995; return; // @line: 333 Block129: // @line: 333 $r982 := $newvariable((132)); assume ($neref(($newvariable((132))), ($null))==1); goto Block133; // @line: 333 Block133: assert ($neref(($r982), ($null))==1); // @line: 333 call void$java.lang.StringBuilder$$la$init$ra$$2261(($r982)); assert ($neref(($r982), ($null))==1); // @line: 333 call $r1083 := java.lang.StringBuilder$java.lang.StringBuilder$append$2266(($r982), (r1894)); $stringSize[$fresh6] := 2; assert ($neref(($r1083), ($null))==1); // @line: 333 call $r1184 := java.lang.StringBuilder$java.lang.StringBuilder$append$2266(($r1083), ($fresh6)); assert ($neref(($r1184), ($null))==1); // @line: 333 call r1692 := java.lang.String$java.lang.StringBuilder$toString$2299(($r1184)); goto Block119; } // @line: 382 // procedure int$javaUtilEx.LinkedList$lastIndexOf$2648(__this : ref, $param_0 : ref) returns (__ret : int) requires ($neref((__this), ($null))==1); { var $r6664 : ref; var $r2658 : ref; var r1657 : ref; var $z0662 : int; var $r3660 : ref; var $r5663 : ref; var r0655 : ref; var i0666 : int; var $r7665 : ref; var r8667 : ref; var r9668 : ref; var $r4661 : ref; Block953: r0655 := __this; r1657 := $param_0; assert ($neref((r0655), ($null))==1); // @line: 383 i0666 := $HeapVar[r0655, int$javaUtilEx.LinkedList$size0]; goto Block954; // @line: 384 Block954: goto Block955, Block957; // @line: 384 Block955: assume ($neref((r1657), ($null))==1); goto Block956; // @line: 384 Block957: // @line: 384 assume ($negInt(($neref((r1657), ($null))))==1); assert ($neref((r0655), ($null))==1); // @line: 385 $r5663 := $HeapVar[r0655, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$header298]; assert ($neref(($r5663), ($null))==1); // @line: 385 r8667 := $HeapVar[$r5663, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$previous302]; goto Block958; // @line: 391 Block956: assert ($neref((r0655), ($null))==1); // @line: 391 $r2658 := $HeapVar[r0655, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$header298]; goto Block969; // @line: 385 Block958: assert ($neref((r0655), ($null))==1); // @line: 385 $r6664 := $HeapVar[r0655, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$header298]; goto Block959; // @line: 391 Block969: assert ($neref(($r2658), ($null))==1); // @line: 391 r9668 := $HeapVar[$r2658, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$previous302]; goto Block970; // @line: 385 Block959: goto Block962, Block960; // @line: 391 Block970: assert ($neref((r0655), ($null))==1); // @line: 391 $r3660 := $HeapVar[r0655, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$header298]; goto Block971; // @line: 385 Block962: // @line: 385 assume ($negInt(($eqref((r8667), ($r6664))))==1); // @line: 386 i0666 := $addint((i0666), (-1)); assert ($neref((r8667), ($null))==1); // @line: 387 $r7665 := $HeapVar[r8667, java.lang.Object$javaUtilEx.LinkedList$Entry$element300]; goto Block963; // @line: 385 Block960: assume ($eqref((r8667), ($r6664))==1); goto Block961; // @line: 391 Block971: goto Block973, Block972; // @line: 387 Block963: goto Block966, Block964; // @line: 385 Block961: goto Block968; // @line: 391 Block973: // @line: 391 assume ($negInt(($eqref((r9668), ($r3660))))==1); // @line: 392 i0666 := $addint((i0666), (-1)); assert ($neref((r9668), ($null))==1); // @line: 393 $r4661 := $HeapVar[r9668, java.lang.Object$javaUtilEx.LinkedList$Entry$element300]; assert ($neref((r1657), ($null))==1); // @line: 393 call $z0662 := boolean$java.lang.Object$equals$32((r1657), ($r4661)); goto Block974; // @line: 391 Block972: assume ($eqref((r9668), ($r3660))==1); goto Block968; // @line: 387 Block966: // @line: 387 assume ($negInt(($neref(($r7665), ($null))))==1); // @line: 388 __ret := i0666; return; // @line: 387 Block964: assume ($neref(($r7665), ($null))==1); goto Block965; // @line: 397 Block968: // @line: 397 __ret := -1; return; // @line: 393 Block974: goto Block975, Block977; // @line: 385 Block965: assert ($neref((r8667), ($null))==1); // @line: 385 r8667 := $HeapVar[r8667, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$previous302]; goto Block967; // @line: 393 Block975: assume ($eqint(($z0662), (0))==1); goto Block976; // @line: 393 Block977: // @line: 393 assume ($negInt(($eqint(($z0662), (0))))==1); // @line: 394 __ret := i0666; return; // @line: 385 Block967: goto Block958; // @line: 391 Block976: assert ($neref((r9668), ($null))==1); // @line: 391 r9668 := $HeapVar[r9668, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$previous302]; goto Block978; // @line: 391 Block978: goto Block970; } // @line: 15 // procedure javaUtilEx.LinkedList$javaUtilEx.juLinkedListCreateRemoveLastOccurrence$createList$2628($param_0 : int) returns (__ret : ref) { var $r1529 : ref; var $r2532 : ref; var i1534 : int; var r0530 : ref; var $i0533 : int; Block773: i1534 := $param_0; // @line: 16 $r1529 := $newvariable((774)); assume ($neref(($newvariable((774))), ($null))==1); assert ($neref(($r1529), ($null))==1); // @line: 16 call void$javaUtilEx.LinkedList$$la$init$ra$$2629(($r1529)); // @line: 16 r0530 := $r1529; goto Block775; // @line: 17 Block775: goto Block776, Block778; // @line: 17 Block776: assume ($leint((i1534), (0))==1); goto Block777; // @line: 17 Block778: // @line: 17 assume ($negInt(($leint((i1534), (0))))==1); // @line: 18 $r2532 := $newvariable((779)); assume ($neref(($newvariable((779))), ($null))==1); // @line: 18 call $i0533 := int$javaUtilEx.Random$random$2674(); assert ($neref(($r2532), ($null))==1); // @line: 18 call void$javaUtilEx.Content$$la$init$ra$$2586(($r2532), ($i0533)); assert ($neref((r0530), ($null))==1); // @line: 18 call void$javaUtilEx.LinkedList$addLast$2636((r0530), ($r2532)); // @line: 19 i1534 := $addint((i1534), (-1)); goto Block775; // @line: 21 Block777: // @line: 21 __ret := r0530; return; } // @line: 773 // procedure java.lang.Object$javaUtilEx.LinkedList$DescendingIterator$next$2690(__this : ref) returns (__ret : ref, $Exep1 : ref, $Exep0 : ref) requires ($neref((__this), ($null))==1); { var $r2895 : ref; var r0893 : ref; var $r1894 : ref; //temp local variables var $caughtEx3 : ref; var $caughtEx2 : ref; // @line: 773 Block1277: $caughtEx3 := $null; $caughtEx2 := $null; $Exep1 := $null; $Exep0 := $null; goto Block1278; Block1278: r0893 := __this; assert ($neref((r0893), ($null))==1); // @line: 774 $r1894 := $HeapVar[r0893, javaUtilEx.LinkedList$ListItr$javaUtilEx.LinkedList$DescendingIterator$itr306]; assert ($neref(($r1894), ($null))==1); // @line: 774 call $r2895, $caughtEx2, $caughtEx3 := java.lang.Object$javaUtilEx.LinkedList$ListItr$previous$2681(($r1894)); goto Block1281, Block1279; Block1281: assume ($eqref(($caughtEx2), ($null))==1); goto Block1282; Block1279: assume ($neref(($caughtEx2), ($null))==1); goto Block1280; Block1282: goto Block1283, Block1285; Block1280: $Exep1 := $caughtEx2; return; Block1283: assume ($neref(($caughtEx3), ($null))==1); goto Block1284; Block1285: assume ($eqref(($caughtEx3), ($null))==1); goto Block1286; Block1284: $Exep0 := $caughtEx3; return; Block1286: // @line: 774 __ret := $r2895; return; } // @line: 571 // procedure void$javaUtilEx.AbstractList$removeRange$2499(__this : ref, $param_0 : int, $param_1 : int) returns ($Exep0 : ref) requires ($neref((__this), ($null))==1); { var i3210 : int; var r0202 : ref; var r1205 : ref; var i1207 : int; var i0203 : int; var i2208 : int; //temp local variables var $freshlocal2 : ref; var $caughtEx1 : ref; // @line: 571 Block208: $caughtEx1 := $null; $Exep0 := $null; goto Block326; Block326: r0202 := __this; i0203 := $param_0; i1207 := $param_1; assert ($neref((r0202), ($null))==1); // @line: 572 call r1205, $caughtEx1 := javaUtilEx.ListIterator$javaUtilEx.AbstractList$listIterator$2495((r0202), (i0203)); goto Block327, Block329; Block327: assume ($neref(($caughtEx1), ($null))==1); goto Block328; Block329: assume ($eqref(($caughtEx1), ($null))==1); goto Block330; Block328: $Exep0 := $caughtEx1; return; Block330: // @line: 573 i3210 := 0; // @line: 573 i2208 := $subint((i1207), (i0203)); goto Block331; // @line: 573 Block331: goto Block332, Block334; // @line: 573 Block332: assume ($geint((i3210), (i2208))==1); goto Block333; // @line: 573 Block334: // @line: 573 assume ($negInt(($geint((i3210), (i2208))))==1); assert ($neref((r1205), ($null))==1); // @line: 574 call $freshlocal2 := java.lang.Object$javaUtilEx.ListIterator$next$2526((r1205)); assert ($neref((r1205), ($null))==1); // @line: 575 call void$javaUtilEx.ListIterator$remove$2531((r1205)); // @line: 573 i3210 := $addint((i3210), (1)); goto Block331; // @line: 577 Block333: return; } // @line: 271 // procedure boolean$javaUtilEx.AbstractCollection$retainAll$2238(__this : ref, $param_0 : ref) returns (__ret : int) requires ($neref((__this), ($null))==1); { var r255 : ref; var $z159 : int; var z260 : int; var r157 : ref; var $z056 : int; var $r358 : ref; var r053 : ref; Block97: r053 := __this; r157 := $param_0; // @line: 272 z260 := 0; assert ($neref((r053), ($null))==1); // @line: 273 call r255 := javaUtilEx.Iterator$javaUtilEx.AbstractCollection$iterator$2229((r053)); goto Block98; // @line: 274 Block98: assert ($neref((r255), ($null))==1); // @line: 274 call $z056 := boolean$javaUtilEx.Iterator$hasNext$2254((r255)); goto Block99; // @line: 274 Block99: goto Block102, Block100; // @line: 274 Block102: // @line: 274 assume ($negInt(($eqint(($z056), (0))))==1); assert ($neref((r255), ($null))==1); // @line: 275 call $r358 := java.lang.Object$javaUtilEx.Iterator$next$2255((r255)); assert ($neref((r157), ($null))==1); // @line: 275 call $z159 := boolean$javaUtilEx.Collection$contains$2243((r157), ($r358)); goto Block103; // @line: 274 Block100: assume ($eqint(($z056), (0))==1); goto Block101; // @line: 275 Block103: goto Block104, Block105; // @line: 280 Block101: // @line: 280 __ret := z260; return; // @line: 275 Block104: assume ($neint(($z159), (0))==1); goto Block98; // @line: 275 Block105: // @line: 275 assume ($negInt(($neint(($z159), (0))))==1); assert ($neref((r255), ($null))==1); // @line: 276 call void$javaUtilEx.Iterator$remove$2256((r255)); // @line: 277 z260 := 1; goto Block98; } // (java.lang.String)> procedure void$java.lang.RuntimeException$$la$init$ra$$761(__this : ref, $param_0 : ref); // @line: 289 // procedure java.lang.Object$javaUtilEx.LinkedList$set$2643(__this : ref, $param_0 : int, $param_1 : ref) returns (__ret : ref, $Exep0 : ref) modifies $HeapVar; requires ($neref((__this), ($null))==1); { var r1618 : ref; var r0613 : ref; var r2616 : ref; var r3617 : ref; var i0614 : int; //temp local variables var $caughtEx1 : ref; // @line: 289 Block875: $caughtEx1 := $null; $Exep0 := $null; goto Block876; Block876: r0613 := __this; i0614 := $param_0; r1618 := $param_1; assert ($neref((r0613), ($null))==1); // @line: 290 call r2616, $caughtEx1 := javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$entry$2646((r0613), (i0614)); goto Block877, Block879; Block877: assume ($neref(($caughtEx1), ($null))==1); goto Block878; Block879: assume ($eqref(($caughtEx1), ($null))==1); goto Block880; Block878: $Exep0 := $caughtEx1; return; Block880: assert ($neref((r2616), ($null))==1); // @line: 291 r3617 := $HeapVar[r2616, java.lang.Object$javaUtilEx.LinkedList$Entry$element300]; assert ($neref((r2616), ($null))==1); // @line: 292 $HeapVar[r2616, java.lang.Object$javaUtilEx.LinkedList$Entry$element300] := r1618; // @line: 293 __ret := r3617; return; } // procedure is generated by joogie. function {:inline true} $negReal($param00 : realVar) returns (__ret : int); // @line: 170 // procedure java.lang.Object$javaUtilEx.AbstractSequentialList$remove$2582(__this : ref, $param_0 : int) returns (__ret : ref, $Exep0 : ref) requires ($neref((__this), ($null))==1); { var r1474 : ref; var $r2475 : ref; var r0469 : ref; var r4477 : ref; var i0470 : int; var $r3476 : ref; //temp local variables var $caughtEx1 : ref; // @line: 170 Block713: $caughtEx1 := $null; $Exep0 := $null; goto Block714; Block714: r0469 := __this; i0470 := $param_0; goto Block715; // @line: 171 Block715: assert ($neref((r0469), ($null))==1); // @line: 171 call r4477 := javaUtilEx.ListIterator$javaUtilEx.AbstractSequentialList$listIterator$2585((r0469), (i0470)); assert ($neref((r4477), ($null))==1); // @line: 172 call r1474 := java.lang.Object$javaUtilEx.ListIterator$next$2526((r4477)); assert ($neref((r4477), ($null))==1); // @line: 173 call void$javaUtilEx.ListIterator$remove$2531((r4477)); goto Block716; // @line: 174 Block716: // @line: 174 __ret := r1474; return; } // @line: 744 // procedure void$javaUtilEx.SubList$1$add$2702(__this : ref, $param_0 : ref) modifies $HeapVar; requires ($neref((__this), ($null))==1); { var $r3957 : ref; var r0954 : ref; var $r4958 : ref; var r1955 : ref; var $r5959 : ref; var $r2956 : ref; var $i0960 : int; var $r6961 : ref; //temp local variables var $freshlocal0 : int; Block1341: r0954 := __this; r1955 := $param_0; assert ($neref((r0954), ($null))==1); // @line: 745 $r2956 := $HeapVar[r0954, javaUtilEx.ListIterator$javaUtilEx.SubList$1$i308]; assert ($neref(($r2956), ($null))==1); // @line: 745 call void$javaUtilEx.ListIterator$add$2533(($r2956), (r1955)); assert ($neref((r0954), ($null))==1); // @line: 746 $r4958 := $HeapVar[r0954, javaUtilEx.SubList$javaUtilEx.SubList$1$this$0309]; assert ($neref((r0954), ($null))==1); // @line: 746 $r3957 := $HeapVar[r0954, javaUtilEx.SubList$javaUtilEx.SubList$1$this$0309]; // @line: 746 call $r5959 := javaUtilEx.AbstractList$javaUtilEx.SubList$access$100$2566(($r3957)); assert ($neref(($r5959), ($null))==1); // @line: 746 $i0960 := $HeapVar[$r5959, int$javaUtilEx.AbstractList$modCount0]; assert ($neref(($r4958), ($null))==1); // @line: 746 $HeapVar[$r4958, int$javaUtilEx.AbstractList$modCount0] := $i0960; assert ($neref((r0954), ($null))==1); // @line: 747 $r6961 := $HeapVar[r0954, javaUtilEx.SubList$javaUtilEx.SubList$1$this$0309]; // @line: 747 call $freshlocal0 := int$javaUtilEx.SubList$access$208$2569(($r6961)); return; } // procedure is generated by joogie. function {:inline true} $refarrtoref($param00 : [int]ref) returns (__ret : ref); // procedure javaUtilEx.Iterator$javaUtilEx.AbstractCollection$iterator$2229(__this : ref) returns (__ret : ref); // @line: 777 // (javaUtilEx.AbstractList,int,int)> procedure void$javaUtilEx.RandomAccessSubList$$la$init$ra$$2540(__this : ref, $param_0 : ref, $param_1 : int, $param_2 : int) returns ($Exep1 : ref, $Exep0 : ref) requires ($neref((__this), ($null))==1); { var r0261 : ref; var i1264 : int; var r1262 : ref; var i0263 : int; //temp local variables var $caughtEx3 : ref; var $caughtEx2 : ref; // @line: 777 Block244: $caughtEx3 := $null; $caughtEx2 := $null; $Exep1 := $null; $Exep0 := $null; goto Block404; Block404: r0261 := __this; r1262 := $param_0; i0263 := $param_1; i1264 := $param_2; assert ($neref((r0261), ($null))==1); // @line: 778 call $caughtEx2, $caughtEx3 := void$javaUtilEx.SubList$$la$init$ra$$2549((r0261), (r1262), (i0263), (i1264)); goto Block405, Block407; Block405: assume ($neref(($caughtEx2), ($null))==1); goto Block406; Block407: assume ($eqref(($caughtEx2), ($null))==1); goto Block408; Block406: $Exep1 := $caughtEx2; return; Block408: goto Block409, Block411; Block409: assume ($neref(($caughtEx3), ($null))==1); goto Block410; Block411: assume ($eqref(($caughtEx3), ($null))==1); goto Block412; Block410: $Exep0 := $caughtEx3; return; Block412: return; } // @line: 417 // procedure int$javaUtilEx.AbstractList$ListItr$previousIndex$2546(__this : ref) returns (__ret : int) requires ($neref((__this), ($null))==1); { var r0288 : ref; var $i0289 : int; var $i1290 : int; Block447: r0288 := __this; assert ($neref((r0288), ($null))==1); // @line: 418 $i0289 := $HeapVar[r0288, int$javaUtilEx.AbstractList$Itr$cursor0]; // @line: 418 $i1290 := $subint(($i0289), (1)); // @line: 418 __ret := $i1290; return; } // procedure is generated by joogie. function {:inline true} $ltreal($param00 : realVar, $param11 : realVar) returns (__ret : int); // procedure void$javaUtilEx.Iterator$remove$2256(__this : ref); // @line: 400 // procedure java.lang.Object$javaUtilEx.AbstractList$ListItr$previous$2544(__this : ref) returns (__ret : ref, $Exep0 : ref, $Exep1 : ref) modifies $HeapVar; requires ($neref((__this), ($null))==1); { var $r2279 : ref; var $r4283 : ref; var $i0277 : int; var r1281 : ref; var r0276 : ref; var i1284 : int; var $r3282 : ref; //temp local variables var $caughtEx2 : ref; var $caughtEx3 : ref; // @line: 400 Block431: $caughtEx3 := $null; $caughtEx2 := $null; $Exep1 := $null; $Exep0 := $null; goto Block432; Block432: r0276 := __this; assert ($neref((r0276), ($null))==1); // @line: 401 call $caughtEx2 := void$javaUtilEx.AbstractList$Itr$checkForComodification$2538((r0276)); goto Block435, Block433; Block435: assume ($eqref(($caughtEx2), ($null))==1); goto Block436; Block433: assume ($neref(($caughtEx2), ($null))==1); goto Block434; Block436: goto Block437; Block434: $Exep0 := $caughtEx2; return; // @line: 403 Block437: assert ($neref((r0276), ($null))==1); // @line: 403 $i0277 := $HeapVar[r0276, int$javaUtilEx.AbstractList$Itr$cursor0]; // @line: 403 i1284 := $subint(($i0277), (1)); assert ($neref((r0276), ($null))==1); // @line: 404 $r2279 := $HeapVar[r0276, javaUtilEx.AbstractList$javaUtilEx.AbstractList$ListItr$this$0296]; assert ($neref(($r2279), ($null))==1); // @line: 404 call r1281 := java.lang.Object$javaUtilEx.AbstractList$get$2485(($r2279), (i1284)); assert ($neref((r0276), ($null))==1); // @line: 405 $HeapVar[r0276, int$javaUtilEx.AbstractList$Itr$cursor0] := i1284; assert ($neref((r0276), ($null))==1); // @line: 405 $HeapVar[r0276, int$javaUtilEx.AbstractList$Itr$lastRet0] := i1284; goto Block438; // @line: 406 Block438: // @line: 406 __ret := r1281; return; } // procedure is generated by joogie. function {:inline true} $addref($param00 : ref, $param11 : ref) returns (__ret : ref); // @line: 647 // procedure int$javaUtilEx.SubList$size$2552(__this : ref) returns (__ret : int, $Exep0 : ref) requires ($neref((__this), ($null))==1); { var $i0339 : int; var r0338 : ref; //temp local variables var $caughtEx1 : ref; // @line: 647 Block532: $caughtEx1 := $null; $Exep0 := $null; goto Block533; Block533: r0338 := __this; assert ($neref((r0338), ($null))==1); // @line: 648 call $caughtEx1 := void$javaUtilEx.SubList$checkForComodification$2564((r0338)); goto Block536, Block534; Block536: assume ($eqref(($caughtEx1), ($null))==1); goto Block537; Block534: assume ($neref(($caughtEx1), ($null))==1); goto Block535; Block537: assert ($neref((r0338), ($null))==1); // @line: 649 $i0339 := $HeapVar[r0338, int$javaUtilEx.SubList$size0]; // @line: 649 __ret := $i0339; return; Block535: $Exep0 := $caughtEx1; return; } // @line: 407 // procedure java.lang.Object$javaUtilEx.LinkedList$peek$2649(__this : ref) returns (__ret : ref, $Exep0 : ref) requires ($neref((__this), ($null))==1); { var r0669 : ref; var $i0670 : int; var $r1671 : ref; //temp local variables var $caughtEx1 : ref; // @line: 407 Block979: $caughtEx1 := $null; $Exep0 := $null; goto Block980; Block980: r0669 := __this; assert ($neref((r0669), ($null))==1); // @line: 408 $i0670 := $HeapVar[r0669, int$javaUtilEx.LinkedList$size0]; goto Block981; // @line: 408 Block981: goto Block984, Block982; // @line: 408 Block984: // @line: 408 assume ($negInt(($neint(($i0670), (0))))==1); // @line: 409 __ret := $null; return; // @line: 408 Block982: assume ($neint(($i0670), (0))==1); goto Block983; // @line: 410 Block983: assert ($neref((r0669), ($null))==1); // @line: 410 call $r1671, $caughtEx1 := java.lang.Object$javaUtilEx.LinkedList$getFirst$2631((r0669)); goto Block987, Block985; // @line: 410 Block987: assume ($eqref(($caughtEx1), ($null))==1); goto Block988; // @line: 410 Block985: assume ($neref(($caughtEx1), ($null))==1); goto Block986; // @line: 410 Block988: goto Block989; // @line: 410 Block986: $Exep0 := $caughtEx1; return; // @line: 410 Block989: // @line: 410 __ret := $r1671; return; } // @line: 42 // ()> procedure void$javaUtilEx.IllegalArgumentException$$la$init$ra$$2622(__this : ref) requires ($neref((__this), ($null))==1); { var r0508 : ref; Block749: r0508 := __this; assert ($neref((r0508), ($null))==1); // @line: 43 call void$java.lang.RuntimeException$$la$init$ra$$760((r0508)); return; } // @line: 256 // procedure boolean$javaUtilEx.AbstractList$addAll$2492(__this : ref, $param_0 : int, $param_1 : ref) returns (__ret : int, $Exep0 : ref, $Exep1 : ref) requires ($neref((__this), ($null))==1); { var i1154 : int; var z1155 : int; var $i0152 : int; var r0145 : ref; var $z0151 : int; var $r3153 : ref; var r1148 : ref; var r2150 : ref; //temp local variables var $caughtEx3 : ref; var $caughtEx2 : ref; // @line: 256 Block215: $caughtEx3 := $null; $caughtEx2 := $null; $Exep1 := $null; $Exep0 := $null; goto Block216; Block216: r0145 := __this; i1154 := $param_0; r1148 := $param_1; assert ($neref((r0145), ($null))==1); // @line: 257 call $caughtEx2 := void$javaUtilEx.AbstractList$rangeCheckForAdd$2500((r0145), (i1154)); goto Block219, Block217; Block219: assume ($eqref(($caughtEx2), ($null))==1); goto Block220; Block217: assume ($neref(($caughtEx2), ($null))==1); goto Block218; Block220: // @line: 258 z1155 := 0; assert ($neref((r1148), ($null))==1); // @line: 259 call r2150 := javaUtilEx.Iterator$javaUtilEx.Collection$iterator$2244((r1148)); goto Block221; Block218: $Exep0 := $caughtEx2; return; // @line: 260 Block221: assert ($neref((r2150), ($null))==1); // @line: 260 call $z0151 := boolean$javaUtilEx.Iterator$hasNext$2254((r2150)); goto Block222; // @line: 260 Block222: goto Block225, Block223; // @line: 260 Block225: // @line: 260 assume ($negInt(($eqint(($z0151), (0))))==1); // @line: 261 $i0152 := i1154; // @line: 261 i1154 := $addint((i1154), (1)); assert ($neref((r2150), ($null))==1); // @line: 261 call $r3153 := java.lang.Object$javaUtilEx.Iterator$next$2255((r2150)); assert ($neref((r0145), ($null))==1); // @line: 261 call $caughtEx3 := void$javaUtilEx.AbstractList$add$2487((r0145), ($i0152), ($r3153)); goto Block226, Block228; // @line: 260 Block223: assume ($eqint(($z0151), (0))==1); goto Block224; // @line: 260 Block226: assume ($neref(($caughtEx3), ($null))==1); goto Block227; // @line: 260 Block228: assume ($eqref(($caughtEx3), ($null))==1); goto Block229; // @line: 264 Block224: // @line: 264 __ret := z1155; return; // @line: 260 Block227: $Exep1 := $caughtEx3; return; // @line: 260 Block229: // @line: 262 z1155 := 1; goto Block221; } // procedure is generated by joogie. function {:inline true} $addreal($param00 : realVar, $param11 : realVar) returns (__ret : realVar); // procedure is generated by joogie. function {:inline true} $gtreal($param00 : realVar, $param11 : realVar) returns (__ret : int); // procedure int$java.lang.Object$hashCode$31(__this : ref) returns (__ret : int); // ()> procedure void$java.lang.IndexOutOfBoundsException$$la$init$ra$$2075(__this : ref); // @line: 369 // procedure void$javaUtilEx.AbstractList$Itr$remove$2537(__this : ref) returns ($Exep1 : ref, $Exep0 : ref, $Exep2 : ref) modifies $HeapVar; requires ($neref((__this), ($null))==1); { var r0238 : ref; var $i1240 : int; var $i2243 : int; var $i0239 : int; var $r6250 : ref; var $r7252 : ref; var $r2241 : ref; var $i5247 : int; var $i4246 : int; var $i3244 : int; var $r4245 : ref; var $r5249 : ref; var $i6248 : int; //temp local variables var $freshlocal5 : ref; var $caughtEx4 : ref; var $caughtEx6 : ref; var $caughtEx3 : ref; // @line: 369 Block370: $caughtEx6 := $null; $caughtEx4 := $null; $caughtEx3 := $null; $Exep2 := $null; $Exep1 := $null; $Exep0 := $null; goto Block371; Block371: r0238 := __this; assert ($neref((r0238), ($null))==1); // @line: 370 $i0239 := $HeapVar[r0238, int$javaUtilEx.AbstractList$Itr$lastRet0]; goto Block372; // @line: 370 Block372: goto Block373, Block375; // @line: 370 Block373: assume ($geint(($i0239), (0))==1); goto Block374; // @line: 370 Block375: // @line: 370 assume ($negInt(($geint(($i0239), (0))))==1); // @line: 371 $r5249 := $newvariable((376)); assume ($neref(($newvariable((376))), ($null))==1); assert ($neref(($r5249), ($null))==1); // @line: 371 call void$javaUtilEx.IllegalStateException$$la$init$ra$$2574(($r5249)); goto Block377; // @line: 372 Block374: assert ($neref((r0238), ($null))==1); // @line: 372 call $caughtEx3 := void$javaUtilEx.AbstractList$Itr$checkForComodification$2538((r0238)); goto Block378, Block380; // @line: 370 Block377: $Exep0 := $r5249; return; // @line: 372 Block378: assume ($neref(($caughtEx3), ($null))==1); goto Block379; // @line: 372 Block380: assume ($eqref(($caughtEx3), ($null))==1); goto Block381; // @line: 372 Block379: $Exep1 := $caughtEx3; return; // @line: 372 Block381: goto Block382; // @line: 375 Block382: assert ($neref((r0238), ($null))==1); // @line: 375 $r2241 := $HeapVar[r0238, javaUtilEx.AbstractList$javaUtilEx.AbstractList$Itr$this$0295]; assert ($neref((r0238), ($null))==1); // @line: 375 $i1240 := $HeapVar[r0238, int$javaUtilEx.AbstractList$Itr$lastRet0]; assert ($neref(($r2241), ($null))==1); // @line: 375 call $freshlocal5, $caughtEx4 := java.lang.Object$javaUtilEx.AbstractList$remove$2488(($r2241), ($i1240)); goto Block385, Block383; // @line: 375 Block385: assume ($eqref(($caughtEx4), ($null))==1); goto Block386; // @line: 375 Block383: assume ($neref(($caughtEx4), ($null))==1); goto Block384; // @line: 375 Block386: assert ($neref((r0238), ($null))==1); // @line: 376 $i3244 := $HeapVar[r0238, int$javaUtilEx.AbstractList$Itr$lastRet0]; assert ($neref((r0238), ($null))==1); // @line: 376 $i2243 := $HeapVar[r0238, int$javaUtilEx.AbstractList$Itr$cursor0]; goto Block387; // @line: 375 Block384: $Exep2 := $caughtEx4; return; // @line: 376 Block387: goto Block390, Block388; // @line: 376 Block390: // @line: 376 assume ($negInt(($geint(($i3244), ($i2243))))==1); assert ($neref((r0238), ($null))==1); // @line: 377 $i5247 := $HeapVar[r0238, int$javaUtilEx.AbstractList$Itr$cursor0]; // @line: 377 $i6248 := $subint(($i5247), (1)); assert ($neref((r0238), ($null))==1); // @line: 377 $HeapVar[r0238, int$javaUtilEx.AbstractList$Itr$cursor0] := $i6248; goto Block389; // @line: 376 Block388: assume ($geint(($i3244), ($i2243))==1); goto Block389; // @line: 378 Block389: assert ($neref((r0238), ($null))==1); // @line: 378 $HeapVar[r0238, int$javaUtilEx.AbstractList$Itr$lastRet0] := -1; assert ($neref((r0238), ($null))==1); // @line: 379 $r4245 := $HeapVar[r0238, javaUtilEx.AbstractList$javaUtilEx.AbstractList$Itr$this$0295]; assert ($neref(($r4245), ($null))==1); // @line: 379 $i4246 := $HeapVar[$r4245, int$javaUtilEx.AbstractList$modCount0]; assert ($neref((r0238), ($null))==1); // @line: 379 $HeapVar[r0238, int$javaUtilEx.AbstractList$Itr$expectedModCount0] := $i4246; goto Block391; // @line: 382 Block391: goto Block392; // @line: 383 Block392: return; } // @line: 441 // procedure java.lang.Object$javaUtilEx.LinkedList$remove$2652(__this : ref) returns (__ret : ref, $Exep0 : ref) requires ($neref((__this), ($null))==1); { var r0677 : ref; var $r1678 : ref; //temp local variables var $caughtEx1 : ref; // @line: 441 Block1007: $caughtEx1 := $null; $Exep0 := $null; goto Block1008; Block1008: r0677 := __this; assert ($neref((r0677), ($null))==1); // @line: 442 call $r1678, $caughtEx1 := java.lang.Object$javaUtilEx.LinkedList$removeFirst$2633((r0677)); goto Block1011, Block1009; Block1011: assume ($eqref(($caughtEx1), ($null))==1); goto Block1012; Block1009: assume ($neref(($caughtEx1), ($null))==1); goto Block1010; Block1012: // @line: 442 __ret := $r1678; return; Block1010: $Exep0 := $caughtEx1; return; } // procedure is generated by joogie. function {:inline true} $newvariable($param00 : int) returns (__ret : ref); // @line: 83 // (java.lang.String)> procedure void$javaUtilEx.ConcurrentModificationException$$la$init$ra$$2571(__this : ref, $param_0 : ref) requires ($neref((__this), ($null))==1); { var r0430 : ref; var r1431 : ref; Block683: r0430 := __this; r1431 := $param_0; assert ($neref((r0430), ($null))==1); // @line: 84 call void$java.lang.RuntimeException$$la$init$ra$$761((r0430), (r1431)); return; } // @line: 574 // procedure boolean$javaUtilEx.LinkedList$removeFirstOccurrence$2662(__this : ref, $param_0 : ref) returns (__ret : int, $Exep0 : ref) requires ($neref((__this), ($null))==1); { var $z0704 : int; var r0702 : ref; var r1703 : ref; //temp local variables var $caughtEx1 : ref; // @line: 574 Block1067: $caughtEx1 := $null; $Exep0 := $null; goto Block1068; Block1068: r0702 := __this; r1703 := $param_0; assert ($neref((r0702), ($null))==1); // @line: 575 call $z0704, $caughtEx1 := boolean$javaUtilEx.LinkedList$remove$2640((r0702), (r1703)); goto Block1071, Block1069; Block1071: assume ($eqref(($caughtEx1), ($null))==1); goto Block1072; Block1069: assume ($neref(($caughtEx1), ($null))==1); goto Block1070; Block1072: // @line: 575 __ret := $z0704; return; Block1070: $Exep0 := $caughtEx1; return; } // procedure is generated by joogie. function {:inline true} $geint(x : int, y : int) returns (__ret : int) { if (x >= y) then 1 else 0 } // procedure javaUtilEx.ListIterator$javaUtilEx.AbstractSequentialList$listIterator$2585(__this : ref, $param_0 : int) returns (__ret : ref); // procedure is generated by joogie. function {:inline true} $shlref($param00 : ref, $param11 : ref) returns (__ret : int); // @line: 776 // procedure void$javaUtilEx.LinkedList$DescendingIterator$remove$2691(__this : ref) returns ($Exep0 : ref, $Exep1 : ref) requires ($neref((__this), ($null))==1); { var r0896 : ref; var $r1897 : ref; //temp local variables var $caughtEx3 : ref; var $caughtEx2 : ref; // @line: 776 Block1287: $caughtEx3 := $null; $caughtEx2 := $null; $Exep1 := $null; $Exep0 := $null; goto Block1288; Block1288: r0896 := __this; assert ($neref((r0896), ($null))==1); // @line: 777 $r1897 := $HeapVar[r0896, javaUtilEx.LinkedList$ListItr$javaUtilEx.LinkedList$DescendingIterator$itr306]; assert ($neref(($r1897), ($null))==1); // @line: 777 call $caughtEx2, $caughtEx3 := void$javaUtilEx.LinkedList$ListItr$remove$2684(($r1897)); goto Block1289, Block1291; Block1289: assume ($neref(($caughtEx2), ($null))==1); goto Block1290; Block1291: assume ($eqref(($caughtEx2), ($null))==1); goto Block1292; Block1290: $Exep0 := $caughtEx2; return; Block1292: goto Block1295, Block1293; Block1295: assume ($eqref(($caughtEx3), ($null))==1); goto Block1296; Block1293: assume ($neref(($caughtEx3), ($null))==1); goto Block1294; Block1296: return; Block1294: $Exep1 := $caughtEx3; return; } // procedure is generated by joogie. function {:inline true} $reftointarr($param00 : ref) returns (__ret : [int]int); // @line: 202 // procedure int$javaUtilEx.LinkedList$size$2638(__this : ref) returns (__ret : int) requires ($neref((__this), ($null))==1); { var r0577 : ref; var $i0578 : int; Block826: r0577 := __this; assert ($neref((r0577), ($null))==1); // @line: 203 $i0578 := $HeapVar[r0577, int$javaUtilEx.LinkedList$size0]; // @line: 203 __ret := $i0578; return; } // procedure java.lang.Object$javaUtilEx.ListIterator$previous$2528(__this : ref) returns (__ret : ref); // @line: 616 // procedure int$javaUtilEx.SubList$access$210$2568($param_0 : ref) returns (__ret : int) modifies $HeapVar; { var $i1425 : int; var r0423 : ref; var $i0424 : int; Block680: r0423 := $param_0; assert ($neref((r0423), ($null))==1); // @line: 617 $i0424 := $HeapVar[r0423, int$javaUtilEx.SubList$size0]; // @line: 617 $i1425 := $subint(($i0424), (1)); assert ($neref((r0423), ($null))==1); // @line: 617 $HeapVar[r0423, int$javaUtilEx.SubList$size0] := $i1425; // @line: 617 __ret := $i0424; return; } // @line: 213 // procedure boolean$javaUtilEx.AbstractSequentialList$addAll$2583(__this : ref, $param_0 : int, $param_1 : ref) returns (__ret : int, $Exep0 : ref) requires ($neref((__this), ($null))==1); { var r3486 : ref; var $r6490 : ref; var r1484 : ref; var r0480 : ref; var i0481 : int; var z1491 : int; var $r5489 : ref; var r2483 : ref; var $r4488 : ref; var $z0487 : int; //temp local variables var $caughtEx1 : ref; // @line: 213 Block720: $caughtEx1 := $null; $Exep0 := $null; goto Block721; Block721: r0480 := __this; i0481 := $param_0; r1484 := $param_1; goto Block722; // @line: 214 Block722: // @line: 214 z1491 := 0; assert ($neref((r0480), ($null))==1); // @line: 215 call r2483 := javaUtilEx.ListIterator$javaUtilEx.AbstractSequentialList$listIterator$2585((r0480), (i0481)); assert ($neref((r1484), ($null))==1); // @line: 216 call r3486 := javaUtilEx.Iterator$javaUtilEx.Collection$iterator$2244((r1484)); goto Block723; // @line: 217 Block723: assert ($neref((r3486), ($null))==1); // @line: 217 call $z0487 := boolean$javaUtilEx.Iterator$hasNext$2254((r3486)); goto Block724; // @line: 217 Block724: goto Block725, Block727; // @line: 217 Block725: assume ($eqint(($z0487), (0))==1); goto Block726; // @line: 217 Block727: // @line: 217 assume ($negInt(($eqint(($z0487), (0))))==1); assert ($neref((r3486), ($null))==1); // @line: 218 call $r4488 := java.lang.Object$javaUtilEx.Iterator$next$2255((r3486)); assert ($neref((r2483), ($null))==1); // @line: 218 call void$javaUtilEx.ListIterator$add$2533((r2483), ($r4488)); // @line: 219 z1491 := 1; goto Block723; // @line: 221 Block726: // @line: 221 __ret := z1491; return; } // procedure boolean$javaUtilEx.ListIterator$hasNext$2525(__this : ref) returns (__ret : int); // @line: 113 // (javaUtilEx.Collection)> procedure void$javaUtilEx.LinkedList$$la$init$ra$$2630(__this : ref, $param_0 : ref) returns ($Exep0 : ref) requires ($neref((__this), ($null))==1); { var r0540 : ref; var r1541 : ref; //temp local variables var $freshlocal2 : int; var $caughtEx1 : ref; // @line: 113 Block782: $caughtEx1 := $null; $Exep0 := $null; goto Block783; Block783: r0540 := __this; r1541 := $param_0; assert ($neref((r0540), ($null))==1); // @line: 114 call void$javaUtilEx.LinkedList$$la$init$ra$$2629((r0540)); assert ($neref((r0540), ($null))==1); // @line: 115 call $freshlocal2, $caughtEx1 := boolean$javaUtilEx.AbstractCollection$addAll$2236((r0540), (r1541)); goto Block784, Block786; Block784: assume ($neref(($caughtEx1), ($null))==1); goto Block785; Block786: assume ($eqref(($caughtEx1), ($null))==1); goto Block787; Block785: $Exep0 := $caughtEx1; return; Block787: return; } // @line: 4 // procedure void$javaUtilEx.juLinkedListCreateRemoveLastOccurrence$main$2627($param_0 : [int]ref) returns ($Exep0 : ref, $Exep1 : ref) modifies java.lang.String$lp$$rp$$javaUtilEx.Random$args299, $stringSize; { var $r3527 : ref; var $i2524 : int; var $r2521 : ref; var $i3526 : int; var r1520 : ref; var $i0518 : int; var r0517 : [int]ref; var $i1522 : int; var r4528 : ref; //temp local variables var $caughtEx3 : ref; var $caughtEx2 : ref; var $freshlocal4 : int; // @line: 4 Block756: $caughtEx3 := $null; $caughtEx2 := $null; $Exep1 := $null; $Exep0 := $null; goto Block759; Block759: r0517 := $param_0; // @line: 5 java.lang.String$lp$$rp$$javaUtilEx.Random$args299 := r0517; // @line: 7 call $i0518 := int$javaUtilEx.Random$random$2674(); // @line: 7 call r1520 := javaUtilEx.LinkedList$javaUtilEx.juLinkedListCreateRemoveLastOccurrence$createList$2628(($i0518)); // @line: 8 $r2521 := $newvariable((760)); assume ($neref(($newvariable((760))), ($null))==1); // @line: 8 call $i1522 := int$javaUtilEx.Random$random$2674(); assert ($neref(($r2521), ($null))==1); // @line: 8 call void$javaUtilEx.Content$$la$init$ra$$2586(($r2521), ($i1522)); // @line: 8 r4528 := $r2521; // @line: 9 call $i2524 := int$javaUtilEx.Random$random$2674(); goto Block761; // @line: 9 Block761: goto Block764, Block762; // @line: 9 Block764: // @line: 9 assume ($negInt(($leint(($i2524), (42))))==1); // @line: 10 call $i3526 := int$javaUtilEx.Random$random$2674(); assert ($neref((r1520), ($null))==1); // @line: 10 call $r3527, $caughtEx2 := java.lang.Object$javaUtilEx.LinkedList$get$2642((r1520), ($i3526)); goto Block767, Block765; // @line: 9 Block762: assume ($leint(($i2524), (42))==1); goto Block763; // @line: 9 Block767: assume ($eqref(($caughtEx2), ($null))==1); goto Block768; // @line: 9 Block765: assume ($neref(($caughtEx2), ($null))==1); goto Block766; // @line: 12 Block763: assert ($neref((r1520), ($null))==1); // @line: 12 call $freshlocal4, $caughtEx3 := boolean$javaUtilEx.LinkedList$removeLastOccurrence$2663((r1520), (r4528)); goto Block771, Block769; // @line: 9 Block768: // @line: 10 r4528 := $r3527; goto Block763; // @line: 9 Block766: $Exep0 := $caughtEx2; return; // @line: 12 Block771: assume ($eqref(($caughtEx3), ($null))==1); goto Block772; // @line: 12 Block769: assume ($neref(($caughtEx3), ($null))==1); goto Block770; // @line: 12 Block772: return; // @line: 12 Block770: $Exep1 := $caughtEx3; return; } // procedure int$javaUtilEx.AbstractCollection$size$2230(__this : ref) returns (__ret : int); // @line: 124 // procedure java.lang.Object$javaUtilEx.LinkedList$getFirst$2631(__this : ref) returns (__ret : ref, $Exep0 : ref) requires ($neref((__this), ($null))==1); { var r0543 : ref; var $r3547 : ref; var $r2546 : ref; var $r1545 : ref; var $i0544 : int; var $r4548 : ref; //temp local variables // @line: 124 Block788: $Exep0 := $null; goto Block789; Block789: r0543 := __this; assert ($neref((r0543), ($null))==1); // @line: 125 $i0544 := $HeapVar[r0543, int$javaUtilEx.LinkedList$size0]; goto Block790; // @line: 125 Block790: goto Block791, Block793; // @line: 125 Block791: assume ($neint(($i0544), (0))==1); goto Block792; // @line: 125 Block793: // @line: 125 assume ($negInt(($neint(($i0544), (0))))==1); // @line: 126 $r4548 := $newvariable((794)); assume ($neref(($newvariable((794))), ($null))==1); assert ($neref(($r4548), ($null))==1); // @line: 126 call void$javaUtilEx.NoSuchElementException$$la$init$ra$$2572(($r4548)); goto Block795; // @line: 128 Block792: assert ($neref((r0543), ($null))==1); // @line: 128 $r1545 := $HeapVar[r0543, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$header298]; goto Block796; // @line: 125 Block795: $Exep0 := $r4548; return; // @line: 128 Block796: assert ($neref(($r1545), ($null))==1); // @line: 128 $r2546 := $HeapVar[$r1545, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$next301]; assert ($neref(($r2546), ($null))==1); // @line: 128 $r3547 := $HeapVar[$r2546, java.lang.Object$javaUtilEx.LinkedList$Entry$element300]; // @line: 128 __ret := $r3547; return; } // procedure is generated by joogie. function {:inline true} $divreal($param00 : realVar, $param11 : realVar) returns (__ret : realVar); // procedure void$javaUtilEx.ListIterator$add$2533(__this : ref, $param_0 : ref); // @line: 616 // procedure int$javaUtilEx.SubList$access$000$2565($param_0 : ref) returns (__ret : int) { var r0417 : ref; var $i0418 : int; Block677: r0417 := $param_0; assert ($neref((r0417), ($null))==1); // @line: 617 $i0418 := $HeapVar[r0417, int$javaUtilEx.SubList$offset0]; // @line: 617 __ret := $i0418; return; } // @line: 655 // procedure java.lang.Object$javaUtilEx.LinkedList$ListItr$next$2679(__this : ref) returns (__ret : ref, $Exep0 : ref, $Exep1 : ref) modifies $HeapVar; requires ($neref((__this), ($null))==1); { var $r2818 : ref; var $i3822 : int; var $i1817 : int; var $i2821 : int; var $i0816 : int; var $r1815 : ref; var $r5823 : ref; var $r6824 : ref; var r0814 : ref; var $r7825 : ref; var $r3819 : ref; var $r4820 : ref; //temp local variables var $caughtEx2 : ref; // @line: 655 Block1187: $caughtEx2 := $null; $Exep1 := $null; $Exep0 := $null; goto Block1188; Block1188: r0814 := __this; assert ($neref((r0814), ($null))==1); // @line: 656 call $caughtEx2 := void$javaUtilEx.LinkedList$ListItr$checkForComodification$2687((r0814)); goto Block1191, Block1189; Block1191: assume ($eqref(($caughtEx2), ($null))==1); goto Block1192; Block1189: assume ($neref(($caughtEx2), ($null))==1); goto Block1190; Block1192: assert ($neref((r0814), ($null))==1); // @line: 657 $i0816 := $HeapVar[r0814, int$javaUtilEx.LinkedList$ListItr$nextIndex0]; assert ($neref((r0814), ($null))==1); // @line: 657 $r1815 := $HeapVar[r0814, javaUtilEx.LinkedList$javaUtilEx.LinkedList$ListItr$this$0305]; // @line: 657 call $i1817 := int$javaUtilEx.LinkedList$access$100$2670(($r1815)); goto Block1193; Block1190: $Exep0 := $caughtEx2; return; // @line: 657 Block1193: goto Block1194, Block1196; // @line: 657 Block1194: assume ($neint(($i0816), ($i1817))==1); goto Block1195; // @line: 657 Block1196: // @line: 657 assume ($negInt(($neint(($i0816), ($i1817))))==1); // @line: 658 $r7825 := $newvariable((1197)); assume ($neref(($newvariable((1197))), ($null))==1); assert ($neref(($r7825), ($null))==1); // @line: 658 call void$javaUtilEx.NoSuchElementException$$la$init$ra$$2572(($r7825)); goto Block1198; // @line: 660 Block1195: assert ($neref((r0814), ($null))==1); // @line: 660 $r2818 := $HeapVar[r0814, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$ListItr$next304]; goto Block1199; // @line: 657 Block1198: $Exep1 := $r7825; return; // @line: 660 Block1199: assert ($neref((r0814), ($null))==1); // @line: 660 $HeapVar[r0814, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$ListItr$lastReturned303] := $r2818; assert ($neref((r0814), ($null))==1); // @line: 661 $r3819 := $HeapVar[r0814, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$ListItr$next304]; assert ($neref(($r3819), ($null))==1); // @line: 661 $r4820 := $HeapVar[$r3819, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$next301]; assert ($neref((r0814), ($null))==1); // @line: 661 $HeapVar[r0814, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$ListItr$next304] := $r4820; assert ($neref((r0814), ($null))==1); // @line: 662 $i2821 := $HeapVar[r0814, int$javaUtilEx.LinkedList$ListItr$nextIndex0]; // @line: 662 $i3822 := $addint(($i2821), (1)); assert ($neref((r0814), ($null))==1); // @line: 662 $HeapVar[r0814, int$javaUtilEx.LinkedList$ListItr$nextIndex0] := $i3822; assert ($neref((r0814), ($null))==1); // @line: 663 $r5823 := $HeapVar[r0814, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$ListItr$lastReturned303]; assert ($neref(($r5823), ($null))==1); // @line: 663 $r6824 := $HeapVar[$r5823, java.lang.Object$javaUtilEx.LinkedList$Entry$element300]; // @line: 663 __ret := $r6824; return; } // procedure is generated by joogie. function {:inline true} $realtoint($param00 : realVar) returns (__ret : int); // @line: 238 // procedure boolean$javaUtilEx.AbstractCollection$removeAll$2237(__this : ref, $param_0 : ref) returns (__ret : int) requires ($neref((__this), ($null))==1); { var $z150 : int; var r246 : ref; var $z047 : int; var r044 : ref; var z251 : int; var $r349 : ref; var r148 : ref; Block88: r044 := __this; r148 := $param_0; // @line: 239 z251 := 0; assert ($neref((r044), ($null))==1); // @line: 240 call r246 := javaUtilEx.Iterator$javaUtilEx.AbstractCollection$iterator$2229((r044)); goto Block89; // @line: 241 Block89: assert ($neref((r246), ($null))==1); // @line: 241 call $z047 := boolean$javaUtilEx.Iterator$hasNext$2254((r246)); goto Block90; // @line: 241 Block90: goto Block91, Block93; // @line: 241 Block91: assume ($eqint(($z047), (0))==1); goto Block92; // @line: 241 Block93: // @line: 241 assume ($negInt(($eqint(($z047), (0))))==1); assert ($neref((r246), ($null))==1); // @line: 242 call $r349 := java.lang.Object$javaUtilEx.Iterator$next$2255((r246)); assert ($neref((r148), ($null))==1); // @line: 242 call $z150 := boolean$javaUtilEx.Collection$contains$2243((r148), ($r349)); goto Block94; // @line: 247 Block92: // @line: 247 __ret := z251; return; // @line: 242 Block94: goto Block96, Block95; // @line: 242 Block96: // @line: 242 assume ($negInt(($eqint(($z150), (0))))==1); assert ($neref((r246), ($null))==1); // @line: 243 call void$javaUtilEx.Iterator$remove$2256((r246)); // @line: 244 z251 := 1; goto Block89; // @line: 242 Block95: assume ($eqint(($z150), (0))==1); goto Block89; } // @line: 419 // procedure java.lang.Object$javaUtilEx.LinkedList$element$2650(__this : ref) returns (__ret : ref, $Exep0 : ref) requires ($neref((__this), ($null))==1); { var $r1673 : ref; var r0672 : ref; //temp local variables var $caughtEx1 : ref; // @line: 419 Block990: $caughtEx1 := $null; $Exep0 := $null; goto Block991; Block991: r0672 := __this; assert ($neref((r0672), ($null))==1); // @line: 420 call $r1673, $caughtEx1 := java.lang.Object$javaUtilEx.LinkedList$getFirst$2631((r0672)); goto Block994, Block992; Block994: assume ($eqref(($caughtEx1), ($null))==1); goto Block995; Block992: assume ($neref(($caughtEx1), ($null))==1); goto Block993; Block995: // @line: 420 __ret := $r1673; return; Block993: $Exep0 := $caughtEx1; return; } // procedure is generated by joogie. function {:inline true} $negRef($param00 : ref) returns (__ret : int); // @line: 680 // procedure boolean$javaUtilEx.SubList$addAll$2557(__this : ref, $param_0 : int, $param_1 : ref) returns (__ret : int, $Exep1 : ref, $Exep0 : ref, $Exep2 : ref) modifies $HeapVar; requires ($neref((__this), ($null))==1); { var $r3387 : ref; var $i5389 : int; var $i2383 : int; var $i4388 : int; var $i6390 : int; var $i3384 : int; var $r2385 : ref; var r0378 : ref; var i1382 : int; var i0379 : int; var r1380 : ref; //temp local variables var $freshlocal6 : int; var $caughtEx5 : ref; var $caughtEx4 : ref; var $caughtEx3 : ref; // @line: 680 Block577: $caughtEx5 := $null; $caughtEx4 := $null; $caughtEx3 := $null; $Exep2 := $null; $Exep1 := $null; $Exep0 := $null; goto Block592; Block592: r0378 := __this; i0379 := $param_0; r1380 := $param_1; assert ($neref((r0378), ($null))==1); // @line: 681 call $caughtEx3 := void$javaUtilEx.SubList$rangeCheckForAdd$2562((r0378), (i0379)); goto Block595, Block593; Block595: assume ($eqref(($caughtEx3), ($null))==1); goto Block596; Block593: assume ($neref(($caughtEx3), ($null))==1); goto Block594; Block596: assert ($neref((r1380), ($null))==1); // @line: 682 call i1382 := int$javaUtilEx.Collection$size$2241((r1380)); goto Block597; Block594: $Exep0 := $caughtEx3; return; // @line: 683 Block597: goto Block600, Block598; // @line: 683 Block600: // @line: 683 assume ($negInt(($neint((i1382), (0))))==1); // @line: 684 __ret := 0; return; // @line: 683 Block598: assume ($neint((i1382), (0))==1); goto Block599; // @line: 686 Block599: assert ($neref((r0378), ($null))==1); // @line: 686 call $caughtEx4 := void$javaUtilEx.SubList$checkForComodification$2564((r0378)); goto Block601, Block603; // @line: 686 Block601: assume ($neref(($caughtEx4), ($null))==1); goto Block602; // @line: 686 Block603: assume ($eqref(($caughtEx4), ($null))==1); goto Block604; // @line: 686 Block602: $Exep1 := $caughtEx4; return; // @line: 686 Block604: goto Block605; // @line: 687 Block605: assert ($neref((r0378), ($null))==1); // @line: 687 $r2385 := $HeapVar[r0378, javaUtilEx.AbstractList$javaUtilEx.SubList$l297]; assert ($neref((r0378), ($null))==1); // @line: 687 $i2383 := $HeapVar[r0378, int$javaUtilEx.SubList$offset0]; // @line: 687 $i3384 := $addint(($i2383), (i0379)); assert ($neref(($r2385), ($null))==1); // @line: 687 call $freshlocal6, $caughtEx3, $caughtEx5 := boolean$javaUtilEx.AbstractList$addAll$2492(($r2385), ($i3384), (r1380)); goto Block606, Block608; // @line: 687 Block606: assume ($neref(($caughtEx3), ($null))==1); goto Block607; // @line: 687 Block608: assume ($eqref(($caughtEx3), ($null))==1); goto Block609; // @line: 687 Block607: $Exep0 := $caughtEx3; return; // @line: 687 Block609: goto Block612, Block610; // @line: 687 Block612: assume ($eqref(($caughtEx5), ($null))==1); goto Block613; // @line: 687 Block610: assume ($neref(($caughtEx5), ($null))==1); goto Block611; // @line: 687 Block613: assert ($neref((r0378), ($null))==1); // @line: 688 $r3387 := $HeapVar[r0378, javaUtilEx.AbstractList$javaUtilEx.SubList$l297]; assert ($neref(($r3387), ($null))==1); // @line: 688 $i4388 := $HeapVar[$r3387, int$javaUtilEx.AbstractList$modCount0]; assert ($neref((r0378), ($null))==1); // @line: 688 $HeapVar[r0378, int$javaUtilEx.AbstractList$modCount0] := $i4388; assert ($neref((r0378), ($null))==1); // @line: 689 $i5389 := $HeapVar[r0378, int$javaUtilEx.SubList$size0]; // @line: 689 $i6390 := $addint(($i5389), (i1382)); assert ($neref((r0378), ($null))==1); // @line: 689 $HeapVar[r0378, int$javaUtilEx.SubList$size0] := $i6390; // @line: 690 __ret := 1; return; // @line: 687 Block611: $Exep2 := $caughtEx5; return; } // @line: 146 // procedure boolean$javaUtilEx.AbstractCollection$remove$2234(__this : ref, $param_0 : ref) returns (__ret : int) requires ($neref((__this), ($null))==1); { var r121 : ref; var $z225 : int; var $r426 : ref; var $z124 : int; var r018 : ref; var $r323 : ref; var r220 : ref; var $z022 : int; Block46: r018 := __this; r121 := $param_0; assert ($neref((r018), ($null))==1); // @line: 147 call r220 := javaUtilEx.Iterator$javaUtilEx.AbstractCollection$iterator$2229((r018)); goto Block47; // @line: 148 Block47: goto Block48, Block50; // @line: 148 Block48: assume ($neref((r121), ($null))==1); goto Block49; // @line: 148 Block50: // @line: 148 assume ($negInt(($neref((r121), ($null))))==1); goto Block51; // @line: 156 Block49: assert ($neref((r220), ($null))==1); // @line: 156 call $z022 := boolean$javaUtilEx.Iterator$hasNext$2254((r220)); goto Block59; // @line: 149 Block51: assert ($neref((r220), ($null))==1); // @line: 149 call $z225 := boolean$javaUtilEx.Iterator$hasNext$2254((r220)); goto Block52; // @line: 156 Block59: goto Block61, Block60; // @line: 149 Block52: goto Block53, Block55; // @line: 156 Block61: // @line: 156 assume ($negInt(($eqint(($z022), (0))))==1); assert ($neref((r220), ($null))==1); // @line: 157 call $r323 := java.lang.Object$javaUtilEx.Iterator$next$2255((r220)); assert ($neref((r121), ($null))==1); // @line: 157 call $z124 := boolean$java.lang.Object$equals$32((r121), ($r323)); goto Block62; // @line: 156 Block60: assume ($eqint(($z022), (0))==1); goto Block54; // @line: 149 Block53: assume ($eqint(($z225), (0))==1); goto Block54; // @line: 149 Block55: // @line: 149 assume ($negInt(($eqint(($z225), (0))))==1); assert ($neref((r220), ($null))==1); // @line: 150 call $r426 := java.lang.Object$javaUtilEx.Iterator$next$2255((r220)); goto Block56; // @line: 157 Block62: goto Block63, Block64; // @line: 163 Block54: // @line: 163 __ret := 0; return; // @line: 150 Block56: goto Block57, Block58; // @line: 157 Block63: assume ($eqint(($z124), (0))==1); goto Block49; // @line: 157 Block64: // @line: 157 assume ($negInt(($eqint(($z124), (0))))==1); assert ($neref((r220), ($null))==1); // @line: 158 call void$javaUtilEx.Iterator$remove$2256((r220)); // @line: 159 __ret := 1; return; // @line: 150 Block57: assume ($neref(($r426), ($null))==1); goto Block51; // @line: 150 Block58: // @line: 150 assume ($negInt(($neref(($r426), ($null))))==1); assert ($neref((r220), ($null))==1); // @line: 151 call void$javaUtilEx.Iterator$remove$2256((r220)); // @line: 152 __ret := 1; return; } // @line: 660 // procedure java.lang.Object$javaUtilEx.SubList$remove$2554(__this : ref, $param_0 : int) returns (__ret : ref, $Exep1 : ref, $Exep0 : ref, $Exep2 : ref) modifies $HeapVar; requires ($neref((__this), ($null))==1); { var $i3358 : int; var $i5360 : int; var r1356 : ref; var $i1352 : int; var $r3357 : ref; var r0350 : ref; var $i4359 : int; var $r2354 : ref; var i0351 : int; var $i2353 : int; //temp local variables var $caughtEx5 : ref; var $caughtEx3 : ref; var $caughtEx4 : ref; // @line: 660 Block553: $caughtEx5 := $null; $caughtEx4 := $null; $caughtEx3 := $null; $Exep2 := $null; $Exep1 := $null; $Exep0 := $null; goto Block554; Block554: r0350 := __this; i0351 := $param_0; assert ($neref((r0350), ($null))==1); // @line: 661 call $caughtEx3 := void$javaUtilEx.SubList$rangeCheck$2561((r0350), (i0351)); goto Block557, Block555; Block557: assume ($eqref(($caughtEx3), ($null))==1); goto Block558; Block555: assume ($neref(($caughtEx3), ($null))==1); goto Block556; Block558: assert ($neref((r0350), ($null))==1); // @line: 662 call $caughtEx4 := void$javaUtilEx.SubList$checkForComodification$2564((r0350)); goto Block561, Block559; Block556: $Exep0 := $caughtEx3; return; Block561: assume ($eqref(($caughtEx4), ($null))==1); goto Block562; Block559: assume ($neref(($caughtEx4), ($null))==1); goto Block560; Block562: assert ($neref((r0350), ($null))==1); // @line: 663 $r2354 := $HeapVar[r0350, javaUtilEx.AbstractList$javaUtilEx.SubList$l297]; assert ($neref((r0350), ($null))==1); // @line: 663 $i1352 := $HeapVar[r0350, int$javaUtilEx.SubList$offset0]; // @line: 663 $i2353 := $addint((i0351), ($i1352)); assert ($neref(($r2354), ($null))==1); // @line: 663 call r1356, $caughtEx5 := java.lang.Object$javaUtilEx.AbstractList$remove$2488(($r2354), ($i2353)); goto Block565, Block563; Block560: $Exep1 := $caughtEx4; return; Block565: assume ($eqref(($caughtEx5), ($null))==1); goto Block566; Block563: assume ($neref(($caughtEx5), ($null))==1); goto Block564; Block566: assert ($neref((r0350), ($null))==1); // @line: 664 $r3357 := $HeapVar[r0350, javaUtilEx.AbstractList$javaUtilEx.SubList$l297]; assert ($neref(($r3357), ($null))==1); // @line: 664 $i3358 := $HeapVar[$r3357, int$javaUtilEx.AbstractList$modCount0]; assert ($neref((r0350), ($null))==1); // @line: 664 $HeapVar[r0350, int$javaUtilEx.AbstractList$modCount0] := $i3358; assert ($neref((r0350), ($null))==1); // @line: 665 $i4359 := $HeapVar[r0350, int$javaUtilEx.SubList$size0]; // @line: 665 $i5360 := $subint(($i4359), (1)); assert ($neref((r0350), ($null))==1); // @line: 665 $HeapVar[r0350, int$javaUtilEx.SubList$size0] := $i5360; // @line: 666 __ret := r1356; return; Block564: $Exep2 := $caughtEx5; return; } // @line: 476 // procedure boolean$javaUtilEx.LinkedList$offerLast$2655(__this : ref, $param_0 : ref) returns (__ret : int) requires ($neref((__this), ($null))==1); { var r1685 : ref; var r0684 : ref; Block1015: r0684 := __this; r1685 := $param_0; assert ($neref((r0684), ($null))==1); // @line: 477 call void$javaUtilEx.LinkedList$addLast$2636((r0684), (r1685)); // @line: 478 __ret := 1; return; } // procedure is generated by joogie. function {:inline true} $negInt(x : int) returns (__ret : int) { if (x == 0) then 1 else 0 } // @line: 214 // procedure boolean$javaUtilEx.LinkedList$add$2639(__this : ref, $param_0 : ref) returns (__ret : int) requires ($neref((__this), ($null))==1); { var r1580 : ref; var $r2581 : ref; var r0579 : ref; //temp local variables var $freshlocal0 : ref; Block827: r0579 := __this; r1580 := $param_0; assert ($neref((r0579), ($null))==1); // @line: 215 $r2581 := $HeapVar[r0579, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$header298]; assert ($neref((r0579), ($null))==1); // @line: 215 call $freshlocal0 := javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$addBefore$2665((r0579), (r1580), ($r2581)); // @line: 216 __ret := 1; return; } // (java.lang.String,java.lang.Throwable)> procedure void$java.lang.RuntimeException$$la$init$ra$$762(__this : ref, $param_0 : ref, $param_1 : ref); // @line: 697 // procedure javaUtilEx.ListIterator$javaUtilEx.SubList$listIterator$2559(__this : ref, $param_0 : int) returns (__ret : ref, $Exep0 : ref, $Exep1 : ref) requires ($neref((__this), ($null))==1); { var $r1395 : ref; var r0393 : ref; var i0394 : int; //temp local variables var $caughtEx2 : ref; var $caughtEx3 : ref; // @line: 697 Block620: $caughtEx3 := $null; $caughtEx2 := $null; $Exep1 := $null; $Exep0 := $null; goto Block622; Block622: r0393 := __this; i0394 := $param_0; assert ($neref((r0393), ($null))==1); // @line: 698 call $caughtEx2 := void$javaUtilEx.SubList$checkForComodification$2564((r0393)); goto Block623, Block625; Block623: assume ($neref(($caughtEx2), ($null))==1); goto Block624; Block625: assume ($eqref(($caughtEx2), ($null))==1); goto Block626; Block624: $Exep0 := $caughtEx2; return; Block626: assert ($neref((r0393), ($null))==1); // @line: 699 call $caughtEx3 := void$javaUtilEx.SubList$rangeCheckForAdd$2562((r0393), (i0394)); goto Block627, Block629; Block627: assume ($neref(($caughtEx3), ($null))==1); goto Block628; Block629: assume ($eqref(($caughtEx3), ($null))==1); goto Block630; Block628: $Exep1 := $caughtEx3; return; Block630: // @line: 701 $r1395 := $newvariable((631)); assume ($neref(($newvariable((631))), ($null))==1); assert ($neref(($r1395), ($null))==1); // @line: 701 call $caughtEx3 := void$javaUtilEx.SubList$1$$la$init$ra$$2693(($r1395), (r0393), (i0394)); goto Block634, Block632; Block634: assume ($eqref(($caughtEx3), ($null))==1); goto Block635; Block632: assume ($neref(($caughtEx3), ($null))==1); goto Block633; Block635: // @line: 701 __ret := $r1395; return; Block633: $Exep1 := $caughtEx3; return; } // @line: 72 // (java.lang.String,java.lang.Throwable)> procedure void$javaUtilEx.IllegalArgumentException$$la$init$ra$$2624(__this : ref, $param_0 : ref, $param_1 : ref) requires ($neref((__this), ($null))==1); { var r2513 : ref; var r1512 : ref; var r0511 : ref; Block751: r0511 := __this; r1512 := $param_0; r2513 := $param_1; assert ($neref((r0511), ($null))==1); // @line: 73 call void$java.lang.RuntimeException$$la$init$ra$$762((r0511), (r1512), (r2513)); return; } // procedure is generated by joogie. function {:inline true} $eqref(x : ref, y : ref) returns (__ret : int) { if (x == y) then 1 else 0 } // @line: 90 // procedure javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$access$000$2669($param_0 : ref) returns (__ret : ref) { var r0761 : ref; var $r1762 : ref; Block1141: r0761 := $param_0; assert ($neref((r0761), ($null))==1); // @line: 91 $r1762 := $HeapVar[r0761, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$header298]; // @line: 91 __ret := $r1762; return; } // @line: 531 // procedure java.lang.Object$javaUtilEx.LinkedList$pollLast$2659(__this : ref) returns (__ret : ref, $Exep0 : ref) requires ($neref((__this), ($null))==1); { var $r1697 : ref; var r0695 : ref; var $i0696 : int; //temp local variables var $caughtEx1 : ref; // @line: 531 Block1049: $caughtEx1 := $null; $Exep0 := $null; goto Block1050; Block1050: r0695 := __this; assert ($neref((r0695), ($null))==1); // @line: 532 $i0696 := $HeapVar[r0695, int$javaUtilEx.LinkedList$size0]; goto Block1051; // @line: 532 Block1051: goto Block1052, Block1054; // @line: 532 Block1052: assume ($neint(($i0696), (0))==1); goto Block1053; // @line: 532 Block1054: // @line: 532 assume ($negInt(($neint(($i0696), (0))))==1); // @line: 533 __ret := $null; return; // @line: 534 Block1053: assert ($neref((r0695), ($null))==1); // @line: 534 call $r1697, $caughtEx1 := java.lang.Object$javaUtilEx.LinkedList$removeLast$2634((r0695)); goto Block1055, Block1057; // @line: 534 Block1055: assume ($neref(($caughtEx1), ($null))==1); goto Block1056; // @line: 534 Block1057: assume ($eqref(($caughtEx1), ($null))==1); goto Block1058; // @line: 534 Block1056: $Exep0 := $caughtEx1; return; // @line: 534 Block1058: goto Block1059; // @line: 534 Block1059: // @line: 534 __ret := $r1697; return; } // @line: 238 // procedure javaUtilEx.Iterator$javaUtilEx.AbstractSequentialList$iterator$2584(__this : ref) returns (__ret : ref, $Exep0 : ref) requires ($neref((__this), ($null))==1); { var $r1494 : ref; var r0493 : ref; //temp local variables var $caughtEx1 : ref; // @line: 238 Block731: $caughtEx1 := $null; $Exep0 := $null; goto Block732; Block732: r0493 := __this; assert ($neref((r0493), ($null))==1); // @line: 239 call $r1494, $caughtEx1 := javaUtilEx.ListIterator$javaUtilEx.AbstractList$listIterator$2494((r0493)); goto Block735, Block733; Block735: assume ($eqref(($caughtEx1), ($null))==1); goto Block736; Block733: assume ($neref(($caughtEx1), ($null))==1); goto Block734; Block736: // @line: 239 __ret := $r1494; return; Block734: $Exep0 := $caughtEx1; return; } // @line: 87 // procedure java.lang.Object$javaUtilEx.AbstractSequentialList$get$2579(__this : ref, $param_0 : int) returns (__ret : ref, $Exep0 : ref) requires ($neref((__this), ($null))==1); { var $r5450 : ref; var r0444 : ref; var $r4448 : ref; var $r2446 : ref; var $r3447 : ref; var i0445 : int; //temp local variables var $caughtEx1 : ref; // @line: 87 Block691: $caughtEx1 := $null; $Exep0 := $null; goto Block692; Block692: r0444 := __this; i0445 := $param_0; goto Block693; // @line: 88 Block693: assert ($neref((r0444), ($null))==1); // @line: 88 call $r2446 := javaUtilEx.ListIterator$javaUtilEx.AbstractSequentialList$listIterator$2585((r0444), (i0445)); assert ($neref(($r2446), ($null))==1); // @line: 88 call $r3447 := java.lang.Object$javaUtilEx.ListIterator$next$2526(($r2446)); goto Block694; // @line: 88 Block694: // @line: 88 __ret := $r3447; return; } // @line: 729 // (java.lang.Object,javaUtilEx.LinkedList$Entry,javaUtilEx.LinkedList$Entry)> procedure void$javaUtilEx.LinkedList$Entry$$la$init$ra$$2676(__this : ref, $param_0 : ref, $param_1 : ref, $param_2 : ref) modifies $HeapVar; requires ($neref((__this), ($null))==1); { var r0779 : ref; var r2781 : ref; var r3782 : ref; var r1780 : ref; Block1153: r0779 := __this; r1780 := $param_0; r2781 := $param_1; r3782 := $param_2; assert ($neref((r0779), ($null))==1); // @line: 730 call void$java.lang.Object$$la$init$ra$$28((r0779)); assert ($neref((r0779), ($null))==1); // @line: 731 $HeapVar[r0779, java.lang.Object$javaUtilEx.LinkedList$Entry$element300] := r1780; assert ($neref((r0779), ($null))==1); // @line: 732 $HeapVar[r0779, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$next301] := r2781; assert ($neref((r0779), ($null))==1); // @line: 733 $HeapVar[r0779, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$Entry$previous302] := r3782; return; } // @line: 180 // procedure void$javaUtilEx.LinkedList$addLast$2636(__this : ref, $param_0 : ref) requires ($neref((__this), ($null))==1); { var $r2570 : ref; var r0568 : ref; var r1569 : ref; //temp local variables var $freshlocal0 : ref; Block819: r0568 := __this; r1569 := $param_0; assert ($neref((r0568), ($null))==1); // @line: 181 $r2570 := $HeapVar[r0568, javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$header298]; assert ($neref((r0568), ($null))==1); // @line: 181 call $freshlocal0 := javaUtilEx.LinkedList$Entry$javaUtilEx.LinkedList$addBefore$2665((r0568), (r1569), ($r2570)); return; } // @line: 126 // procedure boolean$javaUtilEx.AbstractCollection$add$2233(__this : ref, $param_0 : ref) returns (__ret : int, $Exep0 : ref) requires ($neref((__this), ($null))==1); { var $r215 : ref; var r117 : ref; var r016 : ref; //temp local variables // @line: 126 Block42: $Exep0 := $null; goto Block43; Block43: r016 := __this; r117 := $param_0; // @line: 127 $r215 := $newvariable((44)); assume ($neref(($newvariable((44))), ($null))==1); assert ($neref(($r215), ($null))==1); // @line: 127 call void$javaUtilEx.UnsupportedOperationException$$la$init$ra$$2257(($r215)); goto Block45; Block45: $Exep0 := $r215; return; } // procedure void$javaUtilEx.ListIterator$set$2532(__this : ref, $param_0 : ref);