[inferbo] New test + more debug

Reviewed By: jvillard

Differential Revision: D13450070

fbshipit-source-id: d6f53baca

infer/src/bufferoverrun/bufferOverrunDomain.ml

@@ -343,6 +343,9 @@ module Val = struct
 
   let of_path ~may_last_field integer_type_widths location typ path =
     let is_java = Language.curr_language_is Java in
+    L.d_printfln "Val.of_path %a : %a%s%s" SPath.pp_partial path (Typ.pp Pp.text) typ
+      (if may_last_field then ", may_last_field" else "")
+      (if is_java then ", is_java" else "") ;
     match typ.Typ.desc with
     | Tint _ | Tfloat _ | Tvoid | Tfun _ | TVar _ ->
         let l = Loc.of_path path in
@@ -395,11 +398,20 @@ module Val = struct
 
   let on_demand : default:t -> OndemandEnv.t -> Loc.t -> t =
    fun ~default {typ_of_param_path; may_last_field; entry_location; integer_type_widths} l ->
-    Option.value_map (Loc.get_path l) ~default ~f:(fun path ->
-        Option.value_map (typ_of_param_path path) ~default ~f:(fun typ ->
-            let may_last_field = may_last_field path in
-            let path = OndemandEnv.canonical_path typ_of_param_path path in
-            of_path ~may_last_field integer_type_widths entry_location typ path ) )
+    match Loc.get_path l with
+    | None ->
+        L.d_printfln "Val.on_demand for %a -> no path" Loc.pp l ;
+        default
+    | Some path -> (
+      match typ_of_param_path path with
+      | None ->
+          L.d_printfln "Val.on_demand for %a -> no type" Loc.pp l ;
+          default
+      | Some typ ->
+          L.d_printfln "Val.on_demand for %a" Loc.pp l ;
+          let may_last_field = may_last_field path in
+          let path = OndemandEnv.canonical_path typ_of_param_path path in
+          of_path ~may_last_field integer_type_widths entry_location typ path )
 
 
   module Itv = struct

infer/tests/codetoanalyze/c/bufferoverrun/flexible_array.c

@@ -0,0 +1,27 @@
+/*
+ * Copyright (c) 2018-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+#include <stdlib.h>
+
+struct s {
+  int useless_field_because_flexible_array_members_are_not_allowed_in_otherwise_empty_struct;
+  int arr[];
+};
+
+void access_to_incomplete_array_type(struct s* a, int i) { a->arr[i] = 0; }
+
+void call_access_to_incomplete_array_type_Good_FP() {
+  struct s* x = malloc(sizeof(struct s) + sizeof(int));
+  access_to_incomplete_array_type(x, 0);
+}
+
+void call_access_to_incomplete_array_type_Bad() {
+  struct s* x = malloc(sizeof(struct s) + sizeof(int));
+  access_to_incomplete_array_type(x, 1);
+}
+
+// For tests with last field of size 0 or 1, see class.cpp

infer/tests/codetoanalyze/c/bufferoverrun/issues.exp

@@ -82,6 +82,8 @@ 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]]