[pulse] introduce the more precise `VECTOR_INVALIDATION` issue type

Summary:
Get rid of `USE_AFTER_LIFETIME`. This could be useful to deploy pulse
alongside the ownership checker too.

Reviewed By: da319

Differential Revision: D12857477

fbshipit-source-id: 8e2a2a37c

infer/src/base/IssueType.ml

@@ -415,6 +415,8 @@ let untrusted_url_risk = from_string "UNTRUSTED_URL_RISK"
 
 let untrusted_variable_length_array = from_string "UNTRUSTED_VARIABLE_LENGTH_ARRAY"
 
+let vector_invalidation = from_string "VECTOR_INVALIDATION"
+
 let wrong_argument_number = from_string "Wrong_argument_number" ~hum:"Wrong Argument Number"
 
 let zero_execution_time_call = from_string ~enabled:false "ZERO_EXECUTION_TIME_CALL"

infer/src/base/IssueType.mli

@@ -317,6 +317,8 @@ val untrusted_variable_length_array : t
 
 val user_controlled_sql_risk : t
 
+val vector_invalidation : t
+
 val wrong_argument_number : t
 
 val zero_execution_time_call : t

infer/src/checkers/PulseInvalidation.ml

@@ -26,7 +26,7 @@ let issue_type_of_cause = function
   | Nullptr ->
       IssueType.null_dereference
   | StdVectorPushBack _ ->
-      IssueType.use_after_lifetime
+      IssueType.vector_invalidation
 
 
 let get_location = function

infer/tests/codetoanalyze/cpp/pulse/issues.exp

@@ -14,6 +14,6 @@ codetoanalyze/cpp/pulse/use_after_destructor.cpp, placement_new_aliasing2_bad, 5
 codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_destructor_bad, 3, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [invalidated by destructor call `S_~S(s)` at line 61, column 3 here,accessed `*(s.f)` here]
 codetoanalyze/cpp/pulse/use_after_destructor.cpp, use_after_scope4_bad, 6, USE_AFTER_DESTRUCTOR, no_bucket, ERROR, [invalidated by destructor call `C_~C(c)` at line 185, column 3 here,accessed `pc->f` here]
 codetoanalyze/cpp/pulse/use_after_free.cpp, use_after_free_simple_bad, 2, USE_AFTER_FREE, no_bucket, ERROR, [invalidated by call to `free(x)` at line 10, column 3 here,accessed `*(x)` here]
-codetoanalyze/cpp/pulse/vector.cpp, FP_reserve_then_push_back_ok, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(vec, ..)` at line 37, column 3 here,accessed `*(elt)` here]
-codetoanalyze/cpp/pulse/vector.cpp, deref_local_vector_element_after_push_back_bad, 4, USE_AFTER_LIFETIME, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(&(vec), ..)` at line 19, column 3 here,accessed `*(elt)` here]
-codetoanalyze/cpp/pulse/vector.cpp, deref_vector_element_after_push_back_bad, 3, USE_AFTER_LIFETIME, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(vec, ..)` at line 12, column 3 here,accessed `*(elt)` here]
+codetoanalyze/cpp/pulse/vector.cpp, FP_reserve_then_push_back_ok, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(vec, ..)` at line 37, column 3 here,accessed `*(elt)` here]
+codetoanalyze/cpp/pulse/vector.cpp, deref_local_vector_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(&(vec), ..)` at line 19, column 3 here,accessed `*(elt)` here]
+codetoanalyze/cpp/pulse/vector.cpp, deref_vector_element_after_push_back_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [potentially invalidated by call to `std::vector::push_back(vec, ..)` at line 12, column 3 here,accessed `*(elt)` here]