[infer][biabduction] make sure the abort() is treated like exit()

Reviewed By: mbouaziz

Differential Revision: D14110584

fbshipit-source-id: d052f84e6

infer/src/biabduction/BuiltinDefn.ml

@@ -433,12 +433,6 @@ let execute___set_wont_leak_attribute builtin_args : Builtin.ret_typ =
   execute___set_attr PredSymb.Awont_leak builtin_args
 
 
-let execute_abort {Builtin.proc_name} : Builtin.ret_typ =
-  raise
-    (Exceptions.Precondition_not_found
-       (Localise.verbatim_desc (Typ.Procname.to_string proc_name), __POS__))
-
-
 let execute_exit {Builtin.prop_; path} : Builtin.ret_typ = SymExec.diverge prop_ path
 
 let execute_free_ tenv mk ?(mark_as_freed = true) loc acc iter =
@@ -948,7 +942,7 @@ let __unwrap_exception = Builtin.register BuiltinDecl.__unwrap_exception execute
 
 let __variable_initialization = Builtin.register BuiltinDecl.__variable_initialization execute_skip
 
-let abort = Builtin.register BuiltinDecl.abort execute_abort
+let abort = Builtin.register BuiltinDecl.abort execute_exit
 
 let exit = Builtin.register BuiltinDecl.exit execute_exit
 

infer/tests/codetoanalyze/c/errors/issues.exp

@@ -54,6 +54,7 @@ codetoanalyze/c/errors/null_dereference/angelism.c, struct_value_by_ref_callee_w
 codetoanalyze/c/errors/null_dereference/angelism.c, struct_value_by_ref_ptr_write, 4, NULL_DEREFERENCE, B1
 codetoanalyze/c/errors/null_dereference/angelism.c, struct_value_from_pointer_skip_bad, 3, NULL_DEREFERENCE, B1
 codetoanalyze/c/errors/null_dereference/angelism.c, struct_value_skip_null_deref, 4, NULL_DEREFERENCE, B1
+codetoanalyze/c/errors/null_dereference/exit_example.c, exit_example_bad, 5, NULL_DEREFERENCE, B1
 codetoanalyze/c/errors/null_dereference/getc.c, crash_clearerr, 4, NULL_DEREFERENCE, B1
 codetoanalyze/c/errors/null_dereference/getc.c, crash_feof, 4, NULL_DEREFERENCE, B1
 codetoanalyze/c/errors/null_dereference/getc.c, crash_ferror, 4, NULL_DEREFERENCE, B1

infer/tests/codetoanalyze/c/errors/null_dereference/exit_example.c

@@ -0,0 +1,43 @@
+/*
+ * Copyright (c) 2019-present, Facebook, Inc.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+#include <stdlib.h>
+
+void exit_example_bad() {
+  int* p = NULL;
+  if (p) {
+    exit(1);
+  }
+  *p = 42;
+}
+
+void direct_exit_example_ok() {
+  int* p = NULL;
+  exit(1);
+  *p = 42;
+}
+
+void exit_wrapper() { exit(1); }
+
+void indirect_exit_example_ok() {
+  int* p = NULL;
+  exit_wrapper();
+  *p = 42;
+}
+
+void direct_abort_example_ok() {
+  int* p = NULL;
+  abort();
+  *p = 42;
+}
+
+void abort_wrapper() { abort(); }
+
+void indirect_abort_example_ok() {
+  int* p = NULL;
+  abort_wrapper();
+  *p = 42;
+}