From 8fd04d53123555490271844de96ec2d9d0ad5d5f Mon Sep 17 00:00:00 2001 From: Sungkeun Cho Date: Wed, 7 Mar 2018 17:56:08 -0800 Subject: [PATCH] [inferbo][bugfix] Add index to offset at array fields Summary: It corrects a bug that `&(x.f[n])` was evaluated to `&(x.f[0])`. Reviewed By: mbouaziz Differential Revision: D7179620 fbshipit-source-id: 04cbaa7 --- infer/src/bufferoverrun/bufferOverrunSemantics.ml | 2 +- .../codetoanalyze/c/bufferoverrun/array_field.c | 13 +++++++++++++ .../tests/codetoanalyze/c/bufferoverrun/issues.exp | 1 + 3 files changed, 15 insertions(+), 1 deletion(-) diff --git a/infer/src/bufferoverrun/bufferOverrunSemantics.ml b/infer/src/bufferoverrun/bufferOverrunSemantics.ml index b9aa1d47d..547dc85cc 100644 --- a/infer/src/bufferoverrun/bufferOverrunSemantics.ml +++ b/infer/src/bufferoverrun/bufferOverrunSemantics.ml @@ -230,7 +230,7 @@ module Make (CFG : ProcCfg.S) = struct the memory section using the abstract memory, though the memory lookup is not required to evaluate the address of x.f[n] in the concrete semantics. *) - Mem.find_set (Val.get_pow_loc array_v) mem + Val.plus_pi (Mem.find_set (Val.get_pow_loc array_v) mem) index_v | _ -> Val.of_pow_loc PowLoc.unknown else arr diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/array_field.c b/infer/tests/codetoanalyze/c/bufferoverrun/array_field.c index 386bf1693..5425b3011 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/array_field.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/array_field.c @@ -23,3 +23,16 @@ void array_field_access_Bad(struct S1 x, struct S1 y) { x.f[0] = 1; a[y.f[0]] = 0; } + +void decreasing_pointer_Good(struct S1* x) { + int* p = &(x->f[1]); + p--; + *p = 0; +} + +void decreasing_pointer_Bad(struct S1* x) { + int* p = &(x->f[1]); + p--; + p--; + *p = 0; +} diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index e909ca61b..5c4267f6d 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -2,6 +2,7 @@ codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_Bad, 2, BUFFER_OVERRUN_L3, codetoanalyze/c/bufferoverrun/arith.c, modulo_signed_neg_Bad, 2, BUFFER_OVERRUN_L3, [ArrayDeclaration,ArrayAccess: Offset: [-4, 4] Size: [5, 5]] codetoanalyze/c/bufferoverrun/array_dynlength.c, init_variable_array, 3, BUFFER_OVERRUN_L2, [Offset: [3xs$0 + 1, 3xs$1 + 1] Size: [3xs$0 + 1, 3xs$1 + 1]] codetoanalyze/c/bufferoverrun/array_field.c, array_field_access_Bad, 4, BUFFER_OVERRUN_L1, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [20, 20] Size: [10, 10]] +codetoanalyze/c/bufferoverrun/array_field.c, decreasing_pointer_Bad, 4, BUFFER_OVERRUN_L1, [Assignment,Assignment,Assignment,ArrayAccess: Offset: [-1, -1] Size: [2, 2]] codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 4, CONDITION_ALWAYS_TRUE, [] codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 13, CONDITION_ALWAYS_TRUE, [] codetoanalyze/c/bufferoverrun/break_continue_return.c, break_continue_return, 16, BUFFER_OVERRUN_L2, [ArrayDeclaration,Assignment,ArrayAccess: Offset: [0, 10] Size: [10, 10]]