From 8286347ebf84037517a740e7d1d87127ce5a0902 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ezgi=20=C3=87i=C3=A7ek?= Date: Thu, 8 Aug 2019 04:34:15 -0700 Subject: [PATCH] [inferbo] Add models for Java's Integer Summary: Add models for Java's Integer class. Reviewed By: skcho Differential Revision: D16668118 fbshipit-source-id: 05b3c8736 --- .../src/bufferoverrun/bufferOverrunDomain.ml | 5 +++ .../src/bufferoverrun/bufferOverrunModels.ml | 35 ++++++++++++++++++- infer/src/bufferoverrun/bufferOverrunTrace.ml | 7 +++- .../bufferoverrun/bufferOverrunTypModels.ml | 14 +++++--- infer/src/bufferoverrun/bufferOverrunUtils.ml | 2 +- .../java/bufferoverrun/issues.exp | 2 +- .../java/performance/ArrayListTest.java | 3 +- .../java/performance/IntTest.java | 22 ++++++++++++ .../codetoanalyze/java/performance/issues.exp | 16 +++++---- 9 files changed, 91 insertions(+), 15 deletions(-) create mode 100644 infer/tests/codetoanalyze/java/performance/IntTest.java diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 1955338cf..5e6265a69 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -490,6 +490,11 @@ module Val = struct let allocsite = Allocsite.make_symbol deref_path in let length = Itv.of_length_path ~is_void:false path in of_java_array_alloc allocsite ~length ~traces + | Some JavaInteger -> + let l = Loc.of_path path in + let traces = traces_of_loc l in + let unsigned = Typ.is_unsigned_int typ in + of_itv ~traces (Itv.of_normal_path ~unsigned path) | None -> let l = Loc.of_path path in let traces = traces_of_loc l in diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index 8c701e8ba..56f8fcecb 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -712,6 +712,35 @@ module StdVector = struct {exec; check= no_check} end +(** Java's integers are modeled with an indirection to a memory + location that holds the actual integer value *) +module JavaInteger = struct + let intValue exp = + let exec _ ~ret:(id, _) mem = + let powloc = Sem.eval_locs exp mem in + let v = if PowLoc.is_empty powloc then Dom.Val.Itv.top else Dom.Mem.find_set powloc mem in + model_by_value v id mem + in + {exec; check= no_check} + + + let valueOf exp = + let exec {pname; node_hash; location; integer_type_widths} ~ret:(id, _) mem = + let represents_multiple_values = false in + let int_allocsite = + Allocsite.make pname ~node_hash ~inst_num:0 ~dimension:0 ~path:None + ~represents_multiple_values + in + let v = Sem.eval integer_type_widths exp mem in + let int_loc = Loc.of_allocsite int_allocsite in + mem |> Dom.Mem.add_heap int_loc v + |> Dom.Mem.add_stack (Loc.of_id id) + ( int_loc |> PowLoc.singleton + |> Dom.Val.of_pow_loc ~traces:Trace.(Set.singleton location JavaIntDecleration) ) + in + {exec; check= no_check} +end + (* Java's Collections are represented like arrays. But we don't care about the elements. - when they are constructed, we set the size to 0 - each time we add an element, we increase the length of the array @@ -1081,5 +1110,9 @@ module Call = struct ; +PatternMatch.implements_org_json "JSONArray" &:: "length" <>$ capt_exp $!--> Collection.size ; +PatternMatch.implements_org_json "JSONArray" - &:: "" <>$ capt_var_exn $+ capt_exp $--> Collection.init ] + &:: "" <>$ capt_var_exn $+ capt_exp $--> Collection.init + ; +PatternMatch.implements_lang "Integer" + &:: "intValue" <>$ capt_exp $--> JavaInteger.intValue + ; +PatternMatch.implements_lang "Integer" &:: "valueOf" <>$ capt_exp $--> JavaInteger.valueOf + ] end diff --git a/infer/src/bufferoverrun/bufferOverrunTrace.ml b/infer/src/bufferoverrun/bufferOverrunTrace.ml index eab653bce..461099158 100644 --- a/infer/src/bufferoverrun/bufferOverrunTrace.ml +++ b/infer/src/bufferoverrun/bufferOverrunTrace.ml @@ -16,6 +16,7 @@ module BoTrace = struct type elem = | ArrayDeclaration + | JavaIntDecleration | Assign of PowLoc.t | Global of Loc.t | Parameter of Loc.t @@ -77,6 +78,8 @@ module BoTrace = struct let pp_elem f = function | ArrayDeclaration -> F.pp_print_string f "ArrayDeclaration" + | JavaIntDecleration -> + F.pp_print_string f "JavaIntDeclaration" | Assign locs -> F.fprintf f "Assign `%a`" PowLoc.pp locs | Global loc -> @@ -115,7 +118,7 @@ module BoTrace = struct let has_unknown = final_exists ~f:(function UnknownFrom _ -> true) let elem_has_risky = function - | ArrayDeclaration | Assign _ | Global _ | Parameter _ -> + | JavaIntDecleration | ArrayDeclaration | Assign _ | Global _ | Parameter _ -> false | Through {risky_fun} -> Option.is_some risky_fun @@ -155,6 +158,8 @@ module BoTrace = struct let elem_err_desc = function + | JavaIntDecleration -> + "int declaration (java)" | ArrayDeclaration -> "Array declaration" | Assign _ -> diff --git a/infer/src/bufferoverrun/bufferOverrunTypModels.ml b/infer/src/bufferoverrun/bufferOverrunTypModels.ml index 1d20afc16..5a23003bc 100644 --- a/infer/src/bufferoverrun/bufferOverrunTypModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunTypModels.ml @@ -11,6 +11,7 @@ type typ_model = | CArray of {element_typ: Typ.t; deref_kind: Symb.SymbolPath.deref_kind; length: IntLit.t} | CppStdVector of {element_typ: Typ.t} | JavaCollection + | JavaInteger let std_array element_typ length = CArray {element_typ; deref_kind= Symb.SymbolPath.Deref_ArrayIndex; length= IntLit.of_int64 length} @@ -23,13 +24,18 @@ let std_vector element_typ = CppStdVector {element_typ} - each time we add an element, we increase the length of the array - each time we delete an element, we decrease the length of the array *) -let collection = JavaCollection +module Java = struct + let collection = JavaCollection + + let integer = JavaInteger +end let dispatch : (Tenv.t, typ_model) ProcnameDispatcher.TypName.dispatcher = let open ProcnameDispatcher.TypName in make_dispatcher [ -"std" &:: "array" < capt_typ `T &+ capt_int >--> std_array ; -"std" &:: "vector" < capt_typ `T &+ any_typ >--> std_vector - ; +PatternMatch.implements_collection &::.*--> collection - ; +PatternMatch.implements_iterator &::.*--> collection - ; +PatternMatch.implements_org_json "JSONArray" &::.*--> collection ] + ; +PatternMatch.implements_collection &::.*--> Java.collection + ; +PatternMatch.implements_iterator &::.*--> Java.collection + ; +PatternMatch.implements_lang "Integer" &::.*--> Java.integer + ; +PatternMatch.implements_org_json "JSONArray" &::.*--> Java.collection ] diff --git a/infer/src/bufferoverrun/bufferOverrunUtils.ml b/infer/src/bufferoverrun/bufferOverrunUtils.ml index e37725711..1545feffa 100644 --- a/infer/src/bufferoverrun/bufferOverrunUtils.ml +++ b/infer/src/bufferoverrun/bufferOverrunUtils.ml @@ -59,7 +59,7 @@ module Exec = struct | Some (CArray {element_typ; length}) -> decl_local_array model_env loc element_typ ~length:(Some length) ~inst_num ~represents_multiple_values ~dimension mem - | Some (CppStdVector _) | Some JavaCollection | None -> + | Some (CppStdVector _) | Some JavaCollection | Some JavaInteger | None -> (mem, inst_num) ) | _ -> (mem, inst_num) diff --git a/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp index 55123ff5a..2c725bf69 100644 --- a/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp @@ -7,4 +7,4 @@ codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Ar codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.null_pruning2_Good_FP():void, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 10 Size: 5] codetoanalyze/java/bufferoverrun/ArrayMember.java, codetoanalyze.java.bufferoverrun.ArrayMember.load_array_member_Bad():void, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Parameter `this.buf[*]`,Assignment,,Array declaration,Array access: Offset: [max(10, this.buf[*].lb), min(10, this.buf[*].ub)] Size: 10] codetoanalyze/java/bufferoverrun/CompressedData.java, codetoanalyze.java.bufferoverrun.CompressedData.decompressData(codetoanalyze.java.bufferoverrun.CompressedData$D):int, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Parameter `this.yy`,,Parameter `d.cci[*].s`,Assignment,Binary operation: ([0, this.yy - 1] × d.cci[*].s):signed32] -codetoanalyze/java/bufferoverrun/External.java, External.external_function_Bad(external.library.SomeExternalClass):void, 1, INTEGER_OVERFLOW_U5, no_bucket, ERROR, [,Unknown value from: int Integer.intValue(),Assignment,,Unknown value from: int Integer.intValue(),Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed32] +codetoanalyze/java/bufferoverrun/External.java, External.external_function_Bad(external.library.SomeExternalClass):void, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,,Assignment,Binary operation: ([-oo, +oo] + [-oo, +oo]):signed32] diff --git a/infer/tests/codetoanalyze/java/performance/ArrayListTest.java b/infer/tests/codetoanalyze/java/performance/ArrayListTest.java index 2d980d386..7f39ef7aa 100644 --- a/infer/tests/codetoanalyze/java/performance/ArrayListTest.java +++ b/infer/tests/codetoanalyze/java/performance/ArrayListTest.java @@ -187,7 +187,8 @@ public class ArrayListTest { } // Control vars include element which is some intValue and list - // length. Hence, we get quadratic bound. + // length. The result of intValue depends on the list element which + // is not modeled. Hence we get bottom for its value ans 0 cost. // Simplified version of real code https://fburl.com/a3gge1b7 public boolean iterate_over_arraylist_shortcut_FP(ArrayList list) { for (Integer element : list) { diff --git a/infer/tests/codetoanalyze/java/performance/IntTest.java b/infer/tests/codetoanalyze/java/performance/IntTest.java new file mode 100644 index 000000000..2e4f6531f --- /dev/null +++ b/infer/tests/codetoanalyze/java/performance/IntTest.java @@ -0,0 +1,22 @@ +/* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ +class IntTest { + void intValue_linear(Integer mKBytesToSend) { + for (int count = 0; count < mKBytesToSend; count++) {} + } + + static Integer static_Integer; + + static void static_Integer_top() { + for (int count = 0; count < static_Integer; count++) {} + } + + static void valueOf_linear(int p) { + Integer x = p; // call to valueOf + for (int count = 0; count < x; count++) {} + } +} diff --git a/infer/tests/codetoanalyze/java/performance/issues.exp b/infer/tests/codetoanalyze/java/performance/issues.exp index 664c25fce..ef2eb0d6a 100644 --- a/infer/tests/codetoanalyze/java/performance/issues.exp +++ b/infer/tests/codetoanalyze/java/performance/issues.exp @@ -32,18 +32,18 @@ codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_remov codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_set_overrun_bad():void, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Through,Array access: Offset: 1 Size: 1] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.arraylist_set_underrun_bad():void, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 0 Size: 0] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.call_sortArrayList(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 4 + list.length × log(list.length), degree = 1 + 1⋅log,{list.length},call to void ArrayListTest.sortArrayList(ArrayList),Modeled call to Collections.sort,{list.length},call to void ArrayListTest.sortArrayList(ArrayList),Modeled call to Collections.sort] -codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.constructor_add_all(java.util.ArrayList,java.util.ArrayList):void, 4, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 10 + 5 ⋅ (l.length + list.length) + 3 ⋅ (l.length + list.length + 1), degree = 1,{l.length + list.length + 1},Loop at line 245,{l.length + list.length},Loop at line 245] -codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.constructor_add_all_sym(java.util.ArrayList,java.util.ArrayList):void, 4, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 10 + 5 ⋅ (l.length + list.length) + 3 ⋅ (l.length + list.length + 1), degree = 1,{l.length + list.length + 1},Loop at line 252,{l.length + list.length},Loop at line 252] -codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.constructor_linear(java.util.ArrayList):void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 6 + 5 ⋅ list.length + 3 ⋅ (list.length + 1), degree = 1,{list.length + 1},Loop at line 227,{list.length},Loop at line 227] -codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.constructor_modify(java.util.ArrayList):void, 8, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 18 + 5 ⋅ (list.length + 4) + 3 ⋅ (list.length + 5), degree = 1,{list.length + 5},Loop at line 238,{list.length + 4},Loop at line 238] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.constructor_add_all(java.util.ArrayList,java.util.ArrayList):void, 4, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 10 + 5 ⋅ (l.length + list.length) + 3 ⋅ (l.length + list.length + 1), degree = 1,{l.length + list.length + 1},Loop at line 246,{l.length + list.length},Loop at line 246] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.constructor_add_all_sym(java.util.ArrayList,java.util.ArrayList):void, 4, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 10 + 5 ⋅ (l.length + list.length) + 3 ⋅ (l.length + list.length + 1), degree = 1,{l.length + list.length + 1},Loop at line 253,{l.length + list.length},Loop at line 253] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.constructor_linear(java.util.ArrayList):void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 6 + 5 ⋅ list.length + 3 ⋅ (list.length + 1), degree = 1,{list.length + 1},Loop at line 228,{list.length},Loop at line 228] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.constructor_modify(java.util.ArrayList):void, 8, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 18 + 5 ⋅ (list.length + 4) + 3 ⋅ (list.length + 5), degree = 1,{list.length + 5},Loop at line 239,{list.length + 4},Loop at line 239] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 5 + 5 ⋅ list.length, degree = 1,{list.length},Loop at line 14] -codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist_shortcut_FP(java.util.ArrayList):boolean, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 4 + 11 ⋅ (list.length - 1) + 2 ⋅ (list.length - 1) × (-Integer.intValue().lb + 11) + 3 ⋅ list.length × (-Integer.intValue().lb + 11), degree = 2,{-Integer.intValue().lb + 11},Loop at line 193,{list.length},Loop at line 193,{-Integer.intValue().lb + 11},Loop at line 193,{list.length - 1},Loop at line 193] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist_shortcut_FP(java.util.ArrayList):boolean, 0, ZERO_EXECUTION_TIME, no_bucket, ERROR, [] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_arraylist_with_inner(java.util.ArrayList):void, 3, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 7 + 11 ⋅ (list1.length - 1) + 3 ⋅ list1.length, degree = 1,{list1.length},Loop at line 184,{list1.length - 1},Loop at line 184] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_over_local_arraylist(java.util.ArrayList):void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 7 + 5 ⋅ list.length, degree = 1,{list.length},Loop at line 19] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_while_has_next(java.util.ArrayList):void, 3, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 4 + 10 ⋅ (list.length - 1) + 3 ⋅ list.length, degree = 1,{list.length},Loop at line 176,{list.length - 1},Loop at line 176] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.iterate_with_iterator(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 4 + 8 ⋅ (list.length - 1) + 3 ⋅ list.length, degree = 1,{list.length},Loop at line 170,{list.length - 1},Loop at line 170] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.max_linear(java.util.ArrayList):Person, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 8 + people.length, degree = 1,{people.length},Modeled call to Collections.max] -codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.remove_string_from_list(java.lang.String):boolean, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 5 + 12 ⋅ (this.list.length - 1) + 3 ⋅ this.list.length, degree = 1,{this.list.length},Loop at line 216,{this.list.length - 1},Loop at line 216] +codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.remove_string_from_list(java.lang.String):boolean, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 5 + 12 ⋅ (this.list.length - 1) + 3 ⋅ this.list.length, degree = 1,{this.list.length},Loop at line 217,{this.list.length - 1},Loop at line 217] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.sortArrayList(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + list.length × log(list.length), degree = 1 + 1⋅log,{list.length},Modeled call to Collections.sort,{list.length},Modeled call to Collections.sort] codetoanalyze/java/performance/ArrayListTest.java, ArrayListTest.sort_comparator_nlogn(java.util.ArrayList):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 8 + people.length × log(people.length), degree = 1 + 1⋅log,{people.length},Modeled call to Collections.sort,{people.length},Modeled call to Collections.sort] codetoanalyze/java/performance/Break.java, codetoanalyze.java.performance.Break.break_constant(int):int, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 10 + 7 ⋅ p, degree = 1,{p},call to int Break.break_loop(int,int),Loop at line 12] @@ -108,6 +108,10 @@ codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performan codetoanalyze/java/performance/Cost_test_deps.java, codetoanalyze.java.performance.Cost_test_deps.two_loops():int, 7, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 545, degree = 0] codetoanalyze/java/performance/EvilCfg.java, EvilCfg.foo(int,int,boolean):void, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded loop,Loop at line 15] codetoanalyze/java/performance/FieldAccess.java, codetoanalyze.java.performance.FieldAccess.iterate_upto_field_size(codetoanalyze.java.performance.FieldAccess$Test):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 6 ⋅ test.a, degree = 1,{test.a},Loop at line 16] +codetoanalyze/java/performance/IntTest.java, IntTest.intValue_linear(java.lang.Integer):void, 1, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 5 ⋅ mKBytesToSend + 3 ⋅ (1+max(0, mKBytesToSend)), degree = 1,{1+max(0, mKBytesToSend)},Loop at line 9,{mKBytesToSend},Loop at line 9] +codetoanalyze/java/performance/IntTest.java, IntTest.static_Integer_top():void, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded loop,Loop at line 15] +codetoanalyze/java/performance/IntTest.java, IntTest.static_Integer_top():void, 1, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Assignment,Binary operation: ([0, +oo] + 1):signed32] +codetoanalyze/java/performance/IntTest.java, IntTest.valueOf_linear(int):void, 2, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 5 + 5 ⋅ p + 3 ⋅ (1+max(0, p)), degree = 1,{1+max(0, p)},Loop at line 20,{p},Loop at line 20] codetoanalyze/java/performance/Invariant.java, Invariant.do_while_invariant(int,int):void, 3, EXPENSIVE_EXECUTION_TIME, no_bucket, ERROR, [with estimated cost 2 + 3 ⋅ (k - 1) + 4 ⋅ (max(1, k)), degree = 1,{max(1, k)},Loop at line 58,{k - 1},Loop at line 58] codetoanalyze/java/performance/Invariant.java, Invariant.formal_not_invariant_FP(int,int):void, 0, INFINITE_EXECUTION_TIME, no_bucket, ERROR, [Unbounded loop,Loop at line 31] codetoanalyze/java/performance/Invariant.java, Invariant.formal_not_invariant_FP(int,int):void, 2, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [,Parameter `x`,,Parameter `x`,Binary operation: (size + [-oo, +oo]):signed32]