From e5ee27af20998d6484e7c6628441c42599fe7aff Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Fri, 8 Sep 2017 22:35:17 -0700 Subject: [PATCH] [Inferbo] Bugfix: incorrect pruning for unary negation Reviewed By: jvillard Differential Revision: D5716888 fbshipit-source-id: abc1e54 --- infer/src/bufferoverrun/bufferOverrunSemantics.ml | 2 +- infer/tests/codetoanalyze/c/bufferoverrun/issues.exp | 3 +++ .../tests/codetoanalyze/c/bufferoverrun/prune_constant.c | 8 ++++++++ 3 files changed, 12 insertions(+), 1 deletion(-) diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index af71646f2..00d1646d4 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -325,7 +325,7 @@ module Make (CFG : ProcCfg.S) = struct match Mem.find_alias x mem with | Some lv -> let v = Mem.find_heap lv mem in - let itv_v = Itv.prune_ne (Val.get_itv v) Itv.false_sem in + let itv_v = Itv.prune_eq (Val.get_itv v) Itv.false_sem in let v' = Val.modify_itv itv_v v in Mem.update_mem (PowLoc.singleton lv) v' mem | None diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index 17a868b5e..aea7bb4b8 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -47,6 +47,9 @@ codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_not_Ok, 11, CONDITION_A codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_or_Ok, 3, CONDITION_ALWAYS_FALSE, [] codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_or_Ok, 3, CONDITION_ALWAYS_FALSE, [] codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_false_Ok, 3, CONDITION_ALWAYS_FALSE, [] +codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_not_Bad, 3, CONDITION_ALWAYS_FALSE, [] +codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_not_Bad, 3, CONDITION_ALWAYS_TRUE, [] +codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_not_Bad, 4, BUFFER_OVERRUN, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [1, 1] Size: [1, 1]] codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_true_Ok, 3, CONDITION_ALWAYS_TRUE, [] codetoanalyze/c/bufferoverrun/prune_constant.c, prune_constant_value_Ok, 3, CONDITION_ALWAYS_FALSE, [] codetoanalyze/c/bufferoverrun/sizeof.c, eval_sizeof_bad, 1, CONDITION_ALWAYS_TRUE, [] diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/prune_constant.c b/infer/tests/codetoanalyze/c/bufferoverrun/prune_constant.c index 40bf96cbc..436757c5f 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/prune_constant.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/prune_constant.c @@ -36,3 +36,11 @@ void prune_constant_value_Ok(int x) { } } } + +void prune_constant_not_Bad() { + int x = 0; + int a[1]; + if (!x) { + a[x + 1] = 0; + } +}