[inferbo] Add model for C++ exception throw

Reviewed By: ezgicicek

Differential Revision: D19767841

fbshipit-source-id: b76e5a8f3

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

infer/tests/codetoanalyze/cpp/bufferoverrun/conditional_proof_obligation.cpp

@@ -5,6 +5,7 @@
  * LICENSE file in the root directory of this source tree.
  */
 #include <stddef.h>
+#include <stdexcept>
 
 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); }

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,<Offset trace>,Parameter `idx`,<Length trace>,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,<LHS trace>,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,<LHS trace>,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,<Offset trace>,Parameter `i`,<Length trace>,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, [<Length trace>,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, [<Length trace>,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, [<Length trace>,Array declaration,Assignment,Array access: Offset: 0 Size: 0]