diff --git a/infer/tests/codetoanalyze/java/bufferoverrun/ArrayListTest.java b/infer/tests/codetoanalyze/java/bufferoverrun/ArrayListTest.java index 7b058ad18..954aa2ba5 100644 --- a/infer/tests/codetoanalyze/java/bufferoverrun/ArrayListTest.java +++ b/infer/tests/codetoanalyze/java/bufferoverrun/ArrayListTest.java @@ -242,4 +242,34 @@ class ArrayListTest { b.get(0); // size of b should be [0, 2] } } + + interface MyI { + public ArrayList mk_unknown(); + } + + boolean unknown_bool2; + ArrayList unknown_array_list1; + ArrayList unknown_array_list2; + + void loop_on_unknown_iterator_FN(MyI x, int j) { + ArrayList a = new ArrayList<>(); + ArrayList b; + if (unknown_bool) { + b = a; + } else { + b = x.mk_unknown(); + } + // `b` points to an zero-sized array and `Unknown` pointer here. By `b.hasNext()`, the size of + // the array list is pruned incorrectly to [0,-1]. + for (Integer i : b) { + // Both branches are unreachable since `a.size()` is an invalid [0,-1]. + if (a.size() <= -1) { + int[] c = new int[5]; + c[5] = 0; + } else { + int[] c = new int[5]; + c[5] = 0; + } + } + } } diff --git a/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp index 110b53f3d..bb77f1b74 100644 --- a/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp @@ -20,6 +20,9 @@ codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.add_in_loop_i codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.alias_join_bad():void, 10, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.alias_join_bad():void, 11, BUFFER_OVERRUN_L3, no_bucket, ERROR, [,Array declaration,Array access: Offset: 0 Size: [0, 2]] codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.alloc_is_negative_bad():void, 0, INFERBO_ALLOC_IS_NEGATIVE, no_bucket, ERROR, [Allocation: Length: -1] +codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.loop_on_unknown_iterator_FN(ArrayListTest$MyI,int):void, 9, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: ArrayList ArrayListTest$MyI.mk_unknown(),Assignment,Array access: Offset: [-oo, +oo] Size: [0, +oo]] +codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.loop_on_unknown_iterator_FN(ArrayListTest$MyI,int):void, 11, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] +codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.loop_on_unknown_iterator_FN(ArrayListTest$MyI,int):void, 11, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here] codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.multi_adds_in_loop_iterator_bad(java.util.ArrayList):void, 7, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Parameter `b.elements[*]`,Assignment,,Array declaration,Array access: Offset: b.length + 1 Size: b.length] codetoanalyze/java/bufferoverrun/ArrayListTest.java, ArrayListTest.remove_in_loop_iterator_good_FP(java.util.ArrayList):void, 13, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Parameter `b.elements[*]`,Assignment,,Parameter `b.elements[*]`,Array access: Offset: b.length Size: b.length] codetoanalyze/java/bufferoverrun/ArrayMember.java, codetoanalyze.java.bufferoverrun.ArrayMember.load_array_member_Bad():void, 3, 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]