diff --git a/infer/src/bufferoverrun/bufferOverrunModels.ml b/infer/src/bufferoverrun/bufferOverrunModels.ml index f06c5c5ff..aed729535 100644 --- a/infer/src/bufferoverrun/bufferOverrunModels.ml +++ b/infer/src/bufferoverrun/bufferOverrunModels.ml @@ -1259,6 +1259,7 @@ module Call = struct let char_array = Typ.mk (Typ.Tptr (Typ.mk_array char_typ, Pk_pointer)) in make_dispatcher [ -"__exit" <>--> bottom + ; -"__infer_objc_cpp_throw" <>--> bottom ; -"CFArrayCreate" <>$ any_arg $+ capt_exp $+ capt_exp $+...$--> CFArray.create_array ; -"CFArrayCreateCopy" <>$ any_arg $+ capt_exp $!--> create_copy_array ; -"MCFArrayGetCount" <>$ capt_exp $!--> CFArray.length diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp b/infer/tests/codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp index 9bc49580e..9e70aac7f 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp @@ -5,6 +5,7 @@ * LICENSE file in the root directory of this source tree. */ #include +#include void conditional_buffer_access(int* ptr, unsigned int size) { int i; @@ -226,3 +227,15 @@ void call_set_fourth_idx_safe_Good() { MyString* s = new MyString(); set_fourth_idx_safe(s); } + +void throw_exception(int i) { + int a[10]; + if (i >= 10) { + throw std::runtime_error("throw exception"); + } + a[i] = 0; +} + +void call_throw_exception_Good() { throw_exception(15); } + +void call_throw_exception_Bad() { throw_exception(-5); } diff --git a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp index b6b263df3..cca8ec795 100644 --- a/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp +++ b/infer/tests/codetoanalyze/cpp/bufferoverrun/issues.exp @@ -42,6 +42,8 @@ codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_condition codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_inequality_join2_2_Bad, 1, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `idx`,,Array declaration,Array access: Offset: 6 Size: 5 by call to `conditional_inequality_join2` ] codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_minus2_2_Bad, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,,Parameter `size`,Binary operation: (0 - 1):unsigned32 by call to `conditional_minus2` ] codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_conditional_minus_2_Bad, 2, INTEGER_OVERFLOW_L1, no_bucket, ERROR, [Call,,Parameter `size`,Binary operation: (0 - 1):unsigned32 by call to `conditional_minus` ] +codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, call_throw_exception_Bad, 0, BUFFER_OVERRUN_L1, no_bucket, ERROR, [Call,,Parameter `i`,,Array declaration,Array access: Offset: -5 Size: 10 by call to `throw_exception` ] +codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp, throw_exception, 3, UNREACHABLE_CODE, no_bucket, ERROR, [Here] codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 5, BUFFER_OVERRUN_U5, no_bucket, ERROR, [,Unknown value from: lib,Assignment,Array access: Offset: [-oo, +oo] Size: [0, +oo]] codetoanalyze/cpp/bufferoverrun/external.cpp, extern_bad, 10, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Array access: Offset: 30 Size: 10] codetoanalyze/cpp/bufferoverrun/folly_split.cpp, folly_split::FP_do_not_ignore_empty2_Good, 3, BUFFER_OVERRUN_L1, no_bucket, ERROR, [,Array declaration,Assignment,Array access: Offset: 0 Size: 0]