[inferbo] vector::get() returns an allocated value

Summary: This seems to move in the right direction. Also, `const operator[]` did not do an `access_at`, which I fixed.

Reviewed By: mbouaziz

Differential Revision: D5320427

fbshipit-source-id: c31c5ea
master
Jules Villard 8 years ago committed by Facebook Github Bot
parent 3ddbb8342e
commit 6388910b96

@ -90,13 +90,13 @@ class vector {
void* _ignore2; void* _ignore2;
void access_at(size_type index) const { void access_at(size_type index) const {
_Tp* dummy_array = (_Tp*) malloc(sizeof(value_type) * infer_size); int* dummy_array = (int*)malloc(sizeof(int) * infer_size);
__infer_deref_first_arg(&dummy_array[index]); int x = dummy_array[index];
free(dummy_array);
} }
value_type* get() const { value_type* get() const {
return __infer_skip__get_nondet_val<value_type>(); value_type* p = (value_type*)malloc(sizeof(value_type));
return p;
} }
void allocate(size_type __n) { void allocate(size_type __n) {
@ -437,6 +437,7 @@ operator[](size_type __n) {
template <class _Tp, class _Allocator> template <class _Tp, class _Allocator>
inline typename vector<_Tp, _Allocator>::const_reference inline typename vector<_Tp, _Allocator>::const_reference
vector<_Tp, _Allocator>::operator[](size_type __n) const { vector<_Tp, _Allocator>::operator[](size_type __n) const {
access_at(__n);
return (const_reference)*get(); return (const_reference)*get();
} }

@ -6,31 +6,21 @@ codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 7, BUFFER_OVERRUN, [Of
codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 8, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 8, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 10, BUFFER_OVERRUN, [Offset: [30, 30] Size: [10, 10]] codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 10, BUFFER_OVERRUN, [Offset: [30, 30] Size: [10, 10]]
codetoanalyze/cpp/bufferoverrun/function_call.cpp, call_by_ref_bad, 4, BUFFER_OVERRUN, [Offset: [-1, -1] Size: [10, 10]] codetoanalyze/cpp/bufferoverrun/function_call.cpp, call_by_ref_bad, 4, BUFFER_OVERRUN, [Offset: [-1, -1] Size: [10, 10]]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_lI, 2, BUFFER_OVERRUN, [Offset: [0, +oo] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:5 by call `std::vector<LMB<TFM>*,std::allocator<LMB<TFM>*>>_operator[]()` ] codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_lI, 2, BUFFER_OVERRUN, [Offset: [0, +oo] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:13 by call `std::vector<LMB<TFM>*,std::allocator<LMB<TFM>*>>_operator[]()` ]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_lI, 2, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good_FP, 5, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:13 by call `ral()` ]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, LM<TFM>_uI, 0, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, am_Good_FP, 5, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:5 by call `ral()` ]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, it_it, 0, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [16, 16]] codetoanalyze/cpp/bufferoverrun/repro1.cpp, it_it, 0, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [16, 16]]
codetoanalyze/cpp/bufferoverrun/repro1.cpp, it_it, 0, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [16, 16]] codetoanalyze/cpp/bufferoverrun/repro1.cpp, it_it, 0, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [16, 16]]
codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, instantiate_my_vector_oob_Ok, 3, BUFFER_OVERRUN, [Offset: [0, +oo] Size: [0, +oo] @ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp:21:23 by call `my_vector_oob_Bad()` ] codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, instantiate_my_vector_oob_Ok, 3, BUFFER_OVERRUN, [Offset: [0, +oo] Size: [0, +oo] @ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp:21:23 by call `my_vector_oob_Bad()` ]
codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, my_vector_oob_Bad, 2, BUFFER_OVERRUN, [Offset: [max(0, s$4), s$5] Size: [max(0, s$4), s$5] @ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp:21:23 by call `int_vector_access_at()` ] codetoanalyze/cpp/bufferoverrun/simple_vector.cpp, my_vector_oob_Bad, 2, BUFFER_OVERRUN, [Offset: [max(0, s$4), s$5] Size: [max(0, s$4), s$5] @ codetoanalyze/cpp/bufferoverrun/simple_vector.cpp:21:23 by call `int_vector_access_at()` ]
codetoanalyze/cpp/bufferoverrun/trivial.cpp, trivial, 2, BUFFER_OVERRUN, [Offset: [10, 10] Size: [10, 10]] codetoanalyze/cpp/bufferoverrun/trivial.cpp, trivial, 2, BUFFER_OVERRUN, [Offset: [10, 10] Size: [10, 10]]
codetoanalyze/cpp/bufferoverrun/vector.cpp, constructor_Good_FP, 2, BUFFER_OVERRUN, [Offset: [0, 0] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:5 by call `std::vector<int,std::allocator<int>>_operator[]()` ] codetoanalyze/cpp/bufferoverrun/vector.cpp, constructor_Good_FP, 2, BUFFER_OVERRUN, [Offset: [0, 0] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:13 by call `std::vector<int,std::allocator<int>>_operator[]()` ]
codetoanalyze/cpp/bufferoverrun/vector.cpp, constructor_Good_FP, 2, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 11, BUFFER_OVERRUN, [Offset: [0, 0] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:13 by call `std::vector<Int_no_copy,std::allocator<Int_no_copy>>_operator[]()` ]
codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 11, BUFFER_OVERRUN, [Offset: [0, 0] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:5 by call `std::vector<Int_no_copy,std::allocator<Int_no_copy>>_operator[]()` ]
codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 11, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 16, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:352:17 by call `std::vector<int,std::allocator<int>>_vector()` ] codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 16, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:352:17 by call `std::vector<int,std::allocator<int>>_vector()` ]
codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 16, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:352:31 by call `std::vector<int,std::allocator<int>>_vector()` ] codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 16, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:352:31 by call `std::vector<int,std::allocator<int>>_vector()` ]
codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 17, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 17, BUFFER_OVERRUN, [Offset: [0, 0] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:13 by call `std::vector<int,std::allocator<int>>_operator[]()` ]
codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 18, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 18, BUFFER_OVERRUN, [Offset: [1, 1] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:13 by call `std::vector<int,std::allocator<int>>_at()` ]
codetoanalyze/cpp/bufferoverrun/vector.cpp, just_test_model_FP, 18, BUFFER_OVERRUN, [Offset: [1, 1] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:5 by call `std::vector<int,std::allocator<int>>_at()` ] codetoanalyze/cpp/bufferoverrun/vector.cpp, out_of_bound_Bad, 2, BUFFER_OVERRUN, [Offset: [max(0, s$12), s$13] Size: [max(0, s$12), s$13] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:13 by call `std::vector<int,std::allocator<int>>_operator[]()` ]
codetoanalyze/cpp/bufferoverrun/vector.cpp, out_of_bound_Bad, 2, BUFFER_OVERRUN, [Offset: [max(0, s$12), s$13] Size: [max(0, s$12), s$13] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:5 by call `std::vector<int,std::allocator<int>>_operator[]()` ] codetoanalyze/cpp/bufferoverrun/vector.cpp, push_back_Bad, 3, BUFFER_OVERRUN, [Offset: [1, 1] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:13 by call `std::vector<int,std::allocator<int>>_operator[]()` ]
codetoanalyze/cpp/bufferoverrun/vector.cpp, out_of_bound_Bad, 2, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/vector.cpp, push_back_Good_FP, 3, BUFFER_OVERRUN, [Offset: [0, 0] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:13 by call `std::vector<int,std::allocator<int>>_operator[]()` ]
codetoanalyze/cpp/bufferoverrun/vector.cpp, push_back_Bad, 3, BUFFER_OVERRUN, [Offset: [1, 1] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:5 by call `std::vector<int,std::allocator<int>>_operator[]()` ] codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, BUFFER_OVERRUN, [Offset: [0, 0] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:13 by call `std::vector<int,std::allocator<int>>_operator[]()` ]
codetoanalyze/cpp/bufferoverrun/vector.cpp, push_back_Bad, 3, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Good_FP, 4, BUFFER_OVERRUN, [Offset: [0, 0] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:13 by call `std::vector<int,std::allocator<int>>_operator[]()` ]
codetoanalyze/cpp/bufferoverrun/vector.cpp, push_back_Good_FP, 3, BUFFER_OVERRUN, [Offset: [0, 0] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:5 by call `std::vector<int,std::allocator<int>>_operator[]()` ]
codetoanalyze/cpp/bufferoverrun/vector.cpp, push_back_Good_FP, 3, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, BUFFER_OVERRUN, [Offset: [0, 0] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:5 by call `std::vector<int,std::allocator<int>>_operator[]()` ]
codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Bad, 3, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo]]
codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Good_FP, 4, BUFFER_OVERRUN, [Offset: [0, 0] Size: [0, +oo] @ INFER_MODEL/cpp/include/infer_model/vector_bufferoverrun.h:94:5 by call `std::vector<int,std::allocator<int>>_operator[]()` ]
codetoanalyze/cpp/bufferoverrun/vector.cpp, reserve_Good_FP, 4, BUFFER_OVERRUN, [Offset: [-oo, +oo] Size: [0, +oo]]

Loading…
Cancel
Save