From 99a58e691d65b012d642d1f018dde518230da44a Mon Sep 17 00:00:00 2001 From: Andrzej Kotulski Date: Tue, 24 May 2016 09:18:34 -0700 Subject: [PATCH] Report empty vector access in tabulation.ml Summary: I missed that codepath and it lead to NULL_DEREFERENCE errors when in fact they should be EMPTY_VECTOR_ACCESS Reviewed By: jvillard Differential Revision: D3340627 fbshipit-source-id: 52ae85f --- infer/src/backend/tabulation.ml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index a2e1df643..b79f31ce2 100644 --- a/infer/src/backend/tabulation.ml +++ b/infer/src/backend/tabulation.ml @@ -1201,6 +1201,8 @@ let exe_call_postprocess ret_ids trace_call callee_pname callee_attrs loc result raise (Exceptions.Parameter_not_null_checked (desc, __POS__)) else if Localise.is_field_not_null_checked_desc desc then raise (Exceptions.Field_not_null_checked (desc, __POS__)) + else if (Localise.is_empty_vector_access_desc desc) then + raise (Exceptions.Empty_vector_access (desc, __POS__)) else raise (Exceptions.Null_dereference (desc, __POS__)) | Dereference_error (Deref_freed _, desc, path_opt) -> trace_call Specs.CallStats.CR_not_met;