From fd8b4795b878c8efc026a18f9093252195be1862 Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Fri, 14 Dec 2018 05:05:47 -0800 Subject: [PATCH] [inferbo] Symbolic length for no-size flexible arrays Reviewed By: jvillard Differential Revision: D13450086 fbshipit-source-id: 645412be2 --- infer/src/bufferoverrun/bufferOverrunDomain.ml | 13 +++++++++---- .../codetoanalyze/c/bufferoverrun/flexible_array.c | 4 ++-- .../tests/codetoanalyze/c/bufferoverrun/issues.exp | 2 -- 3 files changed, 11 insertions(+), 8 deletions(-) diff --git a/infer/src/bufferoverrun/bufferOverrunDomain.ml b/infer/src/bufferoverrun/bufferOverrunDomain.ml index 70b7e72d0..6d795654f 100644 --- a/infer/src/bufferoverrun/bufferOverrunDomain.ml +++ b/infer/src/bufferoverrun/bufferOverrunDomain.ml @@ -386,10 +386,15 @@ module Val = struct let stride = Option.map stride ~f:(fun n -> IntLit.to_int_exn n) in let offset = Itv.zero in let size = - Option.value_map length ~default:Itv.top ~f:(fun length -> - if may_last_field && (IntLit.iszero length || IntLit.isone length) then - Itv.of_length_path path - else Itv.of_big_int (IntLit.to_big_int length) ) + match length with + | None (* IncompleteArrayType, no-size flexible array *) -> + Itv.of_length_path path + | Some length + when may_last_field && (IntLit.iszero length || IntLit.isone length) + (* 0/1-sized flexible array *) -> + Itv.of_length_path path + | Some length -> + Itv.of_big_int (IntLit.to_big_int length) in of_array_alloc allocsite ~stride ~offset ~size ~traces diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/flexible_array.c b/infer/tests/codetoanalyze/c/bufferoverrun/flexible_array.c index 6123cc4a0..bc410a8aa 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/flexible_array.c +++ b/infer/tests/codetoanalyze/c/bufferoverrun/flexible_array.c @@ -14,12 +14,12 @@ struct s { void access_to_incomplete_array_type(struct s* a, int i) { a->arr[i] = 0; } -void call_access_to_incomplete_array_type_Good_FP() { +void call_access_to_incomplete_array_type_Good() { struct s* x = malloc(sizeof(struct s) + sizeof(int)); access_to_incomplete_array_type(x, 0); } -void call_access_to_incomplete_array_type_Bad() { +void call_access_to_incomplete_array_type_Bad_FN() { struct s* x = malloc(sizeof(struct s) + sizeof(int)); access_to_incomplete_array_type(x, 1); } diff --git a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp index d700d568a..d8485fb8a 100644 --- a/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/c/bufferoverrun/issues.exp @@ -82,8 +82,6 @@ codetoanalyze/c/bufferoverrun/duplicates.c, tsa_two_alarms_Bad, 0, BUFFER_OVERRU codetoanalyze/c/bufferoverrun/duplicates.c, tsa_two_alarms_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `n`,,Array declaration,Array access: Offset: 1 Size: 1 by call to `two_symbolic_accesses` ] codetoanalyze/c/bufferoverrun/external.c, extern_bad, 5, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: lib,Assignment,Array access: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/c/bufferoverrun/external.c, extern_bad, 10, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 30 Size: 10] -codetoanalyze/c/bufferoverrun/flexible_array.c, call_access_to_incomplete_array_type_Bad, 2, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,,Parameter `i`,,Parameter `a->arr[*]`,Array access: Offset: 1 Size: [0, +oo] by call to `access_to_incomplete_array_type` ] -codetoanalyze/c/bufferoverrun/flexible_array.c, call_access_to_incomplete_array_type_Good_FP, 2, BUFFER_OVERRUN_L5, no_bucket, ERROR, [Call,,Parameter `i`,,Parameter `a->arr[*]`,Array access: Offset: 0 Size: [0, +oo] by call to `access_to_incomplete_array_type` ] codetoanalyze/c/bufferoverrun/for_loop.c, call_initialize_arr_Bad, 2, BUFFER_OVERRUN_L2, no_bucket, ERROR, [Array declaration,Call,,Assignment,,Parameter `*arr`,Array access: Offset: [0, 19] Size: 10 by call to `initialize_arr` ] codetoanalyze/c/bufferoverrun/for_loop.c, call_two_loops_Bad, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Assignment,Call,Parameter `m`,Assignment,,Array declaration,Array access: Offset: 15 Size: 10] codetoanalyze/c/bufferoverrun/for_loop.c, for_loop, 10, BUFFER_OVERRUN_L3, no_bucket, ERROR, [,Assignment,,Call,Array declaration,Assignment,Assignment,Assignment,Array access: Offset: [0, 9] Size: [5, 10]]