[pulse] Ignore array elements in uninitialized value check

Summary:
In practice, it is not easy to mark all of NOT initialized elements of array, so let's ignore the
array value at the moment.

Reviewed By: jvillard

Differential Revision: D25372449

fbshipit-source-id: 02b2e217c

infer/src/pulse/PulseAbductiveDomain.ml

@@ -492,10 +492,7 @@ let rec set_uninitialized_post tenv src typ location (post : PostDomain.t) =
               in
               PostDomain.update ~stack ~heap acc
               |> set_uninitialized_post tenv (`Malloc field_addr) field_typ location ) )
-  | Tarray _ ->
-      (* TODO: set uninitialized attributes for elements *)
-      post
-  | Tvoid | Tfun | TVar _ ->
+  | Tarray _ | Tvoid | Tfun | TVar _ ->
       (* We ignore tricky types to mark uninitialized addresses. *)
       post
 

infer/tests/codetoanalyze/c/pulse/uninit.c

@@ -102,6 +102,7 @@ void malloc_array_good(int len) {
   char* o = (char*)malloc(len);
   if (o) {
     o[0] = 'a';
+    char c = o[0];
   }
   free(o);
 }
@@ -116,3 +117,26 @@ void havoc_calling_unknown_struct_good() {
   struct uninit_s x = unknown_wrapper();
   int y = x.f1;
 }
+
+void malloc_array_bad_FN(int len) {
+  char* o = (char*)malloc(len);
+  if (o) {
+    o[0] = 'a';
+    char c = o[1];
+  }
+  free(o);
+}
+
+void local_array_good() {
+  char o[10];
+  o[0] = 'a';
+  char c = o[0];
+  free(o);
+}
+
+void local_array_bad_FN() {
+  char o[10];
+  o[0] = 'a';
+  char c = o[1];
+  free(o);
+}