diff options
author | jbj <devnull@localhost> | 2001-10-15 17:53:34 +0000 |
---|---|---|
committer | jbj <devnull@localhost> | 2001-10-15 17:53:34 +0000 |
commit | 72471f2e54686202a9862a3fd3bd6d0135d81d2a (patch) | |
tree | 3625a73d9ef73f4f29df80fe98fb6133041cb4bc /system.h | |
parent | 3f462f318fd2f602fddb1a95e5d652e67aafa49e (diff) | |
download | rpm-72471f2e54686202a9862a3fd3bd6d0135d81d2a.tar.gz rpm-72471f2e54686202a9862a3fd3bd6d0135d81d2a.tar.bz2 rpm-72471f2e54686202a9862a3fd3bd6d0135d81d2a.zip |
Explicit branchstate annotations.
CVS patchset: 5113
CVS date: 2001/10/15 17:53:34
Diffstat (limited to 'system.h')
-rw-r--r-- | system.h | 8 |
1 files changed, 6 insertions, 2 deletions
@@ -24,6 +24,7 @@ #if defined(__LCLINT__) /*@-superuser -declundef -incondefs @*/ /* LCL: modifies clause missing */ extern int chroot (const char *__path) + /*@globals errno, systemState @*/ /*@modifies errno, systemState @*/; /*@=superuser =declundef =incondefs @*/ #endif @@ -113,6 +114,7 @@ extern int errno; #if defined(__LCLINT__) /*@-declundef -incondefs @*/ /* LCL: modifies clause missing */ extern char * realpath (const char * file_name, /*@out@*/ char * resolved_name) + /*@globals errno, fileSystem @*/ /*@requires maxSet(resolved_name) >= (PATH_MAX - 1); @*/ /*@modifies *resolved_name, errno, fileSystem @*/; /*@=declundef =incondefs @*/ @@ -166,8 +168,8 @@ char *realpath(const char *path, char resolved_path []); #if defined(__LCLINT__) /*@-declundef -incondefs @*/ /* LCL: missing annotation */ -/*@only@*/ void * alloca (size_t size) - /*@ensures MaxSet(result) == (size - 1) @*/ +/*@only@*/ void * alloca (size_t __size) + /*@ensures MaxSet(result) == (__size - 1) @*/ /*@*/; /*@=declundef =incondefs @*/ #endif @@ -231,6 +233,7 @@ char *alloca (); /** */ /*@mayexit@*/ /*@only@*/ /*@out@*/ void * xmalloc (size_t size) + /*@globals errno @*/ /*@ensures MaxSet(result) == (size - 1) @*/ /*@modifies errno @*/; @@ -435,6 +438,7 @@ typedef /*@concrete@*/ struct extern int glob (const char *pattern, int flags, int (*errfunc) (const char *, int), /*@out@*/ glob_t *pglob) + /*@globals errno, fileSystem @*/ /*@modifies *pglob, errno, fileSystem @*/; /* XXX only annotation is a white lie */ extern void globfree (/*@only@*/ glob_t *pglob) |