From 3131660ede7112f81043e04a168cbb7caefde1d5 Mon Sep 17 00:00:00 2001
From: Mehdi Bouaziz <mbouaziz@fb.com>
Date: Tue, 2 May 2017 11:43:57 -0700
Subject: [PATCH] [inferbo] Model-like test for vector

Reviewed By: jvillard

Differential Revision: D4953300

fbshipit-source-id: 0ef33db
---
 .../codetoanalyze/cpp/bufferoverrun/Makefile  |  4 +-
 .../cpp/bufferoverrun/simple_vector.cpp       | 43 +++++++++++++++++++
 2 files changed, 44 insertions(+), 3 deletions(-)
 create mode 100644 infer/tests/codetoanalyze/cpp/bufferoverrun/simple_vector.cpp

diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/Makefile b/infer/tests/codetoanalyze/cpp/bufferoverrun/Makefile
index eec20303a..cc6b815ca 100644
--- a/infer/tests/codetoanalyze/cpp/bufferoverrun/Makefile
+++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/Makefile
@@ -13,9 +13,7 @@ CLANG_OPTIONS = -x c++ -std=c++11 -nostdinc++ -isystem$(MODELS_DIR)/cpp/include
 INFER_OPTIONS = --ml-buckets cpp --no-filtering --debug-exceptions --project-root $(TESTS_DIR) --no-failures-allowed
 INFERPRINT_OPTIONS = --issues-tests
 
-SOURCES = \
-	trivial.cpp \
-  vector.cpp \
+SOURCES = $(wildcard *.cpp)
 
 HEADERS =
 
diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/simple_vector.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/simple_vector.cpp
new file mode 100644
index 000000000..7e2430ee5
--- /dev/null
+++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/simple_vector.cpp
@@ -0,0 +1,43 @@
+/*
+ * Copyright (c) 2017 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ */
+#include <cstdlib>
+
+class int_vector {
+  unsigned int _size;
+public:
+  // FAILS TO RELATE output field _size to argument size, NEED STRONG UPDATE
+  int_vector(int size): _size(size) {}
+  // FAILS TO SET output field _size to 0
+  int_vector(): int_vector(0) {}
+
+  void access_at(int i) {
+    int* dummy_array = (int*)malloc(sizeof(int) * _size);
+    int dummy_value = dummy_array[i];
+    free(dummy_array);
+  }
+  unsigned int size() {
+    return _size;
+  }
+
+  void resize(int newsize) {
+    _size = newsize;
+  }
+};
+
+void FN_my_vector_oob_Bad(int_vector& v) {
+  unsigned int n = v.size();
+  v.access_at(n);
+}
+
+// We expect the error to be throw in FN_my_vector_oob_Bad already
+void FN_instantiate_my_vector_oob_Ok() {
+  int_vector v;
+  v.resize(42);
+  FN_my_vector_oob_Bad(v);
+}