[inferbo] Symbolic length for no-size flexible arrays

Reviewed By: jvillard

Differential Revision: D13450086

fbshipit-source-id: 645412be2

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
 

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);
 }

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,<Offset trace>,Parameter `n`,<Length trace>,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, [<Length trace>,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, [<Length trace>,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,<Offset trace>,Parameter `i`,<Length trace>,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,<Offset trace>,Parameter `i`,<Length trace>,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,<Offset trace>,Assignment,<Length trace>,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, [<Offset trace>,Assignment,Call,Parameter `m`,Assignment,<Length trace>,Array declaration,Array access: Offset: 15 Size: 10]
 codetoanalyze/c/bufferoverrun/for_loop.c, for_loop, 10, BUFFER_OVERRUN_L3, no_bucket, ERROR, [<Offset trace>,Assignment,<Length trace>,Call,Array declaration,Assignment,Assignment,Assignment,Array access: Offset: [0, 9] Size: [5, 10]]