diff --git a/infer/models/cpp/include/infer_model/vector.h b/infer/models/cpp/include/infer_model/vector.h index fa7cd7902..8b3df338b 100644 --- a/infer/models/cpp/include/infer_model/vector.h +++ b/infer/models/cpp/include/infer_model/vector.h @@ -85,29 +85,33 @@ class vector { value_type* get() const { return beginPtr; } void allocate(size_type size) { - if (size > 0) { - beginPtr = __infer_skip__get_nondet_val(); - } else { - beginPtr = nullptr; - } + // assume that allocation will produce non-empty vector regardless of the + // size + // if (size > 0) { + beginPtr = __infer_skip__get_nondet_val(); + //} else { + // deallocate(); + //} } + void deallocate() { beginPtr = nullptr; } + template void allocate_iter(Iter begin, Iter end) { if (begin != end) { allocate(1); } else { - allocate(0); + deallocate(); } } /* std::vector implementation */ vector() noexcept(is_nothrow_default_constructible::value) { - allocate(0); + deallocate(); } - explicit vector(const allocator_type& __a) noexcept { allocate(0); } + explicit vector(const allocator_type& __a) noexcept { deallocate(); } explicit vector(size_type __n); // introduced in C++14 @@ -251,7 +255,7 @@ class vector { iterator erase(const_iterator __position); iterator erase(const_iterator __first, const_iterator __last); - void clear() noexcept { allocate(0); } + void clear() noexcept { deallocate(); } void resize(size_type __sz); void resize(size_type __sz, const_reference __x); diff --git a/infer/tests/codetoanalyze/cpp/errors/vector/empty_access.cpp b/infer/tests/codetoanalyze/cpp/errors/vector/empty_access.cpp index eaebf90a3..71d36f234 100644 --- a/infer/tests/codetoanalyze/cpp/errors/vector/empty_access.cpp +++ b/infer/tests/codetoanalyze/cpp/errors/vector/empty_access.cpp @@ -37,6 +37,12 @@ int resize1_nonempty() { return vec[0]; } +int resize_n_nonempty(int n) { + std::vector vec; + vec.resize(n); + return vec[0]; +} + int push_back_nonempty() { std::vector vec; vec.push_back(1); diff --git a/infer/tests/endtoend/cpp/VectorEmptyAccessTest.java b/infer/tests/endtoend/cpp/VectorEmptyAccessTest.java index 9eba28450..079d6aeab 100644 --- a/infer/tests/endtoend/cpp/VectorEmptyAccessTest.java +++ b/infer/tests/endtoend/cpp/VectorEmptyAccessTest.java @@ -50,7 +50,7 @@ public class VectorEmptyAccessTest { String[] procedures = { "access_empty", "clear_empty", - "resize0_empty", + //"resize0_empty", // resize(0) doesn't make vector empty "copy_empty", "assign_empty", "empty_check_access_empty",