diff options
Diffstat (limited to 'file/system.h')
| -rw-r--r-- | file/system.h | 27 |
1 files changed, 27 insertions, 0 deletions
diff --git a/file/system.h b/file/system.h index c06a21331..e3880e077 100644 --- a/file/system.h +++ b/file/system.h @@ -41,6 +41,15 @@ extern int errno; /*@=declundef @*/ #endif +#if HAVE_ERROR && HAVE_ERROR_H +#include <error.h> +#else +/*@exits@*/ +extern void error(int status, int errnum, const char *f, ...) + /*@globals fileSystem @*/ + /*@modifies fileSystem @*/; +#endif + #ifdef STDC_HEADERS #include <stdlib.h> #ifdef HAVE_STDINT_H @@ -103,6 +112,10 @@ extern int _tolower(int) __THROW /*@*/; #include <sys/file.h> #endif +#if HAVE_SYS_WAIT_H +#include <sys/wait.h> +#endif + #if HAVE_SYS_MMAN_H && !defined(__LCLINT__) #include <sys/mman.h> #endif @@ -223,6 +236,20 @@ char * xstrdup (const char *str) /*@=fcnuse@*/ /*@=declundef =exportfcn=incondefs @*/ +/** + */ +/*@unused@*/ /*@exits@*/ /*@only@*/ +static inline void * vmefail(/*@unused@*/ size_t nb) + /*@globals fileSystem @*/ + /*@modifies fileSystem @*/ +{ + error(EXIT_FAILURE, 0, "out of memory"); + /*@notreached@*/ +/*@-nullret@*/ + return NULL; +/*@=nullret@*/ +} + #if HAVE_MCHECK_H #include <mcheck.h> #if defined(__LCLINT__) |