diff --git a/infer/src/pulse/PulseAbductiveDomain.ml b/infer/src/pulse/PulseAbductiveDomain.ml index aa38cff7b..d454ba1c3 100644 --- a/infer/src/pulse/PulseAbductiveDomain.ml +++ b/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 diff --git a/infer/tests/codetoanalyze/c/pulse/uninit.c b/infer/tests/codetoanalyze/c/pulse/uninit.c index f8f26fccf..95d04bd05 100644 --- a/infer/tests/codetoanalyze/c/pulse/uninit.c +++ b/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); +}