From 3bf771bff4ba84c2e3c830ddb8c0f775a1bc910c Mon Sep 17 00:00:00 2001 From: Jules Villard Date: Fri, 17 Jan 2020 03:47:34 -0800 Subject: [PATCH] [pulse] add model for std::vector<>::at() Summary: Kinda forgot to model this when `operator[]` was modelled. Reviewed By: skcho Differential Revision: D19433156 fbshipit-source-id: 49fbafc8a --- infer/src/pulse/PulseModels.ml | 2 ++ infer/tests/codetoanalyze/cpp/pulse/issues.exp | 1 + infer/tests/codetoanalyze/cpp/pulse/vector.cpp | 8 ++++++++ 3 files changed, 11 insertions(+) diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml index 598b3c19f..7b84ac9bd 100644 --- a/infer/src/pulse/PulseModels.ml +++ b/infer/src/pulse/PulseModels.ml @@ -407,6 +407,8 @@ module ProcNameDispatcher = struct <>--> Misc.return_int ; -"std" &:: "vector" &:: "assign" <>$ capt_arg_payload $+...$--> StdVector.invalidate_references Assign + ; -"std" &:: "vector" &:: "at" <>$ capt_arg_payload $+ capt_arg_payload + $--> StdVector.at ~desc:"std::vector::at()" ; -"std" &:: "vector" &:: "clear" <>$ capt_arg_payload $--> StdVector.invalidate_references Clear ; -"std" &:: "vector" &:: "emplace" $ capt_arg_payload diff --git a/infer/tests/codetoanalyze/cpp/pulse/issues.exp b/infer/tests/codetoanalyze/cpp/pulse/issues.exp index ba46b589d..c0feb5e80 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/issues.exp +++ b/infer/tests/codetoanalyze/cpp/pulse/issues.exp @@ -76,6 +76,7 @@ codetoanalyze/cpp/pulse/vector.cpp, assign_bad, 3, VECTOR_INVALIDATION, no_bucke codetoanalyze/cpp/pulse/vector.cpp, clear_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of clear_bad,was potentially invalidated by `std::vector::clear()`,use-after-lifetime part of the trace starts here,parameter `vec` of clear_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here] codetoanalyze/cpp/pulse/vector.cpp, deref_local_vector_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,variable `vec` declared here,was potentially invalidated by `std::vector::push_back()`,use-after-lifetime part of the trace starts here,variable `vec` declared here,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here] codetoanalyze/cpp/pulse/vector.cpp, deref_vector_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of deref_vector_element_after_push_back_bad,was potentially invalidated by `std::vector::push_back()`,use-after-lifetime part of the trace starts here,parameter `vec` of deref_vector_element_after_push_back_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,assigned,invalid access occurs here] +codetoanalyze/cpp/pulse/vector.cpp, deref_vector_pointer_element_after_push_back_bad, 4, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of deref_vector_pointer_element_after_push_back_bad,was potentially invalidated by `std::vector::push_back()`,use-after-lifetime part of the trace starts here,parameter `vec` of deref_vector_pointer_element_after_push_back_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,assigned,invalid access occurs here] codetoanalyze/cpp/pulse/vector.cpp, emplace_back_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of emplace_back_bad,was potentially invalidated by `std::vector::emplace_back()`,use-after-lifetime part of the trace starts here,parameter `vec` of emplace_back_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here] codetoanalyze/cpp/pulse/vector.cpp, emplace_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of emplace_bad,was potentially invalidated by `std::vector::emplace()`,use-after-lifetime part of the trace starts here,parameter `vec` of emplace_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here] codetoanalyze/cpp/pulse/vector.cpp, insert_bad, 3, VECTOR_INVALIDATION, no_bucket, ERROR, [invalidation part of the trace starts here,parameter `vec` of insert_bad,was potentially invalidated by `std::vector::insert()`,use-after-lifetime part of the trace starts here,parameter `vec` of insert_bad,passed as argument to `std::vector::at()` (modelled),return from call to `std::vector::at()` (modelled),assigned,invalid access occurs here] diff --git a/infer/tests/codetoanalyze/cpp/pulse/vector.cpp b/infer/tests/codetoanalyze/cpp/pulse/vector.cpp index b345fca87..9467690c4 100644 --- a/infer/tests/codetoanalyze/cpp/pulse/vector.cpp +++ b/infer/tests/codetoanalyze/cpp/pulse/vector.cpp @@ -14,6 +14,14 @@ void deref_vector_element_after_push_back_bad(std::vector& vec) { std::cout << *y << "\n"; } +// slight variation of above, in particular use vector::at() +void deref_vector_pointer_element_after_push_back_bad(std::vector* vec) { + int* elt = &vec->at(1); + int* y = elt; + vec->push_back(42); + std::cout << *y << "\n"; +} + void deref_local_vector_element_after_push_back_bad() { std::vector vec = {0, 0}; int* elt = &vec[1];