diff --git a/infer/src/bufferoverrun/arrayBlk.ml b/infer/src/bufferoverrun/arrayBlk.ml index 75920371d..e66cee56e 100644 --- a/infer/src/bufferoverrun/arrayBlk.ml +++ b/infer/src/bufferoverrun/arrayBlk.ml @@ -87,6 +87,10 @@ module ArrInfo = struct fun arr1 arr2 -> {arr1 with offset= Itv.prune_eq arr1.offset arr2.offset} + let prune_ne : t -> t -> t = + fun arr1 arr2 -> {arr1 with offset= Itv.prune_ne arr1.offset arr2.offset} + + let set_size : Itv.t -> t -> t = fun size arr -> {arr with size} end @@ -156,4 +160,6 @@ let prune_comp : Binop.t -> astate -> astate -> astate = let prune_eq : astate -> astate -> astate = fun a1 a2 -> do_prune ArrInfo.prune_eq a1 a2 +let prune_ne : astate -> astate -> astate = fun a1 a2 -> do_prune ArrInfo.prune_ne a1 a2 + let set_size : Itv.t -> astate -> astate = fun size a -> map (ArrInfo.set_size size) a diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index dbb5253cc..e29d276c7 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -193,7 +193,7 @@ module Val = struct let prune_eq : t -> t -> t = lift_prune2 Itv.prune_eq ArrayBlk.prune_eq - let prune_ne : t -> t -> t = lift_prune2 Itv.prune_ne ArrayBlk.prune_eq + let prune_ne : t -> t -> t = lift_prune2 Itv.prune_ne ArrayBlk.prune_ne let lift_pi : (ArrayBlk.astate -> Itv.t -> ArrayBlk.astate) -> t -> t -> t = fun f x y -> {bot with arrayblk= f x.arrayblk y.itv; traces= TraceSet.join x.traces y.traces} diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index dc89322a6..d9699a108 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -59,7 +59,9 @@ codetoanalyze/c/bufferoverrun/nested_loop.c, nested_loop, 7, BUFFER_OVERRUN_L2, codetoanalyze/c/bufferoverrun/nested_loop_with_label.c, nested_loop_with_label, 6, BUFFER_OVERRUN_L4, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, +oo] Size: [10, 10]] codetoanalyze/c/bufferoverrun/pointer_arith.c, array_pointer_arith_Bad, 3, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [10, 10] Size: [10, 10]] codetoanalyze/c/bufferoverrun/pointer_arith.c, pointer_arith_bad, 4, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [10, 10] Size: [10, 10]] +codetoanalyze/c/bufferoverrun/prune_alias.c, FP_call_prune_arrblk_eq_Ok, 2, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,Assignment,Call,Parameter: x,ArrayAccess: Offset: [15, 5] Size: [5, 5] @ codetoanalyze/c/bufferoverrun/prune_alias.c:135:5 by call to `prune_arrblk_eq()` ] codetoanalyze/c/bufferoverrun/prune_alias.c, FP_prune_alias_exp_Ok, 4, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,ArrayAccess: Offset: [1, 1] Size: [1, 1]] +codetoanalyze/c/bufferoverrun/prune_alias.c, call_prune_arrblk_ne_Bad, 2, BUFFER_OVERRUN_L1, ERROR, [ArrayDeclaration,Assignment,Call,Parameter: x,ArrayAccess: Offset: [5, 5] Size: [5, 5] @ codetoanalyze/c/bufferoverrun/prune_alias.c:117:5 by call to `prune_arrblk_ne()` ] codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_and_Ok, 3, CONDITION_ALWAYS_FALSE, WARNING, [] codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_and_Ok, 3, CONDITION_ALWAYS_TRUE, WARNING, [] codetoanalyze/c/bufferoverrun/prune_alias.c, prune_alias_eq_Ok, 3, CONDITION_ALWAYS_TRUE, WARNING, [] diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c b/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c index 26c0012fb..4c15f314d 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/prune_alias.c @@ -107,3 +107,36 @@ void FP_prune_alias_exp_Ok(int x) { a[1] = 0; } } + +#include + +void prune_arrblk_ne(int* x) { + int* y = x + 10; + + if (x != y) { + x[5] = 1; + } +} + +void call_prune_arrblk_ne_Ok() { + int* x = (int*)malloc(sizeof(int) * 10); + prune_arrblk_ne(x); +} + +void call_prune_arrblk_ne_Bad() { + int* x = (int*)malloc(sizeof(int) * 5); + prune_arrblk_ne(x); +} + +void prune_arrblk_eq(int* x) { + int* y = x + 10; + + if (x == y) { + x[5] = 1; /* unreachable */ + } +} + +void FP_call_prune_arrblk_eq_Ok() { + int* x = (int*)malloc(sizeof(int) * 5); + prune_arrblk_eq(x); +}