diff options
Diffstat (limited to 'popt/system.h')
| -rw-r--r-- | popt/system.h | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/popt/system.h b/popt/system.h index 43ad70f9..338be45b 100644 --- a/popt/system.h +++ b/popt/system.h @@ -25,6 +25,14 @@ #include <libc.h> #endif +#if defined(__LCLINT__) +/*@-declundef -incondefs -redecl@*/ /* LCL: missing annotation */ +/*@only@*/ void * alloca (size_t __size) + /*@ensures MaxSet(result) == (__size - 1) @*/ + /*@*/; +/*@=declundef =incondefs =redecl@*/ +#endif + /* AIX requires this to be the first thing in the file. */ #ifndef __GNUC__ # if HAVE_ALLOCA_H @@ -42,7 +50,10 @@ char *alloca (); #define alloca __builtin_alloca #endif -/*@only@*/ char * xstrdup (const char *str); +/*@-redecl -redef@*/ +/*@mayexit@*/ /*@only@*/ char * xstrdup (const char *str) + /*@*/; +/*@=redecl =redef@*/ #if HAVE_MCHECK_H && defined(__GNUC__) #define vmefail() (fprintf(stderr, "virtual memory exhausted.\n"), exit(EXIT_FAILURE), NULL) |