diff --git a/infer/src/biabduction/BuiltinDefn.ml b/infer/src/biabduction/BuiltinDefn.ml index 84d505840..4e3369e85 100644 --- a/infer/src/biabduction/BuiltinDefn.ml +++ b/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 diff --git a/infer/tests/codetoanalyze/c/errors/issues.exp b/infer/tests/codetoanalyze/c/errors/issues.exp index 23be504d8..009e0a563 100644 --- a/infer/tests/codetoanalyze/c/errors/issues.exp +++ b/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 diff --git a/infer/tests/codetoanalyze/c/errors/null_dereference/exit_example.c b/infer/tests/codetoanalyze/c/errors/null_dereference/exit_example.c new file mode 100644 index 000000000..da9228873 --- /dev/null +++ b/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 + +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; +}