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 // procedure is generated by joogie. function {:inline true} $neref(x : ref, y : ref) returns (__ret : int) { if (x != y) then 1 else 0 } // procedure is generated by joogie. function {:inline true} $realarrtoref($param00 : [int]realVar) returns (__ret : ref); // procedure is generated by joogie. function {:inline true} $modreal($param00 : realVar, $param11 : realVar) returns (__ret : realVar); // procedure is generated by joogie. function {:inline true} $leref($param00 : ref, $param11 : ref) returns (__ret : int); // procedure is generated by joogie. function {:inline true} $modint($param00 : int, $param11 : int) returns (__ret : int); // procedure is generated by joogie. function {:inline true} $gtref($param00 : ref, $param11 : ref) returns (__ret : int); // 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} $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); // procedure is generated by joogie. function {:inline true} $inttoreal($param00 : int) returns (__ret : realVar); // procedure is generated by joogie. function {:inline true} $shrint($param00 : int, $param11 : int) returns (__ret : int); // procedure is generated by joogie. function {:inline true} $negReal($param00 : realVar) returns (__ret : int); // procedure is generated by joogie. function {:inline true} $ushrint($param00 : int, $param11 : int) returns (__ret : int); // procedure is generated by joogie. function {:inline true} $refarrtoref($param00 : [int]ref) returns (__ret : ref); // procedure is generated by joogie. function {:inline true} $divref($param00 : ref, $param11 : ref) returns (__ret : ref); // procedure is generated by joogie. function {:inline true} $mulref($param00 : ref, $param11 : ref) returns (__ret : ref); // procedure is generated by joogie. function {:inline true} $neint(x : int, y : int) returns (__ret : int) { if (x != y) then 1 else 0 } // procedure is generated by joogie. function {:inline true} $ltreal($param00 : realVar, $param11 : realVar) returns (__ret : int); // procedure is generated by joogie. function {:inline true} $reftorefarr($param00 : ref) returns (__ret : [int]ref); // procedure is generated by joogie. function {:inline true} $gtint(x : int, y : int) returns (__ret : int) { if (x > y) then 1 else 0 } // procedure is generated by joogie. function {:inline true} $reftoint($param00 : ref) returns (__ret : int); // procedure is generated by joogie. function {:inline true} $addref($param00 : ref, $param11 : ref) returns (__ret : ref); // procedure is generated by joogie. function {:inline true} $xorreal($param00 : realVar, $param11 : realVar) returns (__ret : int); // procedure is generated by joogie. function {:inline true} $andref($param00 : ref, $param11 : ref) returns (__ret : int); // 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 } // 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 is generated by joogie. function {:inline true} $eqreal(x : realVar, y : realVar) returns (__ret : int) { if (x == y) then 1 else 0 } // procedure is generated by joogie. function {:inline true} $ltint(x : int, y : int) returns (__ret : int) { if (x < y) then 1 else 0 } // procedure is generated by joogie. function {:inline true} $newvariable($param00 : int) returns (__ret : ref); // procedure is generated by joogie. function {:inline true} $divint($param00 : int, $param11 : int) returns (__ret : int); // procedure is generated by joogie. function {:inline true} $geint(x : int, y : int) returns (__ret : int) { if (x >= y) then 1 else 0 } // procedure is generated by joogie. function {:inline true} $mulint($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 } // procedure is generated by joogie. function {:inline true} $shlref($param00 : ref, $param11 : ref) returns (__ret : int); // procedure is generated by joogie. function {:inline true} $eqrefarray($param00 : [int]ref, $param11 : [int]ref) returns (__ret : int); // procedure is generated by joogie. function {:inline true} $reftointarr($param00 : ref) returns (__ret : [int]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 is generated by joogie. function {:inline true} $shrref($param00 : ref, $param11 : ref) returns (__ret : int); // procedure is generated by joogie. function {:inline true} $ushrreal($param00 : realVar, $param11 : realVar) returns (__ret : int); // procedure is generated by joogie. function {:inline true} $shrreal($param00 : realVar, $param11 : realVar) returns (__ret : int); // procedure is generated by joogie. function {:inline true} $divreal($param00 : realVar, $param11 : realVar) returns (__ret : realVar); // procedure is generated by joogie. function {:inline true} $orint($param00 : int, $param11 : int) returns (__ret : int); // ()> procedure void$java.lang.Object$$la$init$ra$$28(__this : ref); // procedure is generated by joogie. function {:inline true} $reftorealarr($param00 : ref) returns (__ret : [int]realVar); // 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 is generated by joogie. function {:inline true} $realtoint($param00 : realVar) returns (__ret : int); // procedure is generated by joogie. function {:inline true} $geref($param00 : ref, $param11 : ref) returns (__ret : int); // procedure is generated by joogie. function {:inline true} $orreal($param00 : realVar, $param11 : realVar) returns (__ret : int); // procedure is generated by joogie. function {:inline true} $eqint(x : int, y : int) returns (__ret : int) { if (x == y) then 1 else 0 } // procedure is generated by joogie. function {:inline true} $ushrref($param00 : ref, $param11 : ref) returns (__ret : int); // ()> procedure void$Avg$$la$init$ra$$2228(__this : ref) requires ($neref((__this), ($null))==1); { var r01 : ref; Block16: r01 := __this; assert ($neref((r01), ($null))==1); // @line: 1 call void$java.lang.Object$$la$init$ra$$28((r01)); return; } // procedure is generated by joogie. function {:inline true} $modref($param00 : ref, $param11 : ref) returns (__ret : ref); // 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} $negRef($param00 : ref) returns (__ret : int); // procedure is generated by joogie. function {:inline true} $lereal($param00 : realVar, $param11 : realVar) returns (__ret : int); // procedure is generated by joogie. function {:inline true} $nereal(x : realVar, y : realVar) returns (__ret : int) { if (x != y) then 1 else 0 } // @line: 9 // procedure int$Avg$average$2230($param_0 : int, $param_1 : int) returns (__ret : int) { var i010 : int; var $i415 : int; var $i516 : int; var $i212 : int; var $i718 : int; var i111 : int; var $i617 : int; var $i819 : int; var $i313 : int; Block18: i010 := $param_0; i111 := $param_1; goto Block19; // @line: 10 Block19: goto Block20, Block22; // @line: 10 Block20: assume ($leint((i010), (0))==1); goto Block21; // @line: 10 Block22: // @line: 10 assume ($negInt(($leint((i010), (0))))==1); // @line: 11 $i718 := $subint((i010), (1)); // @line: 11 $i617 := $addint((i111), (1)); // @line: 11 call $i819 := int$Avg$average$2230(($i718), ($i617)); // @line: 11 __ret := $i819; return; // @line: 12 Block21: goto Block25, Block23; // @line: 12 Block25: // @line: 12 assume ($negInt(($leint((i111), (2))))==1); goto Block26; // @line: 12 Block23: assume ($leint((i111), (2))==1); goto Block24; // @line: 13 Block26: // @line: 13 $i313 := $addint((i010), (1)); // @line: 13 $i212 := $subint((i111), (2)); // @line: 13 call $i415 := int$Avg$average$2230(($i313), ($i212)); // @line: 13 $i516 := $addint((1), ($i415)); // @line: 13 __ret := $i516; return; // @line: 15 Block24: // @line: 15 __ret := 1; return; } // procedure is generated by joogie. function {:inline true} $instanceof($param00 : ref, $param11 : classConst) returns (__ret : int); // procedure is generated by joogie. function {:inline true} $xorref($param00 : ref, $param11 : ref) returns (__ret : int); // procedure is generated by joogie. function {:inline true} $orref($param00 : ref, $param11 : ref) returns (__ret : int); // procedure int$java.lang.String$length$59(__this : ref) returns (__ret : int); // 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); // procedure is generated by joogie. function {:inline true} $shlreal($param00 : realVar, $param11 : realVar) returns (__ret : int); // procedure is generated by joogie. function {:inline true} $negInt(x : int) returns (__ret : int) { if (x == 0) then 1 else 0 } // procedure is generated by joogie. function {:inline true} $gereal($param00 : realVar, $param11 : realVar) returns (__ret : int); // procedure is generated by joogie. function {:inline true} $eqref(x : ref, y : ref) returns (__ret : int) { if (x == y) then 1 else 0 } // @line: 3 // procedure void$Avg$main$2229($param_0 : [int]ref) modifies $stringSize; { var i05 : int; var i18 : int; var r02 : [int]ref; var $r26 : ref; var $r13 : ref; //temp local variables var $freshlocal0 : int; Block17: r02 := $param_0; assert ($geint((0), (0))==1); assert ($ltint((0), ($refArrSize[r02[$arrSizeIdx]]))==1); // @line: 4 $r13 := r02[0]; i05 := $stringSize[$r13]; assert ($geint((1), (0))==1); assert ($ltint((1), ($refArrSize[r02[$arrSizeIdx]]))==1); // @line: 5 $r26 := r02[1]; i18 := $stringSize[$r26]; // @line: 6 call $freshlocal0 := int$Avg$average$2230((i05), (i18)); 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 } // procedure is generated by joogie. function {:inline true} $andint($param00 : int, $param11 : int) returns (__ret : int); // procedure is generated by joogie. function {:inline true} $andreal($param00 : realVar, $param11 : realVar) returns (__ret : int); // procedure is generated by joogie. function {:inline true} $shlint($param00 : int, $param11 : int) returns (__ret : int); // procedure is generated by joogie. function {:inline true} $xorint($param00 : int, $param11 : int) returns (__ret : int); // procedure is generated by joogie. function {:inline true} $subint(x : int, y : int) returns (__ret : int) { (x - y) }