Model vector::resize(n) as nonempty vector

Summary:
Assume that std::vector::resize will always create nonempty vector. While this is clearly
wrong for resize(0), it removes many FPs for `resize(n)` calls, where value of `n` is unknown.
Without it, infer was thinking that `n` could be 0 and reported empty vector access.

Reviewed By: jvillard

Differential Revision: D3424355

fbshipit-source-id: cb476de

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<value_type>();
-    } else {
-      beginPtr = nullptr;
-    }
+    // assume that allocation will produce non-empty vector regardless of the
+    // size
+    // if (size > 0) {
+    beginPtr = __infer_skip__get_nondet_val<value_type>();
+    //} else {
+    //  deallocate();
+    //}
   }
 
+  void deallocate() { beginPtr = nullptr; }
+
   template <class Iter>
   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<allocator_type>::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);

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<int> vec;
+  vec.resize(n);
+  return vec[0];
+}
+
 int push_back_nonempty() {
   std::vector<int> vec;
   vec.push_back(1);

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",