From f15b5ca18ccab54cfccaaa143afdea8b629f6dfc Mon Sep 17 00:00:00 2001 From: Mihail Groza Date: Sun, 26 Mar 2017 22:21:14 +0000 Subject: [PATCH] Remove unused headers (for library) from repository --- lib/linux.h | 589 -------------------------- lib/posix.h | 994 -------------------------------------------- lib/standard.h | 1271 -------------------------------------------------------- 3 files changed, 2854 deletions(-) delete mode 100644 lib/linux.h delete mode 100644 lib/posix.h delete mode 100644 lib/standard.h diff --git a/lib/linux.h b/lib/linux.h deleted file mode 100644 index 9b6e9ab..0000000 --- a/lib/linux.h +++ /dev/null @@ -1,589 +0,0 @@ -/* -** linux.h -*/ - -/* -** Based on Linux Standard Base Specification 1.0.0 -** http://www.linuxbase.org/spec/gLSB/gLSB/libc-ddefs.html -*/ - -/* - -Data Definitions for libc - -dirent.h -*/ - -typedef struct __dirstream DIR; - -/* Not in LSB: based on RedHat 7.0: */ - -struct dirent { -#ifndef __USE_FILE_OFFSET64 - __ino_t d_ino; - __off_t d_off; -#else - __ino64_t d_ino; - __off64_t d_off; -#endif - unsigned short int d_reclen; - unsigned char d_type; - char d_name[256]; /* We must not include limits.h! */ -} ; - -/*@i43 struct dirent not in LSB spec - why doesn't alphasort64 use struct dirent64's? -*/ - -int acct (/*@null@*/ const char *filename) - /*:statusreturn@*/ - /*@modifies systemState@*/ ; - -int alphasort (const struct dirent **a, const struct dirent **b) /*@*/ ; -int alphasort64(const struct dirent **a, const struct dirent **b) /*@*/ ; - -/* -ftw.h -*/ - -typedef int (*__ftw_func_t) (char *__filename, struct stat * __status, - int __flag); - -typedef int (*__ftw64_func_t) (char *__filename, struct stat64 * __status, - int __flag); - -typedef int (*__nftw_func_t) (char *__filename, struct stat * __status, - int __flag, struct FTW * __info); - -typedef int (*__nftw64_func_t) (char *__filename, struct stat64 * __status, - int __flag, struct FTW * __info); - -/* -glob.h -*/ - -typedef struct -{ - __size_t gl_pathc; - char **gl_pathv; - __size_t gl_offs; - int gl_flags; - void (*gl_closedir) (); - struct dirent64 *(*gl_readdir) (); - void *(*gl_opendir) (); - int (*gl_lstat) (); - int (*gl_stat) (); -} -glob_t; - -typedef struct -{ - __size_t gl_pathc; - char **gl_pathv; - __size_t gl_offs; - int gl_flags; - void (*gl_closedir) (); - struct dirent64 *(*gl_readdir) (); - void *(*gl_opendir) (); - int (*gl_lstat) (); - int (*gl_stat) (); -} -glob64_t; - -/* -grp.h -*/ - -struct group -{ - char *gr_name; - char *gr_passwd; - __gid_t gr_gid; - char **gr_mem; -} -; - -/* -iconv.h -*/ - -typedef void *iconv_t; - -/* -inttypes.h -*/ - -typedef lldiv_t imaxdiv_t; - -typedef long long intmax_t; - -typedef unsigned long long uintmax_t; - -/* -locale.h -*/ - -struct lconv -{ - char *decimal_point; - char *thousands_sep; - char *grouping; - char *int_curr_symbol; - char *currency_symbol; - char *mon_decimal_point; - char *mon_thousands_sep; - char *mon_grouping; - char *positive_sign; - char *negative_sign; - char int_frac_digits; - char frac_digits; - char p_cs_precedes; - char p_sep_by_space; - char n_cs_precedes; - char n_sep_by_space; - char p_sign_posn; - char n_sign_posn; -} -; - -/* -nl_types.h -*/ - -typedef void *nl_catd; - -typedef int nl_item; - -/* -pwd.h -*/ - -struct passwd -{ - char *pw_name; - char *pw_passwd; - __uid_t pw_uid; - __gid_t pw_gid; - char *pw_gecos; - char *pw_dir; - char *pw_shell; -} -; - -/* -regex.h -*/ - -typedef unsigned long reg_syntax_t; - -typedef struct re_pattern_buffer -{ - unsigned char *buffer; - unsigned long allocated; - unsigned long used; - reg_syntax_t syntax; - char *fastmap; - char *translate; - size_t re_nsub; - unsigned int can_be_null; - unsigned int regs_allocated; - unsigned int fastmap_accurate; - unsigned int no_sub; - unsigned int not_bol; - unsigned int not_eol; - unsigned int newline_anchor; -} -regex_t; - -typedef int regoff_t; - -typedef struct -{ - regoff_t rm_so; - regoff_t rm_eo; -} -regmatch_t; - -/* -search.h -*/ - -typedef enum -{ - FIND, - ENTER -} -ACTION; - -typedef enum -{ - preorder, - postorder, - endorder, - leaf -} -VISIT; - -typedef struct entry -{ - char *key; - void *data; -} -ENTRY; - -typedef void (*__action_fn_t) (void *__nodep, VISIT __value, int __level); - -/* -setjmp.h -*/ - -typedef int __jmp_buf; - -typedef struct __jmp_buf_tag -{ - __jmp_buf __jmpbuf; - int __mask_was_saved; - __sigset_t __saved_mask; -} -jmp_buf; - -typedef jmp_buf sigjmp_buf; - -/* -signal.h -*/ - -typedef union sigval -{ - int sival_int; - void *sival_ptr; -} -sigval_t; - -typedef void (*__sighandler_t) (); - -struct sigevent -{ - sigval_t sigev_value; - int sigev_signo; - int sigev_notify; -} -; - -typedef struct -{ - unsigned long __val[1]; -} -__sigset_t; - -typedef __sigset_t sigset_t; - -struct sigaction; - -typedef struct -{ - int si_band; - int si_fd; - struct _sifields; - struct _sigpoll; -} -siginfo_t; - -struct sigaltstack -{ - void *ss_sp; - int ss_flags; - size_t ss_size; -} -; - -struct sigstack -{ - void *ss_sp; - int ss_onstack; -} -; - -/* -stdio.h -*/ - -typedef struct _IO_FILE FILE; - -typedef __off_t fpos_t; - -typedef __off64_t fpos64_t; - -/* -stdlib.h -*/ - -typedef struct -{ - long long quot; - long long rem; -} -lldiv_t; - -typedef struct -{ - int quot; - int rem; -} -div_t; - -typedef struct -{ - long quot; - long rem; -} -ldiv_t; - -typedef int (*__compar_fn_t) (); - -/* -sys/sem.h -*/ - -struct sembuf -{ - short sem_num; - short sem_op; - short sem_flg; -} -; - -/* -sys/socket.h -*/ - -typedef unsigned short sa_family_t; - -typedef unsigned int socklen_t; - -struct sockaddr -{ - sa_family_t sa_family; - char sa_data[1]; -} -; - -struct msghdr -{ - void *msg_name; - socklen_t msg_namelen; - struct iovec *msg_iov; - size_t msg_iovlen; - void *msg_control; - size_t msg_controllen; - int msg_flags; -} -; - -/* -sys/times.h -*/ - -struct tms -{ - clock_t tms_utime; - clock_t tms_stime; - clock_t tms_cutime; - clock_t tms_cstime; -} -; - -/* -sys/utsname.h -*/ - -struct utsname -{ - char sysname[1]; - char nodename[1]; - char release[1]; - char version[1]; - char machine[1]; - char __domainname[1]; -} -; - -/* -sys/wait.h -*/ - -typedef enum -{ - P_ALL, - P_PID, - P_PGID -} -idtype_t; - -/* -time.h -*/ - -typedef long __clock_t; - -struct timespec -{ - long tv_sec; - long tv_nsec; -} -; - -struct tm -{ - int tm_sec; - int tm_min; - int tm_hour; - int tm_mday; - int tm_mon; - int tm_year; - int tm_wday; - int tm_yday; - int tm_isdst; - long __tm_gmtoff; - char *__tm_zone; -} -; - -typedef __clock_t clock_t; - -typedef __time_t time_t; - -int adjtime (/*@notnull@*/ const struct timeval *delta, /*@null@*/ struct timeval *olddelta) - /*@warn superuser "Only super-user processes may call adjtime."@*/ - /*:statusreturn@*/ - /*@modifies systemState@*/ ; - -/* -unistd.h -*/ - -typedef __ssize_t ssize_t; - -typedef __pid_t pid_t; - -typedef __off_t off_t; - -extern /*@observer@*/ /*@nullterminated@*/ /*@null@*/ -char *bindtextdomain (/*@null@*/ /*@nullterminated@*/ const char *domainname, - /*@null@*/ /*@nullterminated@*/ const char *dirname) /*@*/ ; -/* LSB doesn't specify: taken from - http://www.hgmp.mrc.ac.uk/cgi-bin/man.cgi?section=3C&topic=bindtextdomain -*/ - - -/* -utime.h -*/ - -struct utimbuf -{ - __time_t actime; - __time_t modtime; -} -; - -/* -wchar.h -*/ - -typedef long wchar_t; - -typedef unsigned int wint_t; - -typedef struct -{ - int count; - wint_t value; -} -mbstate_t; - -/* -wctype.h -*/ - -typedef unsigned long wctype_t; - -typedef __int32_t *wctrans_t; - -/* -wordexp.h -*/ - -typedef struct -{ - int we_wordc; - char **we_wordv; - int we_offs; -} -wordexp_t; - -/* -timex.h -*/ - -struct timex { - int modes; /* mode selector */ - long offset; /* time offset (usec) */ - long freq; /* frequency offset (scaled ppm) */ - long maxerror; /* maximum error (usec) */ - long esterror; /* estimated error (usec) */ - int status; /* clock command/status */ - long constant; /* pll time constant */ - long precision; /* clock precision (usec) (read only) */ - long tolerance; /* clock frequency tolerance (ppm) (read only) */ - struct timeval time; /* current time (read only) */ - long tick; /* usecs between clock ticks */ - -}; - -/*@constant int ADJ_OFFSET@*/ -/*@constant int ADJ_FREQUENCY@*/ -/*@constant int ADJ_MAXERROR@*/ -/*@constant int ADJ_ESTERROR@*/ -/*@constant int ADJ_STATUS@*/ -/*@constant int ADJ_TIMECONST@*/ -/*@constant int ADJ_TICK@*/ -/*@constant int ADJ_OFFSET_SINGLESHOT@*/ - -int adjtimex (/*@notnull@*/ struct timex *buf) - /*@warn superuser "Only super-user processes may call adjtimex unless the modes field is 0."@*/ - /*:statusreturn@*/ - /*@modifies systemState@*/ ; - -/* -termios.h -*/ - -typedef unsigned char cc_t; -typedef unsigned int speed_t; -typedef unsigned int tcflag_t; - -struct termios -{ - tcflag_t c_iflag; /* input mode flags */ - tcflag_t c_oflag; /* output mode flags */ - tcflag_t c_cflag; /* control mode flags */ - tcflag_t c_lflag; /* local mode flags */ - cc_t c_cc[NCCS]; /* control characters */ -}; - -int cfmakeraw (/*@out@*/ struct termios *termios_p) - /*:statusreturn@*/ ; - -int cfsetspeed(struct termios *t, speedt speed) - /*:statusreturn@*/ ; - -/* -** Built in -*/ - -/*@exits@*/ void __assert_fail (/*@notnull@*/ const char *assertion, - /*@notnull@*/ const char *file, - unsigned int line, - /*@null@*/ const char *function) - /*@modifies stderr@*/; diff --git a/lib/posix.h b/lib/posix.h deleted file mode 100644 index a5a8bf0..0000000 --- a/lib/posix.h +++ /dev/null @@ -1,994 +0,0 @@ -/* -** posix.h -** -** Splint ISO C + POSIX Library -** -** This file should be processed together with standard.h to produce posix.lcd -** or posixstrict.lcd (the latter with -DSTRICT). -*/ - -/*@-nextlinemacros@*/ -/*@+allimponly@*/ -/*@+globsimpmodifiesnothing@*/ - -/* - * In 1988, IEEE Std 1003.1-1988, commonly known as "POSIX" or the - * "IEEE Portable Operating System Interface for Computing Environments" - * was published as an American National Standard. In 1990, IEEE Std - * 1003.1-1990 was published as an International Standard. The two - * standards differ slightly, and where they do, the 1990 International - * standard was used for this lclint library. The differences are: - * - * 1988: cuserid() - * 1990: -removed- (but still in this lclint library) - * - * 1988: int read (int, void*, unsigned int) - * 1990: ssize_t read (int, void*, size_t) - * - * 1988: int write (int, const void*, unsigned int) - * 1990: ssize_t write (int, const void*, size_t) - * - * The other differences are in the semantics of functions. - */ - -/* - * The reference for the ISO C part of this library was - * Plauger, Brodie's "Standard C - A Reference", Prentice Hall. - * The reference for the POSIX part of this library was - * Donald Lewine's "POSIX Programmer's Guide", O'Reilly. - * Transcription by Jens Schweikhardt - */ - -/* - * Note that Amendment 1 to ISO C was published in 1995 after POSIX was out. - * Amendment 1 basically adds support for wide characters and iso 646 - * source character sets. In particular, there are three new headers: - * , , and - */ - -/* - * Each header has annotations in this order: - * - * 1) type definitions (if any) - * 2) constant definitions (if any) - * 3) structure definitions (if any) - * 4) function prototypes and externals (if any) - * - * 5) type definitions augmented by POSIX (if any) - * 6) constant definitions augmented by POSIX (if any) - * 7) structure definitions augmented by POSIX (if any) - * 8) function prototypes and externals augmented by POSIX (if any) - * - * Builtins are mentioned in the header where they appear according to ISO. - */ - -/* -** sys/types.h -*/ - -typedef /*@integraltype@*/ dev_t; -typedef /*@integraltype@*/ gid_t; -typedef /*@unsignedintegraltype@*/ ino_t; /*: is this definitely unsigned? */ -typedef /*@integraltype@*/ mode_t; -typedef /*@integraltype@*/ nlink_t; -typedef /*@integraltype@*/ off_t; -typedef /*@integraltype@*/ pid_t; -typedef /*@integraltype@*/ uid_t; - -/* -** dirent.h -*/ - -typedef /*@abstract@*/ /*@mutable@*/ void *DIR; - -struct dirent { - char d_name[]; -}; - -extern int closedir (DIR *dirp) - /*@modifies errno@*/; - - /*drl 1/4/2001 added the dependent annotation as suggested by - Ralf Wildenhues */ - -extern /*@null@*/ /*@dependent@*/ DIR *opendir (const char *dirname) - /*@modifies errno, fileSystem@*/; - -extern /*@dependent@*/ /*@null@*/ struct dirent *readdir (DIR *dirp) - /*@modifies errno@*/; - -extern void rewinddir (DIR *dirp) - /*@*/; - -/* -** errno.h -*/ - -/*@constant int E2BIG@*/ -/*@constant int EACCES@*/ -/*@constant int EAGAIN@*/ -/*@constant int EBADF@*/ -/*@constant int EBUSY@*/ -/*@constant int ECHILD@*/ -/*@constant int EDEADLK@*/ -/*@constant int EEXIST@*/ -/*@constant int EFAULT@*/ -/*@constant int EFBIG@*/ -/*@constant int EINTR@*/ -/*@constant int EINVAL@*/ -/*@constant int EIO@*/ -/*@constant int EISDIR@*/ -/*@constant int EMFILE@*/ -/*@constant int EMLINK@*/ -/*@constant int ENAMETOOLONG@*/ -/*@constant int ENFILE@*/ -/*@constant int ENODEV@*/ -/*@constant int ENOENT@*/ -/*@constant int ENOEXEC@*/ -/*@constant int ENOLCK@*/ -/*@constant int ENOMEM@*/ -/*@constant int ENOSPC@*/ -/*@constant int ENOSYS@*/ -/*@constant int ENOTDIR@*/ -/*@constant int ENOTEMPTY@*/ -/*@constant int ENOTTY@*/ -/*@constant int ENXIO@*/ -/*@constant int EPERM@*/ -/*@constant int EPIPE@*/ -/*@constant int EROFS@*/ -/*@constant int ESPIPE@*/ -/*@constant int ESRCH@*/ -/*@constant int EXDEV@*/ - -/* -** fcntl.h -*/ - -/*@constant int FD_CLOEXEC@*/ -/*@constant int F_DUPFD@*/ -/*@constant int F_GETFD@*/ -/*@constant int F_GETFL@*/ -/*@constant int F_GETLK@*/ -/*@constant int F_RDLCK@*/ -/*@constant int F_SETFD@*/ -/*@constant int F_SETFL@*/ -/*@constant int F_SETLK@*/ -/*@constant int F_SETLKW@*/ -/*@constant int F_UNLCK@*/ -/*@constant int F_WRLCK@*/ -/*@constant int O_ACCMODE@*/ -/*@constant int O_APPEND@*/ -/*@constant int O_CREAT@*/ -/*@constant int O_EXCL@*/ -/*@constant int O_NOCTTY@*/ -/*@constant int O_NONBLOCK@*/ -/*@constant int O_RDONLY@*/ -/*@constant int O_RDWR@*/ -/*@constant int O_TRUNC@*/ -/*@constant int O_WRONLY@*/ -/*@constant int SEEK_CUR@*/ -/*@constant int SEEK_END@*/ -/*@constant int SEEK_SET@*/ - -/*@constant mode_t S_IFMT@*/ -/*@constant mode_t S_IFBLK@*/ -/*@constant mode_t S_IFCHR@*/ -/*@constant mode_t S_IFIFO@*/ -/*@constant mode_t S_IFREG@*/ -/*@constant mode_t S_IFDIR@*/ -/*@constant mode_t S_IFLNK@*/ - -/*@constant mode_t S_IRWXU@*/ -/*@constant mode_t S_IRUSR@*/ - -/*@constant mode_t S_IRGRP@*/ -/*@constant mode_t S_IROTH@*/ -/*@constant mode_t S_IUSR@*/ -/*@constant mode_t S_IWXG@*/ -/*@constant mode_t S_IWXO@*/ -/*@constant mode_t S_IWXU@*/ -/*@constant mode_t S_ISGID@*/ -/*@constant mode_t S_ISUID@*/ -/*@constant mode_t S_IWGRP@*/ -/*@constant mode_t S_IWOTH@*/ -/*@constant mode_t S_IWUSR@*/ -/*@constant mode_t S_IXGRP@*/ -/*@constant mode_t S_IXOTH@*/ -/*@constant mode_t S_IXUSR@*/ - -struct flock { - short l_type; - short l_whence; - off_t l_start; - off_t l_len; - pid_t l_pid; -}; - -extern int creat (const char *path, mode_t mode) - /*@modifies errno@*/; - -extern int fcntl (int fd, int cmd, ...) - /*@modifies errno@*/; - -extern int open (const char *path, int oflag, ...) - /*:checkerror -1 - returns -1 on error */ - /* the ... is one mode_t param */ - /*@modifies errno@*/ ; - -/* -** grp.h -*/ - -struct group { - char *gr_name; - gid_t gr_gid; - char **gr_mem; -}; - -/* evans 2002-07-09: added observer annotation (reported by Enrico Scholz). */ - -/*@observer@*/ /*@null@*/ struct group * getgrgid (gid_t gid) - /*@modifies errno@*/; - -/*@observer@*/ /*@null@*/ struct group *getgrnam (const char *nm) - /*@modifies errno@*/; - -/* -** limits.h -*/ - -/* These are always defined: */ - -/*@constant int CHAR_BIT@*/ -/*@constant char CHAR_MIN@*/ -/*@constant char CHAR_MAX@*/ -/*@constant int INT_MIN@*/ -/*@constant int INT_MAX@*/ -/*@constant long LONG_MIN@*/ -/*@constant long LONG_MAX@*/ -/*@constant int MB_LEN_MAX@*/ -/*@constant signed char SCHAR_MIN@*/ -/*@constant signed char SCHAR_MAX@*/ -/*@constant short SHRT_MIN@*/ -/*@constant short SHRT_MAX@*/ -/*@constant unsigned char UCHAR_MAX@*/ -/*@constant unsigned int UINT_MAX@*/ -/*@constant unsigned long ULONG_MAX@*/ -/*@constant unsigned short USHRT_MAX@*/ - -/* When _POSIX_SOURCE is defined */ - -/*@constant long ARG_MAX@*/ -/*@constant long CHILD_MAX@*/ -/*@constant long LINK_MAX@*/ -/*@constant long MAX_CANON@*/ -/*@constant size_t MAX_INPUT@*/ /* evans 2001-10-15 changed type to size_t from long */ -/*@constant size_t NAME_MAX@*/ /* evans 2001-10-15 changed type to size_t from long */ -/*@constant long NGROUPS_MAX@*/ -/*@constant long OPEN_MAX@*/ -/*@constant size_t PATH_MAX@*/ /* evans 2001-10-15 changed type to size_t from long */ -/*@constant size_t PIPE_BUF@*/ /* evans 2001-10-15 changed type to size_t from long */ -/*@constant long SSIZE_MAX@*/ -/*@constant long STREAM_MAX@*/ -/*@constant long TZNAME_MAX@*/ -/*@constant long _POSIX_ARG_MAX@*/ -/*@constant long _POSIX_CHILD_MAX@*/ -/*@constant long _POSIX_LINK_MAX@*/ -/*@constant long _POSIX_MAX_CANON@*/ -/*@constant long _POSIX_MAX_INPUT@*/ -/*@constant long _POSIX_NAME_MAX@*/ -/*@constant long _POSIX_NGROUPS_MAX@*/ -/*@constant long _POSIX_OPEN_MAX@*/ -/*@constant long _POSIX_PATH_MAX@*/ -/*@constant long _POSIX_PIPE_BUF@*/ -/*@constant long _POSIX_SSIZE@*/ -/*@constant long _POSIX_STREAM@*/ -/*@constant long _POSIX_TZNAME_MAX@*/ - -/* -** pwd.h -*/ - -struct passwd { - char *pw_name; - uid_t pw_uid; - gid_t pw_gid; - char *pw_dir; - char *pw_shell; -} ; - -/*@observer@*/ /*@null@*/ struct passwd *getpwnam (const char *) - /*@modifies errno@*/ /*@ensures maxRead(result) == 0 /\ maxSet(result) == 0 @*/; - -/*@observer@*/ /*@null@*/ struct passwd *getpwuid (uid_t uid) - /*@modifies errno@*/ /*@ensures maxRead(result) == 0 /\ maxSet(result) == 0 @*/; - -/* -** setjmp.h -*/ - -typedef /*@abstract@*/ /*@mutable@*/ void *sigjmp_buf; - -/*@mayexit@*/ void siglongjmp (sigjmp_buf env, int val) /*@*/; - -int sigsetjmp (/*@out@*/ sigjmp_buf env, int savemask) /*@modifies env@*/; - -/* -** moved up from signal.h -*/ - -typedef /*@abstract@*/ /*@immutable@*/ sigset_t; - -typedef struct { - void *ss_sp; - size_t ss_size; - int ss_flags; -} stack_t; - -/* -** ucontext.h -*/ - -typedef /*@abstract@*/ mcontext_t; - -typedef struct s_ucontext_t { - /*@null@*/ struct s_ucontext_t *uc_link; - sigset_t uc_sigmask; - stack_t uc_stack; - mcontext_t uc_mcontext; -} ucontext_t; - -int getcontext(ucontext_t *); -int setcontext(const ucontext_t *); -void makecontext(ucontext_t *, void (*)(void), int, ...); -int swapcontext(ucontext_t *restrict, const ucontext_t *restrict); - -/* -** signal.h -*/ - -/*@constant int SA_NOCLDSTOP@*/ -/*@constant int SIG_BLOCK@*/ -/*@constant int SIG_SETMASK@*/ -/*@constant int SIG_UNBLOCK@*/ -/*@constant int SIGALRM@*/ -/*@constant int SIGCHLD@*/ -/*@constant int SIGCONT@*/ -/*@constant int SIGHUP@*/ -/*@constant int SIGKILL@*/ -/*@constant int SIGPIPE@*/ -/*@constant int SIGQUIT@*/ -/*@constant int SIGSTOP@*/ -/*@constant int SIGTSTP@*/ -/*@constant int SIGTTIN@*/ -/*@constant int SIGTTOU@*/ -/*@constant int SIGUSR1@*/ -/*@constant int SIGUSR2@*/ - -struct sigstack { - int ss_onstack; - void *ss_sp; -} ; - -typedef struct { - int si_signo; - int si_errno; - int si_code; - pid_t si_pid; - uid_t si_uid; - void *si_addr; - int si_status; - long si_band; - union sigval si_value; -} siginfo_t; - -typedef union { - int sival_int; - void *sival_ptr; -} sigval; - -struct sigaction { - void (*sa_handler)(); - sigset_t sa_mask; - int sa_flags; - void (*sa_sigaction)(int, siginfo_t *, void *); /* Added 2003-06-13: Noticed by Jerry James */ -} ; - - extern /*@mayexit@*/ int -kill (pid_t pid, int sig) - /*@modifies errno@*/; - - extern int -sigaction (int sig, /*@null@*/ const struct sigaction *act, /*@out@*/ /*@null@*/ struct sigaction *oact) - /*@modifies *oact, errno, systemState@*/; - - extern int -sigaddset (sigset_t *set, int signo) - /*@modifies *set, errno@*/; - - extern int -sigdelset (sigset_t *set, int signo) - /*@modifies *set, errno@*/; - - extern int -sigemptyset (/*@out@*/ sigset_t *set) - /*@modifies *set, errno@*/; - - extern int -sigfillset (/*@out@*/ sigset_t *set) - /*@modifies *set, errno@*/; - - extern int -sigismember (const sigset_t *set, int signo) - /*@modifies errno@*/; - - extern int -sigpending (/*@out@*/ sigset_t *set) - /*@modifies *set, errno@*/; - - extern int -sigprocmask (int how, /*@null@*/ const sigset_t *set, /*@null@*/ /*@out@*/ sigset_t *oset) - /*@modifies *oset, errno, systemState@*/; - - extern int -sigsuspend (const sigset_t *sigmask) - /*@modifies errno, systemState@*/; - -/* -** stdio.h -*/ - -/*@constant int L_ctermid@*/ -/*@constant int L_cuserid@*/ -/*@constant int STREAM_MAX@*/ - -extern /*@null@*/ /*@dependent@*/ FILE *fdopen (int fd, const char *type) - /*@modifies errno, fileSystem@*/; - -extern int fileno (FILE *fp) /*@modifies errno@*/; - -/* -** sys/stat.h -*/ - -struct stat { - mode_t st_mode; - ino_t st_ino; - dev_t st_dev; - nlink_t st_nlink; - uid_t st_uid; - gid_t st_gid; - off_t st_size; - time_t st_atime; /* evans 2001-08-23 - these were previously st_st_atime - POSIX spec says st_atime */ - time_t st_mtime; /* evans 2001-08-23 - these were previously st_st_mtime - POSIX spec says st_mtime */ - time_t st_ctime; /* evans 2001-08-23 - these were previously st_st_ctime - POSIX spec says st_ctime */ -} ; -/* -** evans 2004-05-19: dependent annotations atted for time_t fields. Could not find -** any clear documetation on this, but it seems to be correct. -*/ - -/* -** POSIX does not require that the S_I* be functions. They're -** macros virtually everywhere. -*/ - -# ifdef STRICT -/*@notfunction@*/ -# define SBOOLINT _Bool /*@alt int@*/ -# else -/*@notfunction@*/ -# define SBOOLINT _Bool -# endif - -extern SBOOLINT S_ISBLK (/*@sef@*/ mode_t m) /*@*/ ; - -extern SBOOLINT S_ISCHR (/*@sef@*/ mode_t m) /*@*/ ; - -extern SBOOLINT S_ISDIR (/*@sef@*/ mode_t m) /*@*/ ; - -extern SBOOLINT S_ISFIFO (/*@sef@*/ mode_t m) /*@*/ ; - -extern SBOOLINT S_ISREG (/*@sef@*/ mode_t m) /*@*/ ; - -int chmod (const char *path, mode_t mode) - /*@modifies fileSystem, errno@*/ ; - -int fstat (int fd, /*@out@*/ struct stat *buf) - /*@modifies errno, *buf@*/ ; - -int mkdir (const char *path, mode_t mode) - /*@modifies fileSystem, errno@*/; - -int mkfifo (const char *path, mode_t mode) - /*@modifies fileSystem, errno@*/; - -int stat (const char *path, /*@out@*/ struct stat *buf) - /*:errorcode -1*/ - /*@modifies errno, *buf@*/; - -int umask (mode_t cmask) - /*@modifies systemState@*/; - -/* -** sys/times.h -*/ - -struct tms { - clock_t tms_utime; - clock_t tms_stime; - clock_t tms_cutime; - clock_t tms_cstime; -}; - - extern clock_t -times (/*@out@*/ struct tms *tp) - /*@modifies *tp@*/; - -/* -** sys/utsname.h -*/ - -struct utsname { - char sysname[]; - char nodename[]; - char release[]; - char version[]; - char machine[]; -}; - - extern int -uname (/*@out@*/ struct utsname *name) - /*@modifies *name, errno@*/ ; - -/* -** sys/wait.h -*/ - -extern int WEXITSTATUS (int status) /*@*/ ; -extern int WIFEXITED (int status) /*@*/ ; -extern int WIFSIGNALED (int status) /*@*/ ; -extern int WIFSTOPPED (int status) /*@*/ ; -extern int WSTOPSIG (int status) /*@*/ ; -extern int WTERMSIG (int status) /*@*/ ; - -/*@constant int WUNTRACED@*/ - -/* These are in Unix spec, are they in POSIX? */ -/*@constant int WCONTINUED@*/ -/*@constant int WNOHANG@*/ - -pid_t wait (/*@out@*/ /*@null@*/ int *st) - /*@modifies *st, errno, systemState@*/; - -pid_t waitpid (pid_t pid, /*@out@*/ /*@null@*/ int *st, int opt) - /*@modifies *st, errno, systemState@*/; - -/* -** termios.h -*/ - -typedef unsigned char /*@alt unsigned short@*/ cc_t; -typedef unsigned long /*@alt long@*/ speed_t; -typedef unsigned long /*@alt long@*/ tcflag_t; - -/*@constant int B0@*/ -/*@constant int B50@*/ -/*@constant int B75@*/ -/*@constant int B110@*/ -/*@constant int B134@*/ -/*@constant int B150@*/ -/*@constant int B200@*/ -/*@constant int B300@*/ -/*@constant int B600@*/ -/*@constant int B1200@*/ -/*@constant int B1800@*/ -/*@constant int B2400@*/ -/*@constant int B4800@*/ -/*@constant int B9600@*/ -/*@constant int B19200@*/ -/*@constant int B38400@*/ -/*@constant int BRKINT@*/ -/*@constant int CLOCAL@*/ -/*@constant int CREAD@*/ -/*@constant int CS5@*/ -/*@constant int CS6@*/ -/*@constant int CS7@*/ -/*@constant int CS8@*/ -/*@constant int CSIZE@*/ -/*@constant int CSTOPB@*/ -/*@constant int ECHO@*/ -/*@constant int ECHOE@*/ -/*@constant int ECHOK@*/ -/*@constant int ECHONL@*/ -/*@constant int HUPCL@*/ -/*@constant int ICANON@*/ -/*@constant int ICRNL@*/ -/*@constant int IEXTEN@*/ -/*@constant int IGNBRK@*/ -/*@constant int IGNCR@*/ -/*@constant int IGNPAR@*/ -/*@constant int IGNLCR@*/ -/*@constant int INPCK@*/ -/*@constant int ISIG@*/ -/*@constant int ISTRIP@*/ -/*@constant int IXOFF@*/ -/*@constant int IXON@*/ -/*@constant int NCCS@*/ -/*@constant int NOFLSH@*/ -/*@constant int OPOST@*/ -/*@constant int PARENB@*/ -/*@constant int PARMRK@*/ -/*@constant int PARODD@*/ -/*@constant int TCIFLUSH@*/ -/*@constant int TCIOFF@*/ -/*@constant int TCIOFLUSH@*/ -/*@constant int TCION@*/ -/*@constant int TCOFLUSH@*/ -/*@constant int TCSADRAIN@*/ -/*@constant int TCSAFLUSH@*/ -/*@constant int TCSANOW@*/ -/*@constant int TOSTOP@*/ -/*@constant int VEOF@*/ -/*@constant int VEOL@*/ -/*@constant int VERASE@*/ -/*@constant int VINTR@*/ -/*@constant int VKILL@*/ -/*@constant int VMIN@*/ -/*@constant int VQUIT@*/ -/*@constant int VSTART@*/ -/*@constant int VSTOP@*/ -/*@constant int VSUSP@*/ -/*@constant int VTIME@*/ - -struct termios { - tcflag_t c_iflag; - tcflag_t c_oflag; - tcflag_t c_cflag; - tcflag_t c_lflag; - cc_t c_cc; -} ; - - extern speed_t -cfgetispeed (const struct termios *p) - /*@*/; - - extern speed_t -cfgetospeed (const struct termios *p) - /*@*/; - - extern int -cfsetispeed (struct termios *p) - /*@modifies *p@*/; - - extern int -cfsetospeed (struct termios *p) - /*@modifies *p@*/; - - extern int -tcdrain (int fd) - /*@modifies errno@*/; - - extern int -tcflow (int fd, int action) - /*@modifies errno@*/; - - extern int -tcflush (int fd, int qs) - /*@modifies errno@*/; - - extern int -tcgetattr (int fd, /*@out@*/ struct termios *p) - /*@modifies errno, *p@*/; - - extern int -tcsendbreak (int fd, int d) - /*@modifies errno@*/; - - extern int -tcsetattr (int fd, int opt, const struct termios *p) - /*@modifies errno@*/; - -/* -** time.h -*/ - -/* Environ must be known before it can be used in `globals' clauses. */ - -/*@unchecked@*/ extern char **environ; - -/*@constant int CLK_TCK@*/ - - extern void -tzset (void) - /*@globals environ@*/ /*@modifies systemState@*/; - -/* -** unistd.h -*/ - -/*@constant int F_OK@*/ -/*@constant int R_OK@*/ -/*@constant int SEEK_CUR@*/ -/*@constant int SEEK_END@*/ -/*@constant int SEEK_SET@*/ -/*@constant int STDERR_FILENO@*/ -/*@constant int STDIN_FILENO@*/ -/*@constant int STDOUT_FILENO@*/ -/*@constant int W_OK@*/ -/*@constant int X_OK@*/ -/*@constant int _PC_CHOWN_RESTRUCTED@*/ -/*@constant int _PC_MAX_CANON@*/ -/*@constant int _PC_MAX_INPUT@*/ -/*@constant int _PC_NAME_MAX@*/ -/*@constant int _PC_NO_TRUNC@*/ -/*@constant int _PC_PATH_MAX@*/ -/*@constant int _PC_PIPE_BUF@*/ -/*@constant int _PC_VDISABLE@*/ -/*@constant int _POSIX_CHOWN_RESTRICTED@*/ -/*@constant int _POSIX_JOB_CONTROL@*/ -/*@constant int _POSIX_NO_TRUNC@*/ -/*@constant int _POSIX_SAVED_IDS@*/ -/*@constant int _POSIX_VDISABLE@*/ -/*@constant int _POSIX_VERSION@*/ -/*@constant int _SC_ARG_MAX@*/ -/*@constant int _SC_CHILD_MAX@*/ -/*@constant int _SC_CLK_TCK@*/ -/*@constant int _SC_JOB_CONTROL@*/ -/*@constant int _SC_NGROUPS_MAX@*/ -/*@constant int _SC_OPEN_MAX@*/ -/*@constant int _SC_SAVED_IDS@*/ -/*@constant int _SC_STREAM_MAX@*/ -/*@constant int _SC_TZNAME_MAX@*/ -/*@constant int _SC_VERSION@*/ - -extern /*@exits@*/ void _exit (int status) /*@*/; - -extern int access (const char *path, int mode) /*@modifies errno@*/; - -extern unsigned int alarm (unsigned int) /*@modifies systemState@*/; - -extern int chdir (const char *path) /*@modifies errno@*/; - -extern int chown (const char *path, uid_t owner, gid_t group) - /*@modifies fileSystem, errno@*/; - - extern int -close (int fd) - /*@modifies fileSystem, errno, systemState@*/; - /* state: record locks are unlocked */ - - extern char * -ctermid (/*@returned@*/ /*@out@*/ /*@null@*/ char *s) - /*@modifies *s, systemState@*/; - - /* cuserid is in the 1988 version of POSIX but removed in 1990 */ - extern char * -cuserid (/*@null@*/ /*@out@*/ char *s) - /*@modifies *s@*/; - - extern int -dup2 (int fd, int fd2) - /*@modifies errno, fileSystem@*/; - - extern int -dup (int fd) - /*@modifies errno, fileSystem@*/; - - extern /*@mayexit@*/ int -execl (const char *path, const char *arg, ...) - /*@modifies errno@*/; - - extern /*@mayexit@*/ int -execle (const char *file, const char *arg, ...) - /*@modifies errno@*/; - - extern /*@mayexit@*/ int -execlp (const char *file, const char *arg, ...) - /*@modifies errno@*/; - - extern /*@mayexit@*/ int -execv (const char *path, char *const argv[]) - /*@modifies errno@*/; - - extern /*@mayexit@*/ int -execve (const char *path, char *const argv[], char *const *envp) - /*@modifies errno@*/; - - extern /*@mayexit@*/ int -execvp (const char *file, char *const argv[]) - /*@modifies errno@*/; - - extern pid_t -fork (void) - /*@modifies fileSystem, errno@*/; - - extern long -fpathconf (int fd, int name) - /*@modifies errno@*/; - -extern /*@null@*/ char *getcwd (/*@returned@*/ /*@out@*/ /*@notnull@*/ char *buf, size_t size) - /*@requires maxSet(buf) >= (size - 1)@*/ - /*@ensures maxRead(buf) <= (size - 1)@*/ - - /*@modifies errno, *buf@*/ ; - - extern gid_t -getegid (void) - /*@*/; - - extern uid_t -geteuid (void) - /*@*/; - - extern gid_t -getgid (void) - /*@*/; - - extern int -getgroups (int gs, /*@out@*/ gid_t gl[]) - /*@modifies errno, gl[]@*/; - - extern /*@observer@*/ char * -getlogin (void) - /*@*/; - - extern pid_t -getpgrp (void) - /*@*/; - - extern pid_t -getpid (void) - /*@*/; - - extern pid_t -getppid (void) - /*@*/; - - extern uid_t -getuid (void) - /*@*/; - - extern int -isatty (int fd) - /*@*/; - - extern int -link (const char *o, const char *n) - /*@modifies errno, fileSystem@*/; - - extern off_t -lseek (int fd, off_t offset, int whence) - /*@modifies errno@*/; - - extern long -pathconf (const char *path, int name) - /*@modifies errno@*/; - - extern int -pause (void) - /*@modifies errno@*/; - - extern int -pipe (/*@out@*/ int fd[]) /* Out parameter noticed by Marc Espie. */ - /*@modifies errno@*/; - -extern ssize_t read (int fd, /*@out@*/ void *buf, size_t nbyte) - /*@modifies errno, *buf@*/ - /*@requires maxSet(buf) >= (nbyte - 1) @*/ - /*@ensures maxRead(buf) >= nbyte @*/ ; - -extern int rmdir (const char *path) - /*@modifies fileSystem, errno@*/; - -extern int setgid (gid_t gid) - /*@modifies errno, systemState@*/; - -extern int setpgid (pid_t pid, pid_t pgid) - /*@modifies errno, systemState@*/; - -extern pid_t setsid (void) /*@modifies systemState@*/; - -extern int setuid (uid_t uid) - /*@modifies errno, systemState@*/; - -unsigned int sleep (unsigned int sec) /*@modifies systemState@*/ ; - -extern long sysconf (int name) - /*@modifies errno@*/; - -extern pid_t tcgetpgrp (int fd) - /*@modifies errno@*/; - -extern int tcsetpgrp (int fd, pid_t pgrpid) - /*@modifies errno, systemState@*/; - -/* Q: observer ok? */ -extern /*@null@*/ /*@observer@*/ char *ttyname (int fd) - /*@modifies errno@*/; - -extern int unlink (const char *path) - /*@modifies fileSystem, errno@*/; - -extern ssize_t write (int fd, const void *buf, size_t nbyte) - /*@requires maxRead(buf) >= nbyte@*/ - /*@modifies errno@*/; - -/* -** utime.h -*/ - -struct utimbuf { - time_t actime; - time_t modtime; -} ; - - extern int -utime (const char *path, /*@null@*/ const struct utimbuf *times) - /*@modifies fileSystem, errno@*/; - -/* -** regex.h -*/ - -typedef /*@abstract@*/ /*@mutable@*/ void *regex_t; -typedef /*@integraltype@*/ regoff_t; - -typedef struct -{ - regoff_t rm_so; - regoff_t rm_eo; -} regmatch_t; - -int regcomp (/*@out@*/ regex_t *preg, /*@nullterminated@*/ const char *regex, int cflags) - /*:statusreturn@*/ - /*@modifies preg@*/ ; - -int regexec (const regex_t *preg, /*@nullterminated@*/ const char *string, size_t nmatch, /*@out@*/ regmatch_t pmatch[], int eflags) - /*@requires maxSet(pmatch) >= nmatch@*/ - /*@modifies pmatch@*/ ; - -size_t regerror (int errcode, const regex_t *preg, /*@out@*/ char *errbuf, size_t errbuf_size) - /*@requires maxSet(errbuf) >= errbuf_size@*/ - /*@modifies errbuf@*/ ; - -void regfree (/*@only@*/ regex_t *preg) ; - -/* regcomp flags */ -/*@constant int REG_BASIC@*/ -/*@constant int REG_EXTENDED@*/ -/*@constant int REG_ICASE@*/ -/*@constant int REG_NOSUB@*/ -/*@constant int REG_NEWLINE@*/ -/*@constant int REG_NOSPEC@*/ -/*@constant int REG_PEND@*/ -/*@constant int REG_DUMP@*/ - -/* regerror flags */ -/*@constant int REG_NOMATCH@*/ -/*@constant int REG_BADPAT@*/ -/*@constant int REG_ECOLLATE@*/ -/*@constant int REG_ECTYPE@*/ -/*@constant int REG_EESCAPE@*/ -/*@constant int REG_ESUBREG@*/ -/*@constant int REG_EBRACK@*/ -/*@constant int REG_EPAREN@*/ -/*@constant int REG_EBRACE@*/ -/*@constant int REG_BADBR@*/ -/*@constant int REG_ERANGE@*/ -/*@constant int REG_ESPACE@*/ -/*@constant int REG_BADRPT@*/ -/*@constant int REG_EMPTY@*/ -/*@constant int REG_ASSERT@*/ -/*@constant int REG_INVARG@*/ -/*@constant int REG_ATOI@*/ /* non standard */ -/*@constant int REG_ITOA@*/ /* non standard */ - -/* regexec flags */ -/*@constant int REG_NOTBOL@*/ -/*@constant int REG_NOTEOL@*/ -/*@constant int REG_STARTEND@*/ -/*@constant int REG_TRACE@*/ -/*@constant int REG_LARGE@*/ -/*@constant int REG_BACKR@*/ - diff --git a/lib/standard.h b/lib/standard.h deleted file mode 100644 index 2a2b261..0000000 --- a/lib/standard.h +++ /dev/null @@ -1,1271 +0,0 @@ -/* -** standard.h --- ISO C99 Standard Library for Splint. -** -** Process with -DSTRICT to get strict library. -*/ - -/*@-nextlinemacros@*/ -/*@+allimponly@*/ -/*@+globsimpmodifiesnothing@*/ - -/* -** errno.h -*/ - -/*@constant int EDOM;@*/ -/*@constant int ERANGE;@*/ -/*@constant int EILSEQ;@*/ - -# ifdef STRICT -/*@checkedstrict@*/ int errno; -# else -/*@unchecked@*/ int errno; -# endif - -/* -** stdbool.h -*/ - -/*@-likelybool@*/ -typedef _Bool bool; -/*@=likelybool@*/ -/*@constant bool true@*/ -/*@constant bool false@*/ -/*@constant int __bool_true_false_are_defined = 1@*/ - -/* -** types -*/ - -typedef /*@integraltype@*/ ptrdiff_t; -typedef /*@unsignedintegraltype@*/ size_t; -typedef /*@signedintegraltype@*/ ssize_t; -typedef /*@integraltype@*/ wchar_t; - -/* -** Added by Amendment 1 to ISO. -*/ - -typedef /*@integraltype@*/ wint_t; -typedef /*@abstract@*/ mbstate_t; - -/*@constant null anytype NULL = 0;@*/ - -/* -** assert.h -*/ - -/*@constant _Bool NDEBUG;@*/ - -# ifdef STRICT -/*@falseexit@*/ void assert (/*@sef@*/ _Bool e) - /*@*/ ; -# else -/*@falseexit@*/ void assert (/*@sef@*/ _Bool /*@alt int@*/ e) - /*@*/ ; -# endif - - -/* -** ctype.h -*/ - -# ifdef STRICT -_Bool isalnum (int c) /*@*/ ; -_Bool isalpha (int c) /*@*/ ; -_Bool iscntrl (int c) /*@*/ ; -_Bool isdigit (int c) /*@*/ ; -_Bool isgraph (int c) /*@*/ ; -_Bool islower (int c) /*@*/ ; -_Bool isprint (int c) /*@*/ ; -_Bool ispunct (int c) /*@*/ ; -_Bool isspace (int c) /*@*/ ; -_Bool isupper (int c) /*@*/ ; -_Bool isxdigit (int c) /*@*/ ; -char tolower (int c) /*@*/ ; -char toupper (int c) /*@*/ ; -# else -/* -** evans 2002-01-03: added alt char (was alt unsigned char) -*/ - -_Bool /*@alt int@*/ isalnum (int /*@alt char, unsigned char@*/ c) /*@*/ ; -_Bool /*@alt int@*/ isalpha (int /*@alt char, unsigned char@*/ c) /*@*/ ; -_Bool /*@alt int@*/ iscntrl (int /*@alt char, unsigned char@*/ c) /*@*/ ; -_Bool /*@alt int@*/ isdigit (int /*@alt char, unsigned char@*/ c) /*@*/ ; -_Bool /*@alt int@*/ isgraph (int /*@alt char, unsigned char@*/ c) /*@*/ ; -_Bool /*@alt int@*/ islower (int /*@alt char, unsigned char@*/ c) /*@*/ ; -_Bool /*@alt int@*/ isprint (int /*@alt char, unsigned char@*/ c) /*@*/ ; -_Bool /*@alt int@*/ ispunct (int /*@alt char, unsigned char@*/ c) /*@*/ ; -_Bool /*@alt int@*/ isspace (int /*@alt char, unsigned char@*/ c) /*@*/ ; -_Bool /*@alt int@*/ isupper (int /*@alt char, unsigned char@*/ c) /*@*/ ; -_Bool /*@alt int@*/ isxdigit (int /*@alt char, unsigned char@*/ c) /*@*/ ; -char /*@alt int@*/ tolower (int /*@alt char, unsigned char@*/ c) /*@*/ ; -char /*@alt int@*/ toupper (int /*@alt char, unsigned char@*/ c) /*@*/ ; -# endif - -/* -** locale.h -*/ - -struct lconv -{ - char *decimal_point; - char *thousands_sep; - char *grouping; - char *int_curr_symbol; - char *currency_symbol; - char *mon_decimal_point; - char *mon_thousands_sep; - char *mon_grouping; - char *positive_sign; - char *negative_sign; - char int_frac_digits; - char frac_digits; - char p_cs_precedes; - char p_sep_by_space; - char n_cs_precedes; - char n_sep_by_space; - char p_sign_posn; - char n_sign_posn; -} ; - -/*@constant int LC_ALL;@*/ -/*@constant int LC_COLLATE;@*/ -/*@constant int LC_CTYPE;@*/ -/*@constant int LC_MONETARY;@*/ -/*@constant int LC_NUMERIC;@*/ -/*@constant int LC_TIME;@*/ - -/*@observer@*/ /*@null@*/ char *setlocale (int category, /*@null@*/ char *locale) - /*@modifies internalState, errno@*/ ; - -struct lconv *localeconv (void) /*@*/ ; - -/* -** float.h -*/ - -/* -** Note, these are defined by macros, but NOT necessarily -** constants. They may be used as lvalues. -*/ - -/*@unchecked@*/ int DBL_DIG; -/*@unchecked@*/ double DBL_EPSILON; -/*@unchecked@*/ int DBL_MANT_DIG; -/*@unchecked@*/ double DBL_MAX; -/*@unchecked@*/ int DBL_MAX_10_EXP; -/*@unchecked@*/ int DBL_MAX_EXP; -/*@unchecked@*/ double DBL_MIN; -/*@unchecked@*/ int DBL_MIN_10_EXP; -/*@unchecked@*/ int DBL_MIN_EXP; - -/*@unchecked@*/ int FLT_DIG; -/*@unchecked@*/ float FLT_EPSILON; -/*@unchecked@*/ int FLT_MANT_DIG; -/*@unchecked@*/ float FLT_MAX; -/*@unchecked@*/ int FLT_MAX_10_EXP; -/*@unchecked@*/ int FLT_MAX_EXP; -/*@unchecked@*/ float FLT_MIN; -/*@unchecked@*/ int FLT_MIN_10_EXP; -/*@unchecked@*/ int FLT_MIN_EXP; -/*@constant int FLT_RADIX@*/ -/*@unchecked@*/ int FLT_ROUNDS; - -/*@unchecked@*/ int LDBL_DIG; -/*@unchecked@*/ long double LDBL_EPSILON; -/*@unchecked@*/ int LDBL_MANT_DIG; -/*@unchecked@*/ long double LDBL_MAX; -/*@unchecked@*/ int LDBL_MAX_10_EXP; -/*@unchecked@*/ int LDBL_MAX_EXP; -/*@unchecked@*/ long double LDBL_MIN; -/*@unchecked@*/ int LDBL_MIN_10_EXP; -/*@unchecked@*/ int LDBL_MIN_EXP; - -/* -** limits.h -*/ - -/*@constant int CHAR_BIT; @*/ -/*@constant char CHAR_MAX; @*/ -/*@constant char CHAR_MIN; @*/ -/*@constant int INT_MAX; @*/ -/*@constant int INT_MIN; @*/ -/*@constant long int LONG_MAX; @*/ -/*@constant long int LONG_MIN; @*/ -/*@constant long int MB_LEN_MAX@*/ -/*@constant signed char SCHAR_MAX; @*/ -/*@constant signed char SCHAR_MIN; @*/ -/*@constant short SHRT_MAX; @*/ -/*@constant short SHRT_MIN; @*/ -/*@constant unsigned char UCHAR_MAX; @*/ -/*@constant unsigned int UINT_MAX; @*/ -/*@constant unsigned long ULONG_MAX; @*/ -/*@constant unsigned short USHRT_MAX; @*/ - -/* -** math.h -** -** evans 2002-07-03: updated from ISO C99 (http://www.vmunix.com/~gabor/c/draft.html) -*/ - -typedef float float_t; -typedef double double_t; - -/*@constant double HUGE_VAL; @*/ -/*@constant float HUGE_VALF; @*/ -/*@constant long double HUGE_VALL; @*/ - -/*@constant float INFINITY; @*/ - -/*@constant float NAN; @*/ - /*:warn implementationoptional "NAN is defined if and only if the implementation supports quiet float type NaNs.":*/ ; - -/*@constant int FP_INFINITE;@*/ -/*@constant int FP_NAN;@*/ -/*@constant int FP_NORMAL;@*/ -/*@constant int FP_SUBNORMAL;@*/ -/*@constant int FP_ZERO;@*/ - -/*@constant int FP_ILOGB0;@*/ -/*@constant int FP_ILOGBNAN;@*/ - -/*@constant int DECIMAL_DIG;@*/ - -/* Defined for specs only - this type is any real type */ -typedef float /*@alt double, long double@*/ s_real_t; - -int fpclassify (/*@sef@*/ s_real_t) /*@*/ ; -int signbit (/*@sef@*/ s_real_t) /*@*/ ; -int isfinite (/*@sef@*/ s_real_t) /*@*/ ; -int isnormal (/*@sef@*/ s_real_t) /*@*/ ; -int isnan (/*@sef@*/ s_real_t) /*@*/ ; -int isinf (/*@sef@*/ s_real_t) /*@*/ ; - -/* -** math functions that may have a range error modify errno (implementation defined). -*/ - -double acos (double x) /*@modifies errno@*/ ; -double asin (double x) /*@modifies errno@*/ ; -double atan (double x) /*@*/ ; -double atan2 (double y, double x) /*@*/ ; - -double cos (double x) /*@*/ ; -double sin (double x) /*@*/ ; -double tan (double x) /*@*/ ; - -double cosh (double x) /*@modifies errno@*/ ; -double sinh (double x) /*@modifies errno@*/ ; -double tanh (double x) /*@*/ ; - -double acosh (double x) /*@modifies errno@*/ ; -double asinh (double x) /*@modifies errno@*/ ; -double atanh (double x) /*@modifies errno@*/ ; - -double exp (double x) /*@modifies errno@*/ ; -double frexp (double x, /*@out@*/ int *xp) /*@modifies *xp;@*/ ; -double ldexp (double x, int n) /*@modifies errno@*/ ; - -double log (double x) /*@modifies errno@*/ ; -double log10 (double x) /*@modifies errno@*/ ; - -double modf (double x, /*@out@*/ double *ip) /*@modifies *ip;@*/ ; - -double exp2 (double x) /*@modifies errno@*/ ; -double expm1 (double x) /*@modifies errno@*/ ; -double log1p (double x) /*@modifies errno@*/ ; -double log2 (double x) /*@modifies errno@*/ ; -double logb (double x) /*@modifies errno@*/ ; - -double scalbn (double x, int n) /*@modifies errno@*/ ; -double scalbln (double x, long int n) /*@modifies errno@*/ ; -long double scalblnl(long double x, long int n) /*@modifies errno@*/ ; - -int ilogb (double x) /*@modifies errno@*/ ; -int ilogbf (float x) /*@modifies errno@*/ ; -int ilogbl (long double x) /*@modifies errno@*/ ; - -double fabs (double x) /*@*/ ; -float fabsf (float x) /*@*/ ; -long double fabsl (long double x) /*@*/ ; - -double pow (double x, double y) /*@modifies errno@*/ ; -float powf(float x, float y) /*@modifies errno@*/ ; -long double powl(long double x, long double y) /*@modifies errno@*/ ; - -double sqrt (double x) /*@modifies errno@*/ ; -float sqrtf(float x) /*@modifies errno@*/ ; -long double sqrtl (long double x) /*@modifies errno@*/ ; - -double cbrt (double x) /*@*/ ; -float cbrtf (float x) /*@*/ ; -long double cbrtl (long double x) /*@*/ ; - -double hypot (double x, double y) /*@modifies errno@*/ ; -float hypotf (float x, float y) /*@modifies errno@*/ ; -long double hypotl (long double x, long double y) /*@modifies errno@*/ ; - -double erf (double x) /*@*/ ; -double erfc (double x) /*@*/ ; -float erff (float x) /*@*/ ; -long double erfl (long double x) /*@*/ ; -float erfcf (float x) /*@*/ ; -long double erfcl (long double x) /*@*/ ; - -double gamma (double x) /*@modifies errno@*/ ; -float gammaf(float x) /*@modifies errno@*/ ; -long double gammal (long double x) /*@modifies errno@*/ ; -double lgamma (double x) /*@modifies errno@*/ ; -float lgammaf (float x) /*@modifies errno@*/ ; -long double lgammal (long double x) /*@modifies errno@*/ ; - -double ceil (double x) /*@*/ ; -float ceilf(float x) /*@*/ ; -long double ceill(long double x) /*@*/ ; - -double floor (double x) /*@*/ ; -float floorf (float x) /*@*/ ; -long double floorl (long double x) /*@*/ ; - -double nearbyint (double x) /*@*/ ; -float nearbyintf (float x) /*@*/ ; -long double nearbyintl (long double x) /*@*/ ; - -double rint (double x) /*@*/; -float rintf (float x) /*@*/ ; -long double rintl (long double x) /*@*/ ; -long int lrint (double x) /*@modifies errno@*/ ; -long int lrintf (float x) /*@modifies errno@*/ ; -long int lrintl (long double x) /*@modifies errno@*/ ; -long long llrint (double x) /*@modifies errno@*/ ; -long long llrintf(float x) /*@modifies errno@*/ ; -long long llrintl(long double x) /*@modifies errno@*/ ; - -double round (double x) /*@*/ ; -long int lround (double x) /*@modifies errno@*/ ; -long long llround (double x) /*@modifies errno@*/ ; - -double trunc (double x) /*@*/ ; -double fmod (double x, double y) /*@*/ ; -double remainder (double x, double y) /*@*/ ; -double remquo (double x, double y, /*@out@*/ int *quo) /*@modifies *quo@*/ ; -double copysign (double x, double y) /*@*/ ; -double nan (/*@nullterminated@*/ const char *tagp) /*@*/ ; -double nextafter (double x, double y) /*@*/ ; -double nextafterx (double x, long double y) /*@*/ ; - -double fdim (double x, double y) /*@modifies errno@*/ ; -double fmax (double x, double y) /*@*/ ; -double fmin (double x, double y) /*@*/ ; -double fma (double x, double y, double z) /*@*/ ; - -int isgreater (s_real_t x, s_real_t y) /*@*/ ; -int isgreaterequal (s_real_t x, s_real_t y) /*@*/ ; -int isless (s_real_t x, s_real_t y) /*@*/ ; -int islessequal (s_real_t x, s_real_t y) /*@*/ ; -int islessgreater (s_real_t x, s_real_t y) /*@*/ ; -int isunordered (s_real_t x, s_real_t y) /*@*/ ; - -/* -** These functions are optional in iso C. An implementation does not -** have to provide them. They are included in comments here, but -** are not required to be part of the standard library. -*/ - -# ifdef OPTIONAL_MATH - -float acosf (float x) /*@modifies errno@*/ ; -long double acosl (long double x) /*@modifies errno@*/ ; -float asinf (float x) /*@modifies errno@*/ ; -long double asinl (long double x) /*@modifies errno@*/ ; -float atanf (float x) /*@*/ ; -long double atanl (long double x) /*@*/ ; -float atan2f (float y, float x) /*@*/ ; -long double atan2l (long double y, long double x) /*@*/ ; -float ceilf (float x) /*@*/ ; -long double ceill (long double x) /*@*/ ; -float cosf (float x) /*@*/ ; -long double cosl (long double x) /*@*/ ; -float coshf (float x) /*@modifies errno@*/ ; -long double coshl (long double x) /*@modifies errno@*/ ; -float expf (float x) /*@modifies errno@*/ ; -long double expl (long double x) /*@modifies errno@*/; -float fabsf (float x) /*@*/ ; -long double fabsl (long double x) /*@*/ ; -float floorf (float x) /*@*/ ; -long double floorl (long double x) /*@*/ ; -float fmodf (float x, float y) /*@*/ ; -long double fmodl (long double x, long double y) /*@*/ ; -float frexpf (float x, /*@out@*/ int *xp) /*@modifies *xp@*/; -long double frexpl (long double x, /*@out@*/ int *xp) /*@modifies *xp@*/; -float ldexpf (float x, int n) /*@modifies errno@*/ ; -long double ldexpl (long double x, int n) /*@modifies errno@*/ ; -float logf (float x) /*@modifies errno@*/ ; -long double logl (long double x) /*@modifies errno@*/ ; -float log10f (float x) /*@modifies errno@*/; -long double log10l (long double x) /*@modifies errno@*/; -float modff (float x, /*@out@*/ float *xp) /*@modifies *xp@*/ ; -long double modfl (long double x, /*@out@*/ long double *xp) /*@modifies *xp@*/ ; -float powf (float x, float y) /*@modifies errno@*/ ; -long double powl (long double x, long double y) /*@modifies errno@*/ ; -float sinf (float x) /*@*/ ; -long double sinl (long double x) /*@*/ ; -float sinhf (float x) /*@*/ ; -long double sinhl (long double x) /*@*/ ; -float sqrtf (float x) /*@modifies errno@*/ ; -long double sqrtl (long double x) /*@modifies errno@*/ ; -float tanf (float x) /*@*/ ; -long double tanl (long double x) /*@*/ ; -float tanhf (float x) /*@*/ ; -long double tanhl (long double x) /*@*/ ; - -# endif - -/* -** setjmp.h -*/ - -typedef /*@abstract@*/ /*@mutable@*/ void *jmp_buf; - -int setjmp (/*@out@*/ jmp_buf env) /*@modifies env;@*/ ; -/*@mayexit@*/ void longjmp (jmp_buf env, int val) /*@*/ ; - -/* -** signal.h -*/ - -/*@constant int SIGABRT; @*/ -/*@constant int SIGFPE; @*/ -/*@constant int SIGILL; @*/ -/*@constant int SIGINT; @*/ -/*@constant int SIGSEGV; @*/ -/*@constant int SIGTERM; @*/ - -typedef /*@integraltype@*/ sig_atomic_t; - -/*@constant void (*SIG_DFL)(int); @*/ -/*@constant void (*SIG_ERR)(int); @*/ -/*@constant void (*SIG_IGN)(int); @*/ - -typedef void (*sighandler_t) (int); - -/* -** signal takes an int and a sighandler_t, and returns a sighandler_t -** (possibly NULL). -*/ - -/*@null@*/ sighandler_t signal (int sig, /*@null@*/ sighandler_t func) - /*@modifies internalState, errno;@*/ ; - -/*@mayexit@*/ int raise (int sig) ; - -/* -** stdarg.h -*/ - -typedef /*@abstract@*/ /*@mutable@*/ void *va_list; - -void va_start (/*@out@*/ va_list ap, ...) /*@modifies ap;@*/ ; -void va_end (va_list va) /*@modifies va;@*/ ; - -void va_copy (/*@out@*/ va_list dest, va_list src) /*modifies dest;@*/ ; - -/* -** va_arg is builtin -*/ - -/* -** stdio.h -*/ - -typedef /*@abstract@*/ /*@mutable@*/ void *FILE; -typedef /*@abstract@*/ /*@mutable@*/ void *fpos_t; - -/*@constant size_t _IOFBF; @*/ -/*@constant size_t _IOLBF; @*/ -/*@constant size_t _IONBF; @*/ - -/*@constant size_t BUFSIZ; @*/ /* evans 2002-02-27 change suggested by Walter Briscoe */ - -/*@constant int EOF; @*/ - -/*@constant int FOPEN_MAX; @*/ -/*@constant int FILENAME_MAX; @*/ - -/*@constant int L_tmpnam; @*/ - -/*@constant int SEEK_CUR; @*/ -/*@constant int SEEK_END; @*/ -/*@constant int SEEK_SET; @*/ - -/*@constant int TMP_MAX; @*/ - -# ifdef STRICT -/*@checked@*/ FILE *stderr; -/*@checked@*/ FILE *stdin; -/*@checked@*/ FILE *stdout; -# else -/*@unchecked@*/ FILE *stderr; -/*@unchecked@*/ FILE *stdin; -/*@unchecked@*/ FILE *stdout; -# endif - -int remove (char *filename) /*@modifies fileSystem, errno@*/ ; -int rename (char *old, char *new) /*@modifies fileSystem, errno@*/ ; - -/*@dependent@*/ /*@null@*/ FILE *tmpfile (void) - /*@modifies fileSystem, errno@*/ ; - -/*@observer@*/ char * - tmpnam (/*@out@*/ /*@null@*/ /*@returned@*/ char *s) - /*@modifies *s, internalState@*/ ; - -int fclose (FILE *stream) - /*@modifies *stream, errno, fileSystem;@*/ ; - -int fflush (/*@null@*/ FILE *stream) - /*@modifies *stream, errno, fileSystem;@*/ ; - -/*@null@*/ /*@dependent@*/ FILE *fopen (char *filename, char *mode) - /*@modifies fileSystem@*/ ; - -/*@dependent@*/ /*@null@*/ FILE *freopen (char *filename, char *mode, FILE *stream) - /*@modifies *stream, fileSystem, errno@*/ ; - -void setbuf (FILE *stream, /*@null@*/ /*@exposed@*/ /*@out@*/ char *buf) - /*@modifies fileSystem, *stream, *buf@*/ - /*:errorcode != 0*/ ; - /*:requires maxSet(buf) >= (BUFSIZ - 1):*/ ; - -int setvbuf (FILE *stream, /*@null@*/ /*@exposed@*/ /*@out@*/ char *buf, - int mode, size_t size) - /*@modifies fileSystem, *stream, *buf@*/ - /*@requires maxSet(buf) >= (size - 1) @*/ ; - -# ifdef STRICT -/*@printflike@*/ -int fprintf (FILE *stream, char *format, ...) - /*@modifies fileSystem, *stream@*/ ; -# else -/*@printflike@*/ -int /*@alt void@*/ fprintf (FILE *stream, char *format, ...) - /*@modifies fileSystem, *stream@*/ ; -# endif - -/*@scanflike@*/ -int fscanf (FILE *stream, char *format, ...) - /*@modifies fileSystem, *stream, errno@*/ ; - -# ifdef STRICT -/*@printflike@*/ -int printf (char *format, ...) - /*@globals stdout@*/ - /*@modifies fileSystem, *stdout@*/ ; -# else -/*@printflike@*/ -int /*@alt void@*/ printf (char *format, ...) - /*@globals stdout@*/ - /*@modifies fileSystem, *stdout@*/ ; -# endif - -/*@scanflike@*/ -int scanf(char *format, ...) - /*@globals stdin@*/ - /*@modifies fileSystem, *stdin, errno@*/ ; - /*drl added errno 09-19-2001 */ ; - -# ifdef STRICT -/*@printflike@*/ -int sprintf (/*@out@*/ char *s, char *format, ...) - /*@warn bufferoverflowhigh "Buffer overflow possible with sprintf. Recommend using snprintf instead"@*/ - /*@modifies *s@*/ ; -# else -/*@printflike@*/ -int /*@alt void@*/ sprintf (/*@out@*/ char *s, char *format, ...) - /*@warn bufferoverflowhigh "Buffer overflow possible with sprintf. Recommend using snprintf instead"@*/ - /*@modifies *s@*/ ; -# endif - -/* evans 2002-07-09: snprintf added to standard.h (from unix.h) */ -/*@printflike@*/ -int snprintf (/*@out@*/ char * restrict s, size_t n, const char * restrict format, ...) - /*@modifies s@*/ - /*@requires maxSet(s) >= (n - 1)@*/ ; - -/*@scanflike@*/ -int sscanf (/*@out@*/ char *s, char *format, ...) /*@modifies errno@*/ ; - /* modifies extra arguments */ - -int vprintf (const char *format, va_list arg) - /*@globals stdout@*/ - /*@modifies fileSystem, *stdout@*/ ; - -int vfprintf (FILE *stream, char *format, va_list arg) - /*@modifies fileSystem, *stream, arg, errno@*/ ; - -int vsprintf (/*@out@*/ char *str, const char *format, va_list ap) - /*@warn bufferoverflowhigh "Use vsnprintf instead"@*/ - /*@modifies str@*/ ; - -int vsnprintf (/*@out@*/ char *str, size_t size, const char *format, va_list ap) - /*@requires maxSet(str) >= (size - 1)@*/ /* drl - this was size, size-1 in stdio.h */ - /*@modifies str@*/ ; - -int fgetc (FILE *stream) - /*@modifies fileSystem, *stream, errno@*/ ; - -/*@null@*/ char * - fgets (/*@returned@*/ /*@out@*/ char *s, int n, FILE *stream) - /*@modifies fileSystem, *s, *stream, errno@*/ - /*@requires maxSet(s) >= (n -1); @*/ - /*@ensures maxRead(s) <= (n -1) /\ maxRead(s) >= 0; @*/ - ; - -int fputc (int /*@alt char@*/ c, FILE *stream) - /*:errorcode EOF:*/ - /*@modifies fileSystem, *stream, errno@*/ ; - -int fputs (char *s, FILE *stream) - /*@modifies fileSystem, *stream@*/ ; - -/* note use of sef --- stream may be evaluated more than once */ -int getc (/*@sef@*/ FILE *stream) - /*@modifies fileSystem, *stream, errno@*/ ; - -int getchar (void) /*@globals stdin@*/ /*@modifies fileSystem, *stdin, errno@*/ ; - -/*@null@*/ char *gets (/*@out@*/ char *s) - /*@warn bufferoverflowhigh - "Use of gets leads to a buffer overflow vulnerability. Use fgets instead"@*/ - /*@globals stdin@*/ /*@modifies fileSystem, *s, *stdin, errno@*/ ; - -int putc (int /*@alt char@*/ c, /*@sef@*/ FILE *stream) - /*:errorcode EOF:*/ - /*@modifies fileSystem, *stream, errno;@*/ ; - -int putchar (int /*@alt char@*/ c) - /*:errorcode EOF:*/ - /*@globals stdout@*/ - /*@modifies fileSystem, *stdout, errno@*/ ; - -int puts (const char *s) - /*:errorcode EOF:*/ - /*@globals stdout@*/ - /*@modifies fileSystem, *stdout, errno@*/ ; - -int ungetc (int /*@alt char@*/ c, FILE *stream) - /*@modifies fileSystem, *stream@*/ ; - /*drl REMOVED errno 09-19-2001*/ - -size_t - fread (/*@out@*/ void *ptr, size_t size, size_t nobj, FILE *stream) - /*@modifies fileSystem, *ptr, *stream, errno@*/ - /*requires maxSet(ptr) >= (size - 1) @*/ - /*@ensures maxRead(ptr) == (size - 1) @*/ ; - -size_t fwrite (void *ptr, size_t size, size_t nobj, FILE *stream) - /*@modifies fileSystem, *stream, errno@*/ - /*@requires maxRead(ptr) >= size @*/ ; - -int fgetpos (FILE *stream, /*@out@*/ fpos_t *pos) - /*@modifies *pos, errno@*/ - /*@requires maxSet(pos) >= 0@*/ - /*@ensures maxRead(pos) >= 0 @*/; - -int fseek (FILE *stream, long int offset, int whence) - /*:errorcode -1:*/ - /*@modifies fileSystem, *stream, errno@*/ ; - -int fsetpos (FILE *stream, fpos_t *pos) - /*@modifies fileSystem, *stream, errno@*/ ; - -long int ftell(FILE *stream) - /*:errorcode -1:*/ /*@modifies errno*/ ; - -void rewind (FILE *stream) /*@modifies *stream@*/ ; -void clearerr (FILE *stream) /*@modifies *stream@*/ ; - -int feof (FILE *stream) /*@modifies errno@*/ ; - -int ferror (FILE *stream) /*@modifies errno@*/ ; - -void perror (/*@null@*/ char *s) - /*@globals errno, stderr@*/ /*@modifies fileSystem, *stderr@*/ ; - -/* -** stdlib.h -*/ - -double atof (char *s) /*@*/ ; -int atoi (char *s) /*@*/ ; -long int atol (char *s) /*@*/ ; - -double strtod (char *s, /*@null@*/ /*@out@*/ char **endp) - /*@modifies *endp, errno@*/ ; - -long strtol (char *s, /*@null@*/ /*@out@*/ char **endp, int base) - /*@modifies *endp, errno@*/ ; - -unsigned long - strtoul (char *s, /*@null@*/ /*@out@*/ char **endp, int base) - /*@modifies *endp, errno@*/ ; - -/*@constant int RAND_MAX; @*/ -int rand (void) /*@modifies internalState@*/ ; -void srand (unsigned int seed) /*@modifies internalState@*/ ; - -/* - drl - changed 12/29/2000 -*/ - -/*@null@*/ /*@out@*/ /*@only@*/ void *calloc (size_t nobj, size_t size) /*@*/ - /*@ensures maxSet(result) == (nobj - 1); @*/ ; -/*@null@*/ /*@out@*/ /*@only@*/ void *malloc (size_t size) /*@*/ - /*@ensures maxSet(result) == (size - 1); @*/ ; - -/*end drl changed */ - -/* 11 June 1997: removed out on return value */ - -# if 0 -/*@null@*/ /*@only@*/ void * - realloc (/*@null@*/ /*@only@*/ /*@special@*/ void *p, - size_t size) /*@releases p@*/ /*@modifies *p@*/ - /*@ensures maxSet(result) == (size - 1) @*/; -# endif - -/* -** LCLint annotations cannot fully describe realloc. The semantics we -** want are: -** realloc returns null: ownership of parameter is not changed -** realloc returns non-null: ownership of parameter is transferred to return value -** -** Otherwise, storage is in the same state before and after the call. -*/ - -/*@null@*/ /*@only@*/ void * - realloc (/*@null@*/ /*@only@*/ /*@out@*/ /*@returned@*/ void *p, size_t size) - /*@modifies *p@*/ /*@ensures maxSet(result) >= (size - 1) @*/; - -void free (/*@null@*/ /*@out@*/ /*@only@*/ void *p) /*@modifies p@*/ ; - -/*@constant int EXIT_FAILURE; @*/ -/*@constant int EXIT_SUCCESS; @*/ - -/*@exits@*/ void abort (void) /*@*/ ; -/*@exits@*/ void exit (int status) /*@*/ ; -int atexit (void (*func)(void)) /*@modifies internalState@*/ ; - -/*@observer@*/ /*@null@*/ char *getenv (char *name) /*@*/ ; - -int system (/*@null@*/ char *s) /*@modifies fileSystem@*/ ; - -/*@null@*/ /*@dependent@*/ void * - bsearch (void *key, void *base, - size_t n, size_t size, - int (*compar)(void *, void *)) /*@*/ ; - -void qsort (void *base, size_t n, size_t size, - int (*compar)(void *, void *)) - /*@modifies *base, errno@*/ ; - -int abs (int n) /*@*/ ; - -typedef /*@concrete@*/ struct -{ - int quot; - int rem; -} div_t ; - -div_t div (int num, int denom) /*@*/ ; - -long int labs (long int n) /*@*/ ; - -typedef /*@concrete@*/ struct -{ - long int quot; - long int rem; -} ldiv_t ; - -ldiv_t ldiv (long num, long denom) /*@*/ ; - -/*@constant size_t MB_CUR_MAX; @*/ - -/* -** wchar_t and wint_t functions added by Amendment 1 to ISO. -*/ - -/*@constant int WCHAR_MAX@*/ -/*@constant int WCHAR_MIN@*/ -/*@constant wint_t WEOF@*/ - -wint_t btowc (int c) /*@*/ ; - -wint_t fgetwc (FILE *fp) /*@modifies fileSystem, *fp*/ ; - -/*@null@*/ wchar_t *fgetws (/*@returned@*/ wchar_t *s, int n, FILE *stream) - /*@modifies fileSystem, *s, *stream@*/; - -wint_t fputwc (wchar_t c, FILE *stream) - /*@modifies fileSystem, *stream@*/; - -int fputws (const wchar_t *s, FILE *stream) - /*@modifies fileSystem, *stream@*/ ; - -int fwide (FILE *stream, int mode) /*@*/ ; - /* does not modify the stream */ - -/*@printflike@*/ int fwprintf (FILE *stream, const wchar_t *format, ...) - /*@modifies *stream, fileSystem@*/ ; - -/*@scanflike@*/ int fwscanf (FILE *stream, const wchar_t *format, ...) - /*@modifies *stream, fileSystem@*/ ; - -/* note use of sef --- stream may be evaluated more than once */ -wint_t getwc (/*@sef@*/ FILE *stream) /*@modifies fileSystem, *stream@*/ ; - -wint_t getwchar (void) /*@modifies fileSystem, *stdin@*/; - -size_t mbrlen (const char *s, size_t n, /*@null@*/ mbstate_t *ps) /*@*/ ; - -size_t mbrtowc (/*@null@*/ wchar_t *pwc, const char *s, size_t n, - /*@null@*/ mbstate_t *ps) - /*@modifies *pwc@*/ ; - -int mbsinit (/*@null@*/ const mbstate_t *ps) /*@*/ ; - -size_t mbsrtowcs (/*@null@*/ wchar_t *dst, const char **src, size_t len, - /*@null@*/ mbstate_t *ps) - /*@modifies *dst@*/ ; - -/* note use of sef --- stream may be evaluated more than once */ -wint_t putwc (wchar_t c, /*@sef@*/ FILE *stream) /*@modifies fileSystem, *stream@*/ ; - -wint_t putwchar (wchar_t c) /*@modifies fileSystem, *stdout@*/ ; - -/*@printflike@*/ int swprintf (wchar_t *s, size_t n, const wchar_t *format, ...) - /*@modifies *s@*/ ; - -/*@scanflike@*/ int swscanf (const wchar_t *s, const wchar_t *format, ...) - /*@modifies *stdin@*/ ; - -wint_t ungetwc (wint_t c, FILE *stream) /*@modifies fileSystem, *stream@*/ ; - -int vfwprintf (FILE *stream, const wchar_t *format, va_list arg) - /*@modifies fileSystem, *stream@*/ ; - -int vswprintf (wchar_t *s, size_t n, const wchar_t *format, va_list arg) - /*@modifies *s@*/ ; - -int vwprintf (const wchar_t *format, va_list arg) - /*@modifies fileSystem, *stdout@*/ ; - -size_t wcrtomb (/*@null@*/ /*@out@*/ char *s, wchar_t wc, /*@null@*/ mbstate_t *ps) - /*@modifies *s@*/; - -void /*@alt wchar_t *@*/ - wcscat (/*@unique@*/ /*@returned@*/ /*@out@*/ wchar_t *s1, const wchar_t *s2) - /*@modifies *s1@*/ ; - -/*@exposed@*/ /*@null@*/ wchar_t * - wcschr (/*@returned@*/ const wchar_t *s, wchar_t c) - /*@*/ ; - -int wcscmp (const wchar_t *s1, const wchar_t *s2) /*@*/ ; - -int wcscoll (const wchar_t *s1, const wchar_t *s2) /*@*/ ; - -void /*@alt wchar_t *@*/ - wcscpy (/*@unique@*/ /*@out@*/ /*@returned@*/ wchar_t *s1, const wchar_t *s2) - /*@modifies *s1@*/ ; - -size_t wcscspn (const wchar_t *s1, const wchar_t *s2) /*@*/ ; - -size_t wcsftime (/*@out@*/ wchar_t *s, size_t maxsize, const wchar_t *format, - const struct tm *timeptr) - /*@modifies *s@*/ ; - -size_t wcslen (const wchar_t *s) /*@*/ ; - -void /*@alt wchar_t *@*/ - wcsncat (/*@unique@*/ /*@returned@*/ /*@out@*/ wchar_t *s1, const wchar_t *s2, - size_t n) - /*@modifies *s1@*/ ; - -int wcsncmp (const wchar_t *s1, const wchar_t *s2, size_t n) /*@*/ ; - -void /*@alt wchar_t *@*/ - wcsncpy (/*@unique@*/ /*@returned@*/ /*@out@*/ wchar_t *s1, const wchar_t *s2, - size_t n) - /*@modifies *s1@*/ ; - -/*@null@*/ wchar_t * - wcspbrk (/*@returned@*/ const wchar_t *s1, const wchar_t *s2) - /*@*/ ; - -/*@null@*/ wchar_t * - wcsrchr (/*@returned@*/ const wchar_t *s, wchar_t c) - /*@*/ ; - -size_t - wcsrtombs (/*@null@*/ char *dst, const wchar_t **src, size_t len, - /*@null@*/ mbstate_t *ps) - /*@modifies *src@*/ ; - -size_t wcsspn (const wchar_t *s1, const wchar_t *s2) /*@*/ ; - -/*@null@*/ wchar_t *wcsstr (const wchar_t *s1, const wchar_t *s2) /*@*/ ; - -double wcstod (const wchar_t *nptr, /*@null@*/ wchar_t **endptr) - /*@modifies *endptr@*/ ; - -/*@null@*/ wchar_t * - wcstok (/*@null@*/ wchar_t *s1, const wchar_t *s2, wchar_t **ptr) - /*@modifies *ptr@*/; - -long wcstol (const wchar_t *nptr, /*@null@*/ wchar_t **endptr, int base) - /*@modifies *endptr@*/; - -unsigned long - wcstoul (const wchar_t *nptr, /*@null@*/ wchar_t **endptr, int base) - /*@modifies *endptr@*/; - -size_t - wcsxfrm (/*@null@*/ wchar_t *s1, const wchar_t *s2, size_t n) - /*@modifies *s1@*/; - -int wctob (wint_t c) /*@*/; - -/*@null@*/ wchar_t *wmemchr (const wchar_t *s, wchar_t c, size_t n) /*@*/ ; - -int wmemcmp (const wchar_t *s1, const wchar_t *s2, size_t n) /*@*/ ; - -wchar_t *wmemcpy (/*@returned@*/ wchar_t *s1, const wchar_t *s2, size_t n) - /*@modifies *s1@*/; - -wchar_t *wmemmove (/*@returned@*/ wchar_t *s1, const wchar_t *s2, size_t n) - /*@modifies *s1@*/; - -wchar_t *wmemset (/*@returned@*/ wchar_t *s, wchar_t c, size_t n) - /*@modifies *s@*/; - -/*@printflike@*/ int wprintf (const wchar_t *format, ...) - /*@globals stdout@*/ /*@modifies errno, *stdout@*/; - -/*@scanflike@*/ int - wscanf (const wchar_t *format, ...) - /*@globals stdin@*/ /*@modifies errno, *stdin@*/; - -/* -** wctype.h (added by Amendment 1) -*/ - -/* Warning: not sure about these (maybe abstract?): */ -typedef /*@integraltype@*/ wctype_t; -typedef /*@integraltype@*/ wctrans_t; - -# ifdef STRICT -_Bool iswalnum (wint_t c) /*@*/ ; -_Bool iswalpha (wint_t c) /*@*/ ; -_Bool iswcntrl (wint_t c) /*@*/ ; -_Bool iswctype (wint_t c, wctype_t ctg) /*@*/ ; -_Bool iswdigit (wint_t c) /*@*/ ; -_Bool iswgraph (wint_t c) /*@*/ ; -_Bool iswlower (wint_t c) /*@*/ ; -_Bool iswprint (wint_t c) /*@*/ ; -_Bool iswpunct (wint_t c) /*@*/ ; -_Bool iswspace (wint_t c) /*@*/ ; -_Bool iswupper (wint_t c) /*@*/ ; -_Bool iswxdigit (wint_t c) /*@*/ ; - -wint_t towctrans (wint_t c, wctrans_t ctg) /*@*/ ; -wint_t towlower (wint_t c) /*@*/ ; -wint_t towupper (wint_t c) /*@*/ ; -# else -_Bool /*@alt int@*/ iswalnum (wint_t c) /*@*/ ; -_Bool /*@alt int@*/ iswalpha (wint_t c) /*@*/ ; -_Bool /*@alt int@*/ iswcntrl (wint_t c) /*@*/ ; -_Bool /*@alt int@*/ iswctype (wint_t c, wctype_t ctg) /*@*/ ; -_Bool /*@alt int@*/ iswdigit (wint_t c) /*@*/ ; -_Bool /*@alt int@*/ iswgraph (wint_t c) /*@*/ ; -_Bool /*@alt int@*/ iswlower (wint_t c) /*@*/ ; -_Bool /*@alt int@*/ iswprint (wint_t c) /*@*/ ; -_Bool /*@alt int@*/ iswpunct (wint_t c) /*@*/ ; -_Bool /*@alt int@*/ iswspace (wint_t c) /*@*/ ; -_Bool /*@alt int@*/ iswupper (wint_t c) /*@*/ ; -_Bool /*@alt int@*/ iswxdigit (wint_t c) /*@*/ ; - -wint_t /*@alt int@*/ towctrans (wint_t c, wctrans_t ctg) /*@*/ ; -wint_t /*@alt int@*/ towlower (wint_t c) /*@*/ ; -wint_t /*@alt int@*/ towupper (wint_t c) /*@*/ ; -# endif - -wctrans_t wctrans (const char *property) /*@*/ ; -wctype_t wctype (const char *property) /*@*/ ; - -int mblen (char *s, size_t n) /*@*/ ; -int mbtowc (/*@null@*/ wchar_t *pwc, /*@null@*/ char *s, size_t n) - /*@modifies *pwc@*/ ; -int wctomb (/*@out@*/ /*@null@*/ char *s, wchar_t wchar) - /*@modifies *s@*/ ; -size_t mbstowcs (/*@out@*/ wchar_t *pwcs, char *s, size_t n) - /*@modifies *pwcs@*/ ; -size_t wcstombs (/*@out@*/ char *s, wchar_t *pwcs, size_t n) - /*@modifies *s@*/ ; - -/* -** string.h -*/ - -void /*@alt void * @*/ - memcpy (/*@unique@*/ /*@returned@*/ /*@out@*/ void *s1, void *s2, size_t n) - /*@modifies *s1@*/ - /*@requires maxRead(s2) >= (n - 1) /\ maxSet(s1) >= (n - 1); @*/ - ; - -void /*@alt void * @*/ - memmove (/*@returned@*/ /*@out@*/ void *s1, void *s2, size_t n) - /*@modifies *s1@*/ - /*@requires maxRead(s2) >= (n - 1) /\ maxSet(s1) >= (n - 1); @*/ - ; - - - /* drl - modifed 12/29/2000 - */ - -void /*@alt char * @*/ - strcpy (/*@unique@*/ /*@out@*/ /*@returned@*/ char *s1, char *s2) - /*@modifies *s1@*/ - /*@requires maxSet(s1) >= maxRead(s2) @*/ - /*@ensures maxRead(s1) == maxRead (s2) /\ maxRead(result) == maxRead(s2) /\ maxSet(result) == maxSet(s1); @*/; - -void /*@alt char * @*/ - strncpy (/*@unique@*/ /*@out@*/ /*@returned@*/ char *s1, char *s2, size_t n) - /*@modifies *s1@*/ - /*@requires maxSet(s1) >= ( n - 1 ); @*/ - /*@ensures maxRead (s2) >= maxRead(s1) /\ maxRead (s1) <= n; @*/ ; - -void /*@alt char * @*/ - strcat (/*@unique@*/ /*@returned@*/ char *s1, char *s2) - /*@modifies *s1@*/ /*@requires maxSet(s1) >= (maxRead(s1) + maxRead(s2) );@*/ - /*@ensures maxRead(result) == (maxRead(s1) + maxRead(s2) );@*/; - -void /*@alt char * @*/ - strncat (/*@unique@*/ /*@returned@*/ char *s1, char *s2, size_t n) - /*@modifies *s1@*/ - /*@requires maxSet(s1) >= ( maxRead(s1) + n); @*/ - /*@ensures maxRead(s1) >= (maxRead(s1) + n); @*/; - - /*drl end*/ - -int memcmp (void *s1, void *s2, size_t n) /*@*/ ; -int strcmp (char *s1, char *s2) /*@*/ ; -int strcoll (char *s1, char *s2) /*@*/ ; -int strncmp (char *s1, char *s2, size_t n) /*@*/ ; -size_t strxfrm (/*@out@*/ /*@null@*/ char *s1, char *s2, size_t n) - /*@modifies *s1@*/ ; /* s1 may be null only if n == 0 */ - -/*@null@*/ void *memchr (void *s, int c, size_t n) /*@*/ ; - -# ifdef STRICT -/*@exposed@*/ /*@null@*/ char * -strchr (/*@returned@*/ char *s, char c) /*@*/ /*@ensures maxSet(result) >= 0 /\ maxSet(result) <= maxSet(s) /\ maxRead (result) <= maxRead(s) /\ maxRead(result) >= 0 @*/ ; -# else -/*@exposed@*/ /*@null@*/ char * - strchr (/*@returned@*/ char *s, int /*@alt char@*/ c) /*@*/ /*@ensures maxSet(result) >= 0 /\ maxSet(result) <= maxSet(s) /\ maxRead (result) <= maxRead(s) /\ maxRead(result) >= 0; @*/ ; -# endif - -size_t strcspn (char *s1, char *s2) /*@*/ ; -/*@null@*/ /*@exposed@*/ char * - strpbrk (/*@returned@*/ char *s, char *t) /*@*/ ; - -# ifdef STRICT -/*@null@*/ /*@exposed@*/ char * - strrchr (/*@returned@*/ char *s, char c) /*@*/ /*@ensures maxSet(result) >= 0 /\ maxSet(result) <= maxSet(s) /\ maxRead (result) <= maxRead(s) /\ maxRead(result) >= 0 @*/ ; -# else -/*@null@*/ /*@exposed@*/ char * - strrchr (/*@returned@*/ char *s, int /*@alt char@*/ c) /*@*/ /*@ensures maxSet(result) >= 0 /\ maxSet(result) <= maxSet(s) /\ maxRead (result) <= maxRead(s) /\ maxRead(result) >= 0 @*/ ; -# endif - -size_t strspn (char *s, char *t) /*@*/ ; - -/*@null@*/ /*@exposed@*/ char * - strstr (/*@returned@*/ const char *s, const char *t) /*@*/ - /*@ensures maxSet(result) >= 0 /\ maxSet(result) <= maxSet(s) /\ maxRead (result) <= maxRead(s) /\ maxRead(result) >= 0 /\ maxRead(result) >= maxRead(t) /\ maxSet(result) >= maxRead(t)@*/ ; - -/*@null@*/ /*@exposed@*/ char * - strtok (/*@returned@*/ /*@null@*/ char *s, char *t) - /*@modifies *s, internalState, errno@*/ ; - -void /*@alt void *@*/ memset (/*@out@*/ /*@returned@*/ void *s, - int c, size_t n) - /*@modifies *s@*/ /*@requires maxSet(s) >= (n - 1) @*/ /*@ensures maxRead(s) >= (n - 1) @*/ ; - -/*@observer@*/ char *strerror (int errnum) /*@*/ ; - -/*drl */ -size_t strlen (char *s) /*@*/ /*@ensures result == maxRead(s); @*/; - -/* -** time.h -*/ - -/*@constant int CLOCKS_PER_SEC;@*/ - -typedef /*@integraltype@*/ clock_t; -typedef /*@integraltype@*/ time_t; - -struct tm - { - int tm_sec; - int tm_min; - int tm_hour; - int tm_mday; - int tm_mon; - int tm_year; - int tm_wday; - int tm_yday; - int tm_isdst; - } ; - -clock_t clock (void) /*@modifies internalState@*/ ; -double difftime (time_t time1, time_t time0) /*@*/ ; -time_t mktime (struct tm *timeptr) /*@*/ ; - -time_t time (/*@null@*/ /*@out@*/ time_t *tp) - /*@modifies *tp@*/ ; - -/*@observer@*/ char *asctime (struct tm *timeptr) - /*@modifies errno*/ /*@ensures maxSet(result) == 25 /\ maxRead(result) == 25; @*/ ; - -/*@observer@*/ char *ctime (time_t *tp) /*@*/ - /*@ensures maxSet(result) == 25 /\ maxRead(result) == 25; @*/; - -/* 2003-11-01: remove null annotation: gmtima and localtime cannot return null */ -/*@observer@*/ struct tm *gmtime (time_t *tp) /*@*/ ; - -/*@observer@*/ struct tm *localtime (time_t *tp) - /*@modifies errno@*/ ; - -size_t strftime (/*@out@*/ char *s, size_t smax, - char *fmt, struct tm *timeptr) - /*@modifies *s@*/ ; - -/* -** ISO c99: 7.18 Integer types -*/ - -/* -** These types are OPTIONAL. Provide warnings on use. -*/ - -typedef /*@integraltype@*/ int8_t - /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider int_least8_t instead."@*/ ; - -typedef /*@integraltype@*/ int16_t - /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider int_least16_t instead."@*/ ; - -typedef /*@integraltype@*/ int32_t - /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider int_least32_t instead."@*/ ; - -typedef /*@integraltype@*/ int64_t - /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider int_least64_t instead."@*/ ; - -typedef /*@unsignedintegraltype@*/ uint8_t - /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider uint_least8_t instead."@*/ ; - -typedef /*@unsignedintegraltype@*/ uint16_t - /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider uint_least16_t instead."@*/ ; - -typedef /*@unsignedintegraltype@*/ uint32_t - /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider uint_least32_t instead."@*/ ; - -typedef /*@unsignedintegraltype@*/ uint64_t - /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide. Consider uint_least64_t instead."@*/ ; - -typedef /*@integraltype@*/ int_least8_t; -typedef /*@integraltype@*/ int_least16_t; -typedef /*@integraltype@*/ int_least32_t; -typedef /*@integraltype@*/ int_least64_t; - -typedef /*@unsignedintegraltype@*/ uint_least8_t; -typedef /*@unsignedintegraltype@*/ uint_least16_t; -typedef /*@unsignedintegraltype@*/ uint_least32_t; -typedef /*@unsignedintegraltype@*/ uint_least64_t; - -typedef /*@integraltype@*/ int_fast8_t; -typedef /*@integraltype@*/ int_fast16_t; -typedef /*@integraltype@*/ int_fast32_t; -typedef /*@integraltype@*/ int_fast64_t; - -typedef /*@unsignedintegraltype@*/ uint_fast8_t; -typedef /*@unsignedintegraltype@*/ uint_fast16_t; -typedef /*@unsignedintegraltype@*/ uint_fast32_t; -typedef /*@unsignedintegraltype@*/ uint_fast64_t; - -/* Corrections to intptr_t and uintptr_t decparations provided by David Sanderson */ - -typedef /*@signedintegraltype@*/ intptr_t - /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide."@*/ ; - -typedef /*@unsignedintegraltype@*/ uintptr_t - /*@warn implementationoptional "ISO99 specifies as optional type, implementation need not provide."@*/ ; - -typedef /*@signedintegraltype@*/ intmax_t; -typedef /*@unsignedintegraltype@*/ uintmax_t; - -/* -** What should the types be here? -*/ - -/*@constant int INT8_MIN@*/ -/*@constant int INT16_MIN@*/ -/*@constant int INT32_MIN@*/ -/*@constant int INT64_MIN@*/ - -/*@constant int INT8_MAX@*/ -/*@constant int INT16_MAX@*/ -/*@constant int INT32_MAX@*/ -/*@constant int INT64_MAX@*/ - -/*@constant unsigned int UINT8_MAX@*/ -/*@constant unsigned int UINT16_MAX@*/ -/*@constant unsigned int UINT32_MAX@*/ -/*@constant unsigned int UINT64_MAX@*/ - -/*@constant int INT_LEAST8_MIN@*/ -/*@constant int INT_LEAST16_MIN@*/ -/*@constant int INT_LEAST32_MIN@*/ -/*@constant int INT_LEAST64_MIN@*/ - -/*@constant int INT_LEAST8_MAX@*/ -/*@constant int INT_LEAST16_MAX@*/ -/*@constant int INT_LEAST32_MAX@*/ -/*@constant int INT_LEAST64_MAX@*/ - -/*@constant unsigned int UINT_LEAST8_MAX@*/ -/*@constant unsigned int UINT_LEAST16_MAX@*/ -/*@constant unsigned int UINT_LEAST32_MAX@*/ -/*@constant unsigned int UINT_LEAST64_MAX@*/ - -/*@constant int INT_FAST8_MIN@*/ -/*@constant int INT_FAST16_MIN@*/ -/*@constant int INT_FAST32_MIN@*/ -/*@constant int INT_FAST64_MIN@*/ - -/*@constant int INT_FAST8_MAX@*/ -/*@constant int INT_FAST16_MAX@*/ -/*@constant int INT_FAST32_MAX@*/ -/*@constant int INT_FAST64_MAX@*/ - -/*@constant unsigned int UINT_FAST8_MAX@*/ -/*@constant unsigned int UINT_FAST16_MAX@*/ -/*@constant unsigned int UINT_FAST32_MAX@*/ -/*@constant unsigned int UINT_FAST64_MAX@*/ - -/*@constant size_t INTPTR_MIN@*/ -/*@constant size_t INTPTR_MAX@*/ -- 2.11.4.GIT