+/*@constant int _POSIX_VERSION@*/
+/*@constant int _POSIX2_VERSION@*/
+/*@constant int _POSIX2_C_VERSION@*/
+/*@constant int _XOPEN_VERSION@*/
+/*@constant int _XOPEN_XCU_VERSION@*/
+
+/* for access: */
+
+/*@constant int R_OK@*/
+/*@constant int W_OK@*/
+/*@constant int X_OK@*/
+/*@constant int F_OK@*/
+
+/* for confstr: */
+/*@constant int _CS_PATH@*/
+/*@constant int _CS_XBS5_ILP32_OFF32_CFLAGS@*/
+/*@constant int _CS_XBS5_ILP32_OFF32_LDFLAGS@*/
+/*@constant int _CS_XBS5_ILP32_OFF32_LIBS@*/
+/*@constant int _CS_XBS5_ILP32_OFF32_LINTFLAGS@*/
+/*@constant int _CS_XBS5_ILP32_OFFBIG_CFLAGS@*/
+/*@constant int _CS_XBS5_ILP32_OFFBIG_LDFLAGS@*/
+/*@constant int _CS_XBS5_ILP32_OFFBIG_LIBS@*/
+/*@constant int _CS_XBS5_ILP32_OFFBIG_LINTFLAGS@*/
+/*@constant int _CS_XBS5_LP64_OFF64_CFLAGS@*/
+/*@constant int _CS_XBS5_LP64_OFF64_LDFLAGS@*/
+/*@constant int _CS_XBS5_LP64_OFF64_LIBS@*/
+/*@constant int _CS_XBS5_LP64_OFF64_LINTFLAGS@*/
+/*@constant int _CS_XBS5_LPBIG_OFFBIG_CFLAGS@*/
+/*@constant int _CS_XBS5_LPBIG_OFFBIG_LDFLAGS@*/
+/*@constant int _CS_XBS5_LPBIG_OFFBIG_LIBS@*/
+/*@constant int _CS_XBS5_LPBIG_OFFBIG_LINTFLAGS@*/
+
+/* name parameters to sysconf: */
+
+/*@constant int _SC_2_C_BIND@*/
+/*@constant int _SC_2_C_DEV@*/
+/*@constant int _SC_2_C_VERSION@*/
+/*@constant int _SC_2_FORT_DEV@*/
+/*@constant int _SC_2_FORT_RUN@*/
+/*@constant int _SC_2_LOCALEDEF@*/
+/*@constant int _SC_2_SW_DEV@*/
+/*@constant int _SC_2_UPE@*/
+/*@constant int _SC_2_VERSION@*/
+/*@constant int _SC_ARG_MAX@*/
+/*@constant int _SC_AIO_LISTIO_MAX@*/
+/*@constant int _SC_AIO_MAX@*/
+/*@constant int _SC_AIO_PRIO_DELTA_MAX@*/
+/*@constant int _SC_ASYNCHRONOUS_IO@*/
+/*@constant int _SC_ATEXIT_MAX@*/
+/*@constant int _SC_BC_BASE_MAX@*/
+/*@constant int _SC_BC_DIM_MAX@*/
+/*@constant int _SC_BC_SCALE_MAX@*/
+/*@constant int _SC_BC_STRING_MAX@*/
+/*@constant int _SC_CHILD_MAX@*/
+/*@constant int _SC_CLK_TCK@*/
+/*@constant int _SC_COLL_WEIGHTS_MAX@*/
+/*@constant int _SC_DELAYTIMER_MAX@*/
+/*@constant int _SC_EXPR_NEST_MAX@*/
+/*@constant int _SC_FSYNC@*/
+/*@constant int _SC_GETGR_R_SIZE_MAX@*/
+/*@constant int _SC_GETPW_R_SIZE_MAX@*/
+/*@constant int _SC_IOV_MAX@*/
+/*@constant int _SC_JOB_CONTROL@*/
+/*@constant int _SC_LINE_MAX@*/
+/*@constant int _SC_LOGIN_NAME_MAX@*/
+/*@constant int _SC_MAPPED_FILES@*/
+/*@constant int _SC_MEMLOCK@*/
+/*@constant int _SC_MEMLOCK_RANGE@*/
+/*@constant int _SC_MEMORY_PROTECTION@*/
+/*@constant int _SC_MESSAGE_PASSING@*/
+/*@constant int _SC_MQ_OPEN_MAX@*/
+/*@constant int _SC_MQ_PRIO_MAX@*/
+/*@constant int _SC_NGROUPS_MAX@*/
+/*@constant int _SC_OPEN_MAX@*/
+/*@constant int _SC_PAGESIZE@*/
+/*@constant int _SC_PAGE_SIZE@*/
+/*@constant int _SC_PASS_MAX@*/
+/*@constant int _SC_PRIORITIZED_IO@*/
+/*@constant int _SC_PRIORITY_SCHEDULING@*/
+/*@constant int _SC_RE_DUP_MAX@*/
+/*@constant int _SC_REALTIME_SIGNALS@*/
+/*@constant int _SC_RTSIG_MAX@*/
+/*@constant int _SC_SAVED_IDS@*/
+/*@constant int _SC_SEMAPHORES@*/
+/*@constant int _SC_SEM_NSEMS_MAX@*/
+/*@constant int _SC_SEM_VALUE_MAX@*/
+/*@constant int _SC_SHARED_MEMORY_OBJECTS@*/
+/*@constant int _SC_SIGQUEUE_MAX@*/
+/*@constant int _SC_STREAM_MAX@*/
+/*@constant int _SC_SYNCHRONIZED_IO@*/
+/*@constant int _SC_THREADS@*/
+/*@constant int _SC_THREAD_ATTR_STACKADDR@*/
+/*@constant int _SC_THREAD_ATTR_STACKSIZE@*/
+/*@constant int _SC_THREAD_DESTRUCTOR_ITERATIONS@*/
+/*@constant int _SC_THREAD_KEYS_MAX@*/
+/*@constant int _SC_THREAD_PRIORITY_SCHEDULING@*/
+/*@constant int _SC_THREAD_PRIO_INHERIT@*/
+/*@constant int _SC_THREAD_PRIO_PROTECT@*/
+/*@constant int _SC_THREAD_PROCESS_SHARED@*/
+/*@constant int _SC_THREAD_SAFE_FUNCTIONS@*/
+/*@constant int _SC_THREAD_STACK_MIN@*/
+/*@constant int _SC_THREAD_THREADS_MAX@*/
+/*@constant int _SC_TIMERS@*/
+/*@constant int _SC_TIMER_MAX@*/
+/*@constant int _SC_TTY_NAME_MAX@*/
+/*@constant int _SC_TZNAME_MAX@*/
+/*@constant int _SC_VERSION@*/
+/*@constant int _SC_XOPEN_VERSION@*/
+/*@constant int _SC_XOPEN_CRYPT@*/
+/*@constant int _SC_XOPEN_ENH_I18N@*/
+/*@constant int _SC_XOPEN_SHM@*/
+/*@constant int _SC_XOPEN_UNIX@*/
+/*@constant int _SC_XOPEN_XCU_VERSION@*/
+/*@constant int _SC_XOPEN_LEGACY@*/
+/*@constant int _SC_XOPEN_REALTIME@*/
+/*@constant int _SC_XOPEN_REALTIME_THREADS@*/
+/*@constant int _SC_XBS5_ILP32_OFF32@*/
+/*@constant int _SC_XBS5_ILP32_OFFBIG@*/
+/*@constant int _SC_XBS5_LP64_OFF64@*/
+/*@constant int _SC_XBS5_LPBIG_OFFBIG@*/
+
+
+int access(const char *, int) /*@modifies errno@*/ /*:errorcode -1:*/ ;
+unsigned int alarm (unsigned int) /*@modifies internalState@*/ ;
+
+int brk(void *)
+ /*@modifies errno@*/
+ /*:errorcode -1:*/
+ /*@warn legacy "brk is obsolete"@*/ ;
+
+int chdir (const char *)
+ /*@modifies internalState, errno@*/
+ /*:errorcode -1:*/ ;
+
+int chown (const char *, uid_t, gid_t)
+ /*@modifies internalState, errno@*/
+ /*:errorcode -1:*/ ;
+
+int close (int)
+ /*@modifies internalState, errno@*/
+ /*:errorcode -1:*/ ;
+
+size_t confstr(int, /*@null@*/ char *, size_t)
+ /*@globals internalState@*/
+ /*@modifies errno@*/
+ /*:errorcode 0:*/ ;
+
+/*@dependent@*/ /*@null@*/ char *crypt(const char *, const char *)
+ /*@modifies errno, internalState@*/ ;
+
+/*@dependent@*/ /*@null@*/ char *ctermid(/*@returned@*/ /*@null@*/ /*@out@*/ char *s)
+ /*@modifies s@*/ ;
+
+/*@null@*/ /*@dependent@*/ char *cuserid (/*@null@*/ /*@returned@*/ char *s)
+ /*@warn legacy "cuserid is obsolete"@*/
+ /*@modifies s@*/ ;
+
+int dup(int)
+ /*@modifies errno, internalState@*/
+ /*:errorcode -1:*/ ;
+
+int dup2(int, int)
+ /*@modifies errno, internalState@*/
+ /*:errorcode -1:*/ ;
+
+void encrypt(char p_block[], int)
+ /*@requires maxSet(p_block) == 63@*/
+ /*@modifies p_block, errno@*/ ;
+
+extern char **environ;
+
+int execl (const char *, const char *, ...)
+ /*@modifies errno, internalState@*/
+ /*:errorcode -1:*/ ;
+
+int execle(const char *, const char *, ...)
+ /*@modifies errno, internalState@*/
+ /*:errorcode -1:*/ ;
+
+int execlp(const char *, const char *, ...)
+ /*@modifies errno, internalState@*/
+ /*:errorcode -1:*/ ;
+
+int execv(const char *, char *const [])
+ /*@modifies errno, internalState@*/
+ /*:errorcode -1:*/ ;
+
+int execve(const char *, char *const [], char *const [])
+ /*@modifies errno, internalState@*/
+ /*:errorcode -1:*/ ;
+
+int execvp(const char *, char *const [])
+ /*@modifies errno, internalState@*/
+ /*:errorcode -1:*/ ;
+
+/*@exits@*/ void _exit (int);
+
+int fchown (int, uid_t, gid_t)
+ /*@modifies errno, fileSystem@*/
+ /*:errorcode -1:*/ ;
+
+int fchdir (int)
+ /*@modifies errno, fileSystem@*/
+ /*:errorcode -1:*/ ;