infer_clone/infer/tests/codetoanalyze/java/bufferoverrun/issues.exp

codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.collection_remove_from_empty_Bad():java.util.ArrayList, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 0 Size: 0]
codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.null_pruning1_Bad():void, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.null_pruning1_Bad():void, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Assignment,Assignment,Array access: Offset: 10 Size: 5]
codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.null_pruning1_Good():void, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.null_pruning2_Bad():void, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Assignment,Assignment,Array access: Offset: 10 Size: 5]
codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.null_pruning2_Good_FP():void, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Assignment,Assignment,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, [<Offset trace>,Parameter `this.buf[*]`,Assignment,<Length trace>,Array declaration,Assignment,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, [<LHS trace>,Assignment,<RHS trace>,Parameter `d.cci[*].s`,Assignment,Binary operation: ([0, this.yy - 1] × d.cci[*].s):signed32]
-												[inferbo] Model Java collections using arrays

Reviewed By: ezgicicek, skcho

Differential Revision: D13190960

fbshipit-source-id: fba435f34

											
										
										
											6 years ago
+								codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.collection_remove_from_empty_Bad():java.util.ArrayList, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Array access: Offset: 0 Size: 0]
-												[inferbo] Prune (p=null)

Summary: This diff unset powloc and arrayblk values of p when assume(p==Null).

Reviewed By: mbouaziz, jvillard

Differential Revision: D13415366

fbshipit-source-id: a491a957f

											
										
										
											6 years ago
+								codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.null_pruning1_Bad():void, 2, CONDITION_ALWAYS_TRUE, no_bucket, WARNING, [Here]
 								codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.null_pruning1_Bad():void, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Assignment,Assignment,Array access: Offset: 10 Size: 5]
 								codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.null_pruning1_Good():void, 2, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here]
 								codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.null_pruning2_Bad():void, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Assignment,Assignment,Array access: Offset: 10 Size: 5]
 								codetoanalyze/java/bufferoverrun/Array.java, codetoanalyze.java.bufferoverrun.Array.null_pruning2_Good_FP():void, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Length trace>,Array declaration,Assignment,Assignment,Array access: Offset: 10 Size: 5]
-												[inferbo] Fix array member access in Java

Summary: In SIL, Java's array member is a pointer to an array, while C++'s is the array itself.  This diff differentiate them in evaluating abstract locations.

Reviewed By: ezgicicek, mbouaziz

Differential Revision: D14021451

fbshipit-source-id: 00f14fe3b

											
										
										
											6 years ago
+								codetoanalyze/java/bufferoverrun/ArrayMember.java, codetoanalyze.java.bufferoverrun.ArrayMember.load_array_member_Bad():void, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [<Offset trace>,Parameter `this.buf[*]`,Assignment,<Length trace>,Array declaration,Assignment,Array access: Offset: [max(10, this.buf[*].lb), min(10, this.buf[*].ub)] Size: 10]
-												[inferbo] Symbols for one value

Summary:
For abstract values representing one concrete value, create only one symbol instead of two.
Still create two symbols (lb, ub) for abstract values representing multiple concrete values (like array cells).

As a consequence, comparisons of symbolic values are more precise (we can even prove equality). I expect to remove a bunch of FPs.
Another consequence is the disappearance of `.lb` and `.ub` in many reports.

Reviewed By: skcho

Differential Revision: D13072084

fbshipit-source-id: 9bc0b9881

											
										
										
											6 years ago
+								codetoanalyze/java/bufferoverrun/CompressedData.java, codetoanalyze.java.bufferoverrun.CompressedData.decompressData(codetoanalyze.java.bufferoverrun.CompressedData$D):int, 9, INTEGER_OVERFLOW_L5, no_bucket, ERROR, [<LHS trace>,Assignment,<RHS trace>,Parameter `d.cci[*].s`,Assignment,Binary operation: ([0, this.yy - 1] × d.cci[*].s):signed32]