diff --git a/infer/models/c/src/libc_basic.c b/infer/models/c/src/libc_basic.c index 0abcb55c7..dff2c9c91 100644 --- a/infer/models/c/src/libc_basic.c +++ b/infer/models/c/src/libc_basic.c @@ -642,15 +642,27 @@ int fputc(int c, FILE* stream) { char* getcwd(char* buffer, size_t size) { int n; int size_buf; - n = __infer_nondet_int(); - - if (n > 0) { - __require_allocated_array(buffer); - size_buf = __get_array_length(buffer); - INFER_EXCLUDE_CONDITION(size > size_buf); - return buffer; - } else - return NULL; + char* result; + + if (buffer == NULL) { + if (size == 0) { + n = __infer_nondet_int(); + } else { + n = size; + } + return (char*)malloc(n); + } else { + n = __infer_nondet_int(); + + if (n > 0) { + __require_allocated_array(buffer); + size_buf = __get_array_length(buffer); + INFER_EXCLUDE_CONDITION(size > size_buf); + return buffer; + } else { + return NULL; + } + } } // return nonteterministically 0 or -1 diff --git a/infer/tests/codetoanalyze/c/errors/issues.exp b/infer/tests/codetoanalyze/c/errors/issues.exp index 792cf68a9..c9f6f3007 100644 --- a/infer/tests/codetoanalyze/c/errors/issues.exp +++ b/infer/tests/codetoanalyze/c/errors/issues.exp @@ -71,6 +71,9 @@ codetoanalyze/c/errors/null_dereference/getc.c, crash_putc, 4, NULL_DEREFERENCE, codetoanalyze/c/errors/null_dereference/getc.c, crash_rewind, 4, NULL_DEREFERENCE, B1 codetoanalyze/c/errors/null_dereference/getc.c, crash_ungetc, 5, NULL_DEREFERENCE, B1 codetoanalyze/c/errors/null_dereference/getc.c, crash_vfprintf, 5, NULL_DEREFERENCE, B1 +codetoanalyze/c/errors/null_dereference/getcwd.c, getcwd_no_buf_no_check_bad, 2, NULL_DEREFERENCE, B1 +codetoanalyze/c/errors/null_dereference/getcwd.c, getcwd_no_buf_no_free_bad, 3, MEMORY_LEAK, no_bucket +codetoanalyze/c/errors/null_dereference/getcwd.c, getcwd_no_check_bad, 3, NULL_DEREFERENCE, B1 codetoanalyze/c/errors/null_dereference/issue_680.c, null_ptr_deref2_bad, 0, NULL_DEREFERENCE, B1 codetoanalyze/c/errors/null_dereference/issue_680.c, null_ptr_deref_bad, 0, NULL_DEREFERENCE, B1 codetoanalyze/c/errors/null_dereference/issue_680.c, null_ptr_deref_bad_FN, 0, PRECONDITION_NOT_MET, no_bucket diff --git a/infer/tests/codetoanalyze/c/errors/null_dereference/getcwd.c b/infer/tests/codetoanalyze/c/errors/null_dereference/getcwd.c new file mode 100644 index 000000000..b8d6ad9c1 --- /dev/null +++ b/infer/tests/codetoanalyze/c/errors/null_dereference/getcwd.c @@ -0,0 +1,45 @@ +/* + * Copyright (c) 2018-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 + +#define BUFFER_SIZE 16 + +char getcwd_ok() { + char* cwd = getcwd(NULL, 0); + if (cwd != NULL) { + char result = cwd[0]; + free(cwd); + return result; + } + char buf[BUFFER_SIZE]; + cwd = getcwd(&buf, BUFFER_SIZE); + if (cwd != NULL) { + return cwd[0]; + } + return 'a'; +} + +char getcwd_no_buf_no_check_bad() { + char* cwd = getcwd(NULL, 0); + char result = cwd[0]; + free(cwd); + return result; +} + +char getcwd_no_buf_no_free_bad() { + char* cwd = getcwd(NULL, 0); + if (cwd != NULL) { + return cwd[0]; + } + return 'a'; +} + +char getcwd_no_check_bad() { + char buf[BUFFER_SIZE]; + char* cwd = getcwd(&buf, BUFFER_SIZE); + return cwd[0]; +}