Explicit branchstate annotations.

CVS patchset: 5113
CVS date: 2001/10/15 17:53:34

1 files changed, 6 insertions, 2 deletions

diff --git a/system.h b/system.h
index 4e02cb9be..74e9a5906 100644
--- a/system.h
+++ b/system.h
@@ -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)