diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index dcbef3e93..b0497bf09 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -727,6 +727,14 @@ module LatestPrune = struct | TrueBranch (x', ptrue), FalseBranch (y', pfalse) when Pvar.equal x' y' -> V (x', ptrue, pfalse) + | TrueBranch (x1, ptrue1), V (x2, ptrue2, pfalse) + | V (x2, ptrue2, pfalse), TrueBranch (x1, ptrue1) + when Pvar.equal x1 x2 -> + V (x1, PrunePairs.join ptrue1 ptrue2, pfalse) + | FalseBranch (x1, pfalse1), V (x2, ptrue, pfalse2) + | V (x2, ptrue, pfalse2), FalseBranch (x1, pfalse1) + when Pvar.equal x1 x2 -> + V (x1, ptrue, PrunePairs.join pfalse1 pfalse2) | V (x1, ptrue1, pfalse1), V (x2, ptrue2, pfalse2) when Pvar.equal x1 x2 -> V (x1, PrunePairs.join ptrue1 ptrue2, PrunePairs.join pfalse1 pfalse2) | _, _ -> diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index bd91a1ae7..173653a78 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -197,6 +197,7 @@ codetoanalyze/c/bufferoverrun/pointer_arith.c, pointer_arith_bad, 4, BUFFER_OVER codetoanalyze/c/bufferoverrun/prune_alias.c, FP_prune_alias_exp_Ok, 4, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 1 Size: 1] codetoanalyze/c/bufferoverrun/prune_alias.c, bad_if_alias, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 1 Size: 1] codetoanalyze/c/bufferoverrun/prune_alias.c, bad_if_not_alias, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 1 Size: 1] +codetoanalyze/c/bufferoverrun/prune_alias.c, call_latest_prune_join_3_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Call,,Parameter `n`,,Parameter `*a`,Array access: Offset: 3 Size: 2 by call to `latest_prune_join` ] codetoanalyze/c/bufferoverrun/prune_alias.c, call_prune_arrblk_ne_Bad, 2, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Array declaration,Assignment,Call,,Parameter `*x`,Array access: Offset: 5 Size: 5 by call to `prune_arrblk_ne` ] codetoanalyze/c/bufferoverrun/prune_alias.c, loop_prune2_Good_FP, 8, BUFFER_OVERRUN_L2, no_bucket, ERROR, [,Parameter `length`,,Parameter `length`,Array declaration,Array access: Offset: [length - length + 1, length] Size: length] codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_and_Ok, 3, CONDITION_ALWAYS_FALSE, no_bucket, WARNING, [Here] diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c b/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c index d735b5867..ea33697ac 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c @@ -227,3 +227,40 @@ void call_bad_if_not_alias_Bad_AlreadyReported() { int x, y; bad_if_not_alias(x, y); } + +int unknown_function(); + +void latest_prune_join(int* a, int n) { + int x; + if (unknown_function()) { + if (n < 4) { + x = 1; + } else { + x = 0; + } + } else { + if (n < 5) { + x = 1; + } else { + return; + } + } + if (x) { + a[n] = 0; + } +} + +void call_latest_prune_join_1_Good() { + int a[5]; + latest_prune_join(a, 3); +} + +void call_latest_prune_join_2_Good() { + int a[5]; + latest_prune_join(a, 10); +} + +void call_latest_prune_join_3_Bad() { + int a[2]; + latest_prune_join(a, 3); +}