diff options
Diffstat (limited to 'script')
| -rwxr-xr-x | script/coverity.sh | 2 | ||||
| -rw-r--r-- | script/user_nodefs.h | 8 |
2 files changed, 10 insertions, 0 deletions
diff --git a/script/coverity.sh b/script/coverity.sh index dcfeffc1d..785044c8a 100755 --- a/script/coverity.sh +++ b/script/coverity.sh @@ -33,6 +33,8 @@ if [ ! -d "$TOOL_BASE" ]; then ln -s "$TOOL_DIR" "$TOOL_BASE"/cov-analysis fi +cp script/user_nodefs.h "$TOOL_BASE"/cov-analysis/config/user_nodefs.h + COV_BUILD="$TOOL_BASE/cov-analysis/bin/cov-build" # Configure and build diff --git a/script/user_nodefs.h b/script/user_nodefs.h new file mode 100644 index 000000000..110f76851 --- /dev/null +++ b/script/user_nodefs.h @@ -0,0 +1,8 @@ +/* + * Copyright (C) the libgit2 contributors. All rights reserved. + * + * This file is part of libgit2, distributed under the GNU GPL v2 with + * a Linking Exception. For full terms see the included COPYING file. + */ + +#nodef GITERR_CHECK_ALLOC(ptr) if (ptr == NULL) { __coverity_panic__(); } |