[kernel] Parsing tests/libc/fc_libc.c (with preprocessing) /* Generated by Frama-C */ typedef unsigned int size_t; struct __fc_fenv_t { unsigned short __control_word ; unsigned short __unused1 ; unsigned short __status_word ; unsigned short __unused2 ; unsigned short __tags ; unsigned short __unused3 ; unsigned int __eip ; unsigned short __cs_selector ; unsigned int __opcode : 11 ; unsigned int __unused4 : 5 ; unsigned int __data_offset ; unsigned short __data_selector ; unsigned short __unused5 ; }; typedef struct __fc_fenv_t fenv_t; typedef int wchar_t; typedef int ssize_t; typedef unsigned int gid_t; typedef unsigned int uid_t; typedef long off_t; typedef int pid_t; typedef unsigned int useconds_t; struct option { char const *name ; int has_arg ; int *flag ; int val ; }; struct __fc_glob_t { unsigned int gl_pathc ; char **gl_pathv ; unsigned int gl_offs ; int gl_flags ; void (*gl_closedir)(void *) ; void *(*gl_readdir)(void *) ; void *(*gl_opendir)(char const *) ; int (*gl_lstat)(char const * __restrict , void * __restrict ) ; int (*gl_stat)(char const * __restrict , void * __restrict ) ; }; typedef struct __fc_glob_t glob_t; struct __fc_div_t { int quot ; int rem ; }; typedef struct __fc_div_t div_t; struct __fc_ldiv_t { long quot ; long rem ; }; typedef struct __fc_ldiv_t ldiv_t; struct __fc_lldiv_t { long long quot ; long long rem ; }; typedef struct __fc_lldiv_t lldiv_t; typedef unsigned char uint8_t; typedef unsigned short uint16_t; typedef unsigned int uint32_t; typedef unsigned int uintptr_t; typedef long long intmax_t; struct __fc_imaxdiv_t { intmax_t quot ; intmax_t rem ; }; typedef struct __fc_imaxdiv_t imaxdiv_t; 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 ; char int_p_cs_precedes ; char int_p_sep_by_space ; char int_n_cs_precedes ; char int_n_sep_by_space ; char int_p_sign_posn ; char int_n_sign_posn ; }; union __fc_u_finitef { float f ; unsigned short w[2] ; }; union __fc_u_finite { double d ; unsigned short w[4] ; }; struct __fc_pthread_attr_t { int _fc ; }; typedef struct __fc_pthread_attr_t pthread_attr_t; struct __fc_pthread_cond_t { int _fc ; }; typedef struct __fc_pthread_cond_t pthread_cond_t; struct __fc_pthread_condattr_t { int _fc ; }; typedef struct __fc_pthread_condattr_t pthread_condattr_t; struct __fc_pthread_mutex_t { int _fc ; }; typedef struct __fc_pthread_mutex_t pthread_mutex_t; struct __fc_pthread_mutexattr_t { int _fc ; }; typedef struct __fc_pthread_mutexattr_t pthread_mutexattr_t; struct __fc_pthread_t { int _fc ; }; typedef struct __fc_pthread_t pthread_t; typedef unsigned long sigset_t; union sigval { int sival_int ; void *sival_ptr ; }; struct __fc_siginfo_t { int si_signo ; int si_code ; union sigval si_value ; int si_errno ; pid_t si_pid ; uid_t si_uid ; void *si_addr ; int si_status ; int si_band ; }; typedef struct __fc_siginfo_t siginfo_t; struct sigaction { void (*sa_handler)(int ) ; void (*sa_sigaction)(int , siginfo_t *, void *) ; sigset_t sa_mask ; int sa_flags ; }; typedef unsigned int socklen_t; typedef unsigned short sa_family_t; struct sockaddr { sa_family_t sa_family ; char sa_data[14] ; }; struct iovec { void *iov_base ; size_t iov_len ; }; struct msghdr { void *msg_name ; socklen_t msg_namelen ; struct iovec *msg_iov ; int msg_iovlen ; void *msg_control ; socklen_t msg_controllen ; int msg_flags ; }; struct __fc_sockfds_type { int x ; }; typedef uint32_t in_addr_t; struct in_addr { in_addr_t s_addr ; }; struct in6_addr { uint8_t s6_addr[16] ; }; enum __fc_ipproto { IPPROTO_IP = 0, IPPROTO_HOPOPTS = 0, IPPROTO_ICMP = 1, IPPROTO_IGMP = 2, IPPROTO_IPIP = 4, IPPROTO_TCP = 6, IPPROTO_EGP = 8, IPPROTO_PUP = 12, IPPROTO_UDP = 17, IPPROTO_IDP = 22, IPPROTO_TP = 29, IPPROTO_DCCP = 33, IPPROTO_IPV6 = 41, IPPROTO_ROUTING = 43, IPPROTO_FRAGMENT = 44, IPPROTO_RSVP = 46, IPPROTO_GRE = 47, IPPROTO_ESP = 50, IPPROTO_AH = 51, IPPROTO_ICMPV6 = 58, IPPROTO_NONE = 59, IPPROTO_DSTOPTS = 60, IPPROTO_MTP = 92, IPPROTO_ENCAP = 98, IPPROTO_PIM = 103, IPPROTO_COMP = 108, IPPROTO_SCTP = 132, IPPROTO_UDPLITE = 136, IPPROTO_RAW = 255, IPPROTO_MAX = 256 }; struct hostent { char *h_name ; char **h_aliases ; int h_addrtype ; int h_length ; char **h_addr_list ; }; struct addrinfo { int ai_flags ; int ai_family ; int ai_socktype ; int ai_protocol ; socklen_t ai_addrlen ; struct sockaddr *ai_addr ; char *ai_canonname ; struct addrinfo *ai_next ; }; struct __fc_gethostbyname { struct hostent host ; unsigned char host_addr[sizeof(struct in_addr)] ; char *h_addr_ptrs[2 + 1] ; char *host_aliases[2] ; char hostbuf[128] ; }; typedef void * const * va_list; typedef unsigned int ino_t; typedef long time_t; typedef unsigned int blkcnt_t; typedef unsigned int blksize_t; typedef unsigned int dev_t; typedef unsigned int mode_t; typedef unsigned int nlink_t; struct stat { dev_t st_dev ; ino_t st_ino ; mode_t st_mode ; nlink_t st_nlink ; uid_t st_uid ; gid_t st_gid ; dev_t st_rdev ; off_t st_size ; time_t st_atime ; time_t st_mtime ; time_t st_ctime ; blksize_t st_blksize ; blkcnt_t st_blocks ; }; struct __fc_pos_t { unsigned long __fc_stdio_position ; }; typedef struct __fc_pos_t fpos_t; struct __fc_FILE { unsigned int __fc_FILE_id ; unsigned int __fc_FILE_data ; }; typedef struct __fc_FILE FILE; typedef unsigned int id_t; typedef int suseconds_t; typedef int clockid_t; typedef unsigned int clock_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 ; }; struct timespec { long tv_sec ; long tv_nsec ; }; struct dirent { ino_t d_ino ; off_t d_off ; unsigned short d_reclen ; unsigned char d_type ; char d_name[256] ; }; struct DIR { unsigned int __fc_dir_id ; unsigned int __fc_dir_position ; struct stat *__fc_dir_inode ; struct dirent **__fc_dir_entries ; }; typedef struct DIR DIR; struct __fc_fd_set { long __fc_fd_set[(unsigned int)1024 / ((unsigned int)8 * sizeof(long))] ; }; typedef struct __fc_fd_set fd_set; struct flock { short l_type ; short l_whence ; off_t l_start ; off_t l_len ; pid_t l_pid ; }; struct timeval { time_t tv_sec ; suseconds_t tv_usec ; }; struct timezone { int tz_minuteswest ; int tz_dsttime ; }; struct itimerval { struct timeval it_interval ; struct timeval it_value ; }; typedef void * iconv_t; struct pollfd { int fd ; short events ; short revents ; }; typedef unsigned long nfds_t; 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 ; }; typedef int ( jmp_buf)[5]; struct __fc_sigjmp_buf { jmp_buf buf ; sigset_t sigs ; }; typedef struct __fc_sigjmp_buf sigjmp_buf; struct __fc_code { char const *c_name ; int c_val ; }; typedef struct __fc_code CODE; typedef unsigned long rlim_t; struct rlimit { rlim_t rlim_cur ; rlim_t rlim_max ; }; struct rusage { struct timeval ru_utime ; struct timeval ru_stime ; }; struct tms { clock_t tms_utime ; clock_t tms_stime ; clock_t tms_cutime ; clock_t tms_cstime ; }; typedef unsigned int tcflag_t; typedef unsigned char cc_t; struct termios { tcflag_t c_iflag ; tcflag_t c_oflag ; tcflag_t c_cflag ; tcflag_t c_lflag ; cc_t c_cc[32] ; }; int volatile Frama_C_entropy_source __attribute__((__unused__, __FRAMA_C_MODEL__)); void Frama_C_make_unknown(char *p, size_t l); int Frama_C_nondet(int a, int b); void *Frama_C_nondet_ptr(void *a, void *b); int Frama_C_interval(int min, int max); /*@ requires order: min ≤ max; ensures result_bounded: \old(min) ≤ \result ≤ \old(max); assigns \result, Frama_C_entropy_source; assigns \result \from min, max, Frama_C_entropy_source; assigns Frama_C_entropy_source \from Frama_C_entropy_source; */ extern int Frama_C_interval_split(int min, int max); /*@ requires order: min ≤ max; ensures result_bounded: \old(min) ≤ \result ≤ \old(max); assigns \result, Frama_C_entropy_source; assigns \result \from min, max, Frama_C_entropy_source; assigns Frama_C_entropy_source \from Frama_C_entropy_source; */ extern unsigned char Frama_C_unsigned_char_interval(unsigned char min, unsigned char max); char Frama_C_char_interval(char min, char max); /*@ requires order: min ≤ max; ensures result_bounded: \old(min) ≤ \result ≤ \old(max); assigns \result, Frama_C_entropy_source; assigns \result \from min, max, Frama_C_entropy_source; assigns Frama_C_entropy_source \from Frama_C_entropy_source; */ extern unsigned short Frama_C_unsigned_short_interval(unsigned short min, unsigned short max); /*@ requires order: min ≤ max; ensures result_bounded: \old(min) ≤ \result ≤ \old(max); assigns \result, Frama_C_entropy_source; assigns \result \from min, max, Frama_C_entropy_source; assigns Frama_C_entropy_source \from Frama_C_entropy_source; */ extern short Frama_C_short_interval(short min, short max); /*@ requires order: min ≤ max; ensures result_bounded: \old(min) ≤ \result ≤ \old(max); assigns \result, Frama_C_entropy_source; assigns \result \from min, max, Frama_C_entropy_source; assigns Frama_C_entropy_source \from Frama_C_entropy_source; */ extern unsigned int Frama_C_unsigned_int_interval(unsigned int min, unsigned int max); /*@ requires order: min ≤ max; ensures result_bounded: \old(min) ≤ \result ≤ \old(max); assigns \result, Frama_C_entropy_source; assigns \result \from min, max, Frama_C_entropy_source; assigns Frama_C_entropy_source \from Frama_C_entropy_source; */ extern int Frama_C_int_interval(int min, int max); /*@ requires order: min ≤ max; ensures result_bounded: \old(min) ≤ \result ≤ \old(max); assigns \result, Frama_C_entropy_source; assigns \result \from min, max, Frama_C_entropy_source; assigns Frama_C_entropy_source \from Frama_C_entropy_source; */ extern unsigned long Frama_C_unsigned_long_interval(unsigned long min, unsigned long max); /*@ requires order: min ≤ max; ensures result_bounded: \old(min) ≤ \result ≤ \old(max); assigns \result, Frama_C_entropy_source; assigns \result \from min, max, Frama_C_entropy_source; assigns Frama_C_entropy_source \from Frama_C_entropy_source; */ extern long Frama_C_long_interval(long min, long max); /*@ requires order: min ≤ max; ensures result_bounded: \old(min) ≤ \result ≤ \old(max); assigns \result, Frama_C_entropy_source; assigns \result \from min, max, Frama_C_entropy_source; assigns Frama_C_entropy_source \from Frama_C_entropy_source; */ extern unsigned long long Frama_C_unsigned_long_long_interval(unsigned long long min, unsigned long long max); /*@ requires order: min ≤ max; ensures result_bounded: \old(min) ≤ \result ≤ \old(max); assigns \result, Frama_C_entropy_source; assigns \result \from min, max, Frama_C_entropy_source; assigns Frama_C_entropy_source \from Frama_C_entropy_source; */ extern long long Frama_C_long_long_interval(long long min, long long max); /*@ requires order: min ≤ max; ensures result_bounded: \old(min) ≤ \result ≤ \old(max); assigns \result, Frama_C_entropy_source; assigns \result \from min, max, Frama_C_entropy_source; assigns Frama_C_entropy_source \from Frama_C_entropy_source; */ extern size_t Frama_C_size_t_interval(size_t min, size_t max); float Frama_C_float_interval(float min, float max); double Frama_C_double_interval(double min, double max); /*@ requires finite: \is_finite(min) ∧ \is_finite(max); requires order: min ≤ max; ensures result_bounded: \is_finite(\result) ∧ \old(min) ≤ \result ≤ \old(max); assigns \result, Frama_C_entropy_source; assigns \result \from min, max, Frama_C_entropy_source; assigns Frama_C_entropy_source \from Frama_C_entropy_source; */ extern double Frama_C_real_interval_as_double(double min, double max); __attribute__((__noreturn__)) void Frama_C_abort(void); /*@ assigns \result; assigns \result \from p; */ extern size_t Frama_C_offset(void const *p); /*@ assigns \result; assigns \result \from i; */ extern long long Frama_C_abstract_cardinal(long long i); /*@ assigns \result; assigns \result \from i; */ extern long long Frama_C_abstract_max(long long i); /*@ assigns \result; assigns \result \from i; */ extern long long Frama_C_abstract_min(long long i); /*@ assigns Frama_C_entropy_source; assigns Frama_C_entropy_source \from Frama_C_entropy_source; */ void Frama_C_update_entropy(void) { Frama_C_entropy_source = Frama_C_entropy_source; return; } /*@ requires valid_p: \valid(p + (0 .. l - 1)); ensures initialization: \initialized(\old(p) + (0 .. \old(l) - 1)); assigns *(p + (0 .. l - 1)), Frama_C_entropy_source; assigns *(p + (0 .. l - 1)) \from Frama_C_entropy_source; assigns Frama_C_entropy_source \from Frama_C_entropy_source; */ void Frama_C_make_unknown(char *p, size_t l) { Frama_C_update_entropy(); { size_t i = (unsigned int)0; while (i < l) { *(p + i) = (char)Frama_C_entropy_source; i += (size_t)1; } } return; } /*@ ensures result_a_or_b: \result ≡ \old(a) ∨ \result ≡ \old(b); assigns \result, Frama_C_entropy_source; assigns \result \from a, b, Frama_C_entropy_source; assigns Frama_C_entropy_source \from Frama_C_entropy_source; */ int Frama_C_nondet(int a, int b) { int tmp; Frama_C_update_entropy(); if (Frama_C_entropy_source) tmp = a; else tmp = b; return tmp; } /*@ ensures result_a_or_b: \result ≡ \old(a) ∨ \result ≡ \old(b); assigns \result, Frama_C_entropy_source; assigns \result \from a, b, Frama_C_entropy_source; assigns Frama_C_entropy_source \from Frama_C_entropy_source; */ void *Frama_C_nondet_ptr(void *a, void *b) { void *tmp; Frama_C_update_entropy(); if (Frama_C_entropy_source) tmp = a; else tmp = b; return tmp; } /*@ requires order: min ≤ max; ensures result_bounded: \old(min) ≤ \result ≤ \old(max); assigns \result, Frama_C_entropy_source; assigns \result \from min, max, Frama_C_entropy_source; assigns Frama_C_entropy_source \from Frama_C_entropy_source; */ int Frama_C_interval(int min, int max) { int r; int aux; Frama_C_update_entropy(); aux = Frama_C_entropy_source; if (aux >= min) if (aux <= max) r = aux; else r = min; else r = min; return r; } /*@ requires order: min ≤ max; ensures result_bounded: \old(min) ≤ \result ≤ \old(max); assigns \result, Frama_C_entropy_source; assigns \result \from min, max, Frama_C_entropy_source; assigns Frama_C_entropy_source \from Frama_C_entropy_source; */ char Frama_C_char_interval(char min, char max) { char __retres; int r; char aux; Frama_C_update_entropy(); aux = (char)Frama_C_entropy_source; if ((int)aux >= (int)min) if ((int)aux <= (int)max) r = (int)aux; else r = (int)min; else r = (int)min; __retres = (char)r; return __retres; } /*@ requires finite: \is_finite(min) ∧ \is_finite(max); requires order: min ≤ max; ensures result_bounded: \is_finite(\result) ∧ \old(min) ≤ \result ≤ \old(max); assigns \result, Frama_C_entropy_source; assigns \result \from min, max, Frama_C_entropy_source; assigns Frama_C_entropy_source \from Frama_C_entropy_source; */ float Frama_C_float_interval(float min, float max) { float tmp; Frama_C_update_entropy(); if (Frama_C_entropy_source) tmp = min; else tmp = max; return tmp; } /*@ requires finite: \is_finite(min) ∧ \is_finite(max); requires order: min ≤ max; ensures result_bounded: \is_finite(\result) ∧ \old(min) ≤ \result ≤ \old(max); assigns \result, Frama_C_entropy_source; assigns \result \from min, max, Frama_C_entropy_source; assigns Frama_C_entropy_source \from Frama_C_entropy_source; */ double Frama_C_double_interval(double min, double max) { double tmp; Frama_C_update_entropy(); if (Frama_C_entropy_source) tmp = min; else tmp = max; return tmp; } extern __attribute__((__noreturn__)) void __builtin_abort(void); /*@ terminates \false; ensures never_terminates: \false; assigns \nothing; */ __attribute__((__noreturn__)) void Frama_C_abort(void); void Frama_C_abort(void) { __builtin_abort(); return; } void __FC_assert(int c, char const *file, int line, char const *expr); /*@ assigns \nothing; */ extern void Frama_C_show_each_warning(); /*@ requires nonnull_c: c ≢ 0; terminates c ≢ 0; assigns \nothing; */ void __FC_assert(int c, char const *file, int line, char const *expr) { if (! c) { Frama_C_show_each_warning("Assertion may fail",file,line,expr); Frama_C_abort(); } return; } int isalnum(int c); int isalpha(int c); int isblank(int c); int iscntrl(int c); int isdigit(int c); int isgraph(int c); int islower(int c); int isprint(int c); int ispunct(int c); int isspace(int c); int isupper(int c); int isxdigit(int c); int tolower(int c); int toupper(int c); /*@ requires c_uchar_or_eof: (0 ≤ c ≤ 255) ∨ c ≡ -1; assigns \result; assigns \result \from c; behavior match: assumes c_ascii: 0 ≤ c ≤ 127; ensures nonzero_result: \result < 0 ∨ \result > 0; behavior no_match: assumes c_non_ascii: ¬(0 ≤ c ≤ 127); ensures zero_result: \result ≡ 0; complete behaviors no_match, match; disjoint behaviors no_match, match; */ extern int isascii(int c); /*@ requires c_uchar_or_eof_or_EOF: (0 ≤ c ≤ 255) ∨ c ≡ -1; assigns \result; assigns \result \from c; behavior definitely_match: assumes c_alnum: ('A' ≤ c ≤ 'Z') ∨ ('a' ≤ c ≤ 'z') ∨ ('0' ≤ c ≤ '9'); ensures nonzero_result: \result < 0 ∨ \result > 0; behavior definitely_not_match: assumes c_non_alnum: c ≡ -1 ∨ (0 ≤ c ≤ 47) ∨ (58 ≤ c ≤ 64) ∨ (91 ≤ c ≤ 96) ∨ (123 ≤ c ≤ 127); ensures zero_result: \result ≡ 0; disjoint behaviors definitely_not_match, definitely_match; */ int isalnum(int c) { int tmp; if (c >= 'A') { if (c <= 'Z') tmp = 1; else goto _LAND_0; } else { _LAND_0: ; if (c >= 'a') { if (c <= 'z') tmp = 1; else goto _LAND; } else { _LAND: ; if (c >= '0') if (c <= '9') tmp = 1; else tmp = 0; else tmp = 0; } } return tmp; } /*@ requires c_uchar_or_eof: (0 ≤ c ≤ 255) ∨ c ≡ -1; assigns \result; assigns \result \from c; behavior definitely_match: assumes c_alpha: ('A' ≤ c ≤ 'Z') ∨ ('a' ≤ c ≤ 'z'); ensures nonzero_result: \result < 0 ∨ \result > 0; behavior definitely_not_match: assumes c_non_alpha: c ≡ -1 ∨ (0 ≤ c ≤ 64) ∨ (91 ≤ c ≤ 96) ∨ (123 ≤ c ≤ 127); ensures zero_result: \result ≡ 0; disjoint behaviors definitely_not_match, definitely_match; */ int isalpha(int c) { int tmp; if (c >= 'A') { if (c <= 'Z') tmp = 1; else goto _LAND; } else { _LAND: ; if (c >= 'a') if (c <= 'z') tmp = 1; else tmp = 0; else tmp = 0; } return tmp; } /*@ requires c_uchar_or_eof: (0 ≤ c ≤ 255) ∨ c ≡ -1; assigns \result; assigns \result \from c; behavior match: assumes c_tab_or_space: c ≡ ' ' ∨ c ≡ '\t'; ensures nonzero_result: \result < 0 ∨ \result > 0; behavior no_match: assumes c_non_blank: c ≢ ' ' ∧ c ≢ '\t'; ensures zero_result: \result ≡ 0; complete behaviors no_match, match; disjoint behaviors no_match, match; */ int isblank(int c) { int tmp; if (c == ' ') tmp = 1; else if (c == '\t') tmp = 1; else if (c == ' ') tmp = 1; else if (c == '\f') tmp = 1; else if (c == '\n') tmp = 1; else if (c == '\r') tmp = 1; else if (c == '\t') tmp = 1; else if (c == '\v') tmp = 1; else tmp = 0; return tmp; } /*@ requires c_uchar_or_eof: (0 ≤ c ≤ 255) ∨ c ≡ -1; assigns \result; assigns \result \from c; behavior definitely_match: assumes c_control_char: (0 ≤ c ≤ 31) ∨ c ≡ 127; ensures nonzero_result: \result < 0 ∨ \result > 0; behavior definitely_not_match: assumes c_non_control_char: c ≡ -1 ∨ (32 ≤ c ≤ 126); ensures zero_result: \result ≡ 0; disjoint behaviors definitely_not_match, definitely_match; */ int iscntrl(int c) { int tmp; tmp = Frama_C_nondet(0,1); return tmp; } /*@ requires c_uchar_or_eof: (0 ≤ c ≤ 255) ∨ c ≡ -1; assigns \result; assigns \result \from c; behavior match: assumes c_digit: '0' ≤ c ≤ '9'; ensures nonzero_result: \result < 0 ∨ \result > 0; behavior no_match: assumes c_non_digit: c < '0' ∨ c > '9'; ensures zero_result: \result ≡ 0; complete behaviors no_match, match; disjoint behaviors no_match, match; */ int isdigit(int c) { int tmp; if (c >= '0') if (c <= '9') tmp = 1; else tmp = 0; else tmp = 0; return tmp; } /*@ requires c_uchar_or_eof: (0 ≤ c ≤ 255) ∨ c ≡ -1; assigns \result; assigns \result \from c; behavior definitely_match: assumes c_graphical: 33 ≤ c ≤ 126; ensures nonzero_result: \result < 0 ∨ \result > 0; behavior definitely_not_match: assumes c_non_graphical: c ≡ -1 ∨ (0 ≤ c ≤ 32) ∨ c ≡ 127; ensures zero_result: \result ≡ 0; disjoint behaviors definitely_not_match, definitely_match; */ int isgraph(int c) { int tmp; tmp = Frama_C_nondet(0,1); return tmp; } /*@ requires c_uchar_or_eof: (0 ≤ c ≤ 255) ∨ c ≡ -1; assigns \result; assigns \result \from c; behavior definitely_match: assumes c_lower: 'a' ≤ c ≤ 'z'; ensures nonzero_result: \result < 0 ∨ \result > 0; behavior definitely_not_match: assumes c_non_lower: c ≡ -1 ∨ (0 ≤ c < 'a') ∨ ('z' < c < 127); ensures zero_result: \result ≡ 0; disjoint behaviors definitely_not_match, definitely_match; */ int islower(int c) { int tmp; if (c >= 'a') if (c <= 'z') tmp = 1; else tmp = 0; else tmp = 0; return tmp; } /*@ requires c_uchar_or_eof: (0 ≤ c ≤ 255) ∨ c ≡ -1; assigns \result; assigns \result \from c; behavior definitely_match: assumes c_printable: 32 ≤ c ≤ 126; ensures nonzero_result: \result < 0 ∨ \result > 0; behavior definitely_not_match: assumes c_non_printable: c ≡ -1 ∨ (0 ≤ c ≤ 31) ∨ c ≡ 127; ensures zero_result: \result ≡ 0; disjoint behaviors definitely_not_match, definitely_match; */ int isprint(int c) { int tmp; tmp = Frama_C_nondet(0,1); return tmp; } /*@ requires c_uchar_or_eof: (0 ≤ c ≤ 255) ∨ c ≡ -1; assigns \result; assigns \result \from c; behavior definitely_match: assumes c_punct: (33 ≤ c ≤ 47) ∨ (58 ≤ c ≤ 64) ∨ (91 ≤ c ≤ 96) ∨ (123 ≤ c ≤ 126); ensures nonzero_result: \result < 0 ∨ \result > 0; behavior definitely_not_match: assumes c_non_punct: c ≡ -1 ∨ (0 ≤ c ≤ 32) ∨ (48 ≤ c ≤ 57) ∨ (65 ≤ c ≤ 90) ∨ (97 ≤ c ≤ 122) ∨ c ≡ 127; ensures zero_result: \result ≡ 0; disjoint behaviors definitely_not_match, definitely_match; */ int ispunct(int c) { int tmp; tmp = Frama_C_nondet(0,1); return tmp; } /*@ requires c_uchar_or_eof: (0 ≤ c ≤ 255) ∨ c ≡ -1; assigns \result; assigns \result \from c; behavior definitely_match: assumes c_space: (9 ≤ c ≤ 13) ∨ c ≡ ' '; ensures nonzero_result: \result < 0 ∨ \result > 0; behavior definitely_not_match: assumes c_non_space: c ≡ -1 ∨ (0 ≤ c ≤ 8) ∨ (14 ≤ c < ' ') ∨ (' ' < c ≤ 127); ensures zero_result: \result ≡ 0; disjoint behaviors definitely_not_match, definitely_match; */ int isspace(int c) { int tmp; if (c == ' ') tmp = 1; else if (c == '\f') tmp = 1; else if (c == '\n') tmp = 1; else if (c == '\r') tmp = 1; else if (c == '\t') tmp = 1; else if (c == '\v') tmp = 1; else tmp = 0; return tmp; } /*@ requires c_uchar_or_eof: (0 ≤ c ≤ 255) ∨ c ≡ -1; assigns \result; assigns \result \from c; behavior definitely_match: assumes c_upper: 'A' ≤ c ≤ 'Z'; ensures nonzero_result: \result < 0 ∨ \result > 0; behavior definitely_not_match: assumes c_non_upper: c ≡ -1 ∨ (0 ≤ c < 'A') ∨ ('Z' < c ≤ 127); ensures zero_result: \result ≡ 0; disjoint behaviors definitely_not_match, definitely_match; */ int isupper(int c) { int tmp; if (c >= 'A') if (c <= 'Z') tmp = 1; else tmp = 0; else tmp = 0; return tmp; } /*@ requires c_uchar_or_eof: (0 ≤ c ≤ 255) ∨ c ≡ -1; assigns \result; assigns \result \from c; behavior match: assumes c_hexa_digit: ('0' ≤ c ≤ '9') ∨ ('A' ≤ c ≤ 'F') ∨ ('a' ≤ c ≤ 'f'); ensures nonzero_result: \result < 0 ∨ \result > 0; behavior no_match: assumes c_non_hexa_digit: ¬(('0' ≤ c ≤ '9') ∨ ('A' ≤ c ≤ 'F') ∨ ('a' ≤ c ≤ 'f')); ensures zero_result: \result ≡ 0; complete behaviors no_match, match; disjoint behaviors no_match, match; */ int isxdigit(int c) { int tmp; if (c >= '0') { if (c <= '9') tmp = 1; else goto _LAND_0; } else { _LAND_0: ; if (c >= 'a') { if (c <= 'f') tmp = 1; else goto _LAND; } else { _LAND: ; if (c >= 'A') if (c <= 'F') tmp = 1; else tmp = 0; else tmp = 0; } } return tmp; } /*@ requires c_uchar_or_eof: (0 ≤ c ≤ 255) ∨ c ≡ -1; ensures result_uchar_of_eof: (0 ≤ \result ≤ 255) ∨ \result ≡ -1; assigns \result; assigns \result \from c; behavior definitely_changed: assumes c_ascii_upper: 'A' ≤ c ≤ 'Z'; ensures result_ascii_lower: \result ≡ \old(c) + 32; behavior definitely_not_changed: assumes c_ascii_but_non_upper: c ≡ -1 ∨ (0 ≤ c < 'A') ∨ ('Z' < c ≤ 127); ensures result_unchanged: \result ≡ \old(c); disjoint behaviors definitely_not_changed, definitely_changed; */ int tolower(int c) { int __retres; if (c >= 'A') if (c <= 'Z') { __retres = c + 0x20; goto return_label; } __retres = c; return_label: return __retres; } /*@ requires c_uchar_of_eof: (0 ≤ c ≤ 255) ∨ c ≡ -1; ensures result_uchar_of_eof: (0 ≤ \result ≤ 255) ∨ \result ≡ -1; assigns \result; assigns \result \from c; behavior definitely_changed: assumes c_ascii_lower: 'a' ≤ c ≤ 'z'; ensures result_ascii_upper: \result ≡ \old(c) - 32; behavior definitely_not_changed: assumes c_ascii_but_non_lower: c ≡ -1 ∨ (0 ≤ c < 'a') ∨ ('z' < c ≤ 127); ensures result_unchanged: \result ≡ \old(c); disjoint behaviors definitely_not_changed, definitely_changed; */ int toupper(int c) { int __retres; if (c >= 'a') if (c <= 'z') { __retres = c - 0x20; goto return_label; } __retres = c; return_label: return __retres; } int __fc_errno; int __fc_errno = 0; int fetestexcept(int excepts); int feholdexcept(fenv_t *envp); int fesetenv(fenv_t const *envp); static int volatile fetestexcept___fc_random_fetestexcept __attribute__(( __FRAMA_C_MODEL__)); int fetestexcept(int excepts) { int __retres; __retres = 0x00FF & fetestexcept___fc_random_fetestexcept; return __retres; } fenv_t volatile __fc_fenv_state __attribute__((__FRAMA_C_MODEL__)); int feholdexcept(fenv_t *envp) { int __retres; *envp = __fc_fenv_state; __retres = 0; return __retres; } int fesetenv(fenv_t const *envp) { int __retres; __fc_fenv_state = *envp; __retres = 0; return __retres; } /*@ axiomatic MemCmp { logic ℤ memcmp{L1, L2}(char *s1, char *s2, ℤ n) reads \at(*(s1 + (0 .. n - 1)),L1), \at(*(s2 + (0 .. n - 1)),L2); axiom memcmp_zero{L1, L2}: ∀ char *s1, char *s2; ∀ ℤ n; memcmp{L1, L2}(s1, s2, n) ≡ 0 ⇔ (∀ ℤ i; 0 ≤ i < n ⇒ \at(*(s1 + i),L1) ≡ \at(*(s2 + i),L2)); } */ /*@ axiomatic MemChr { logic 𝔹 memchr{L}(char *s, ℤ c, ℤ n) reads *(s + (0 .. n - 1)); logic ℤ memchr_off{L}(char *s, ℤ c, ℤ n) reads *(s + (0 .. n - 1)); axiom memchr_def{L}: ∀ char *s; ∀ ℤ c; ∀ ℤ n; memchr(s, c, n) ≡ \true ⇔ (∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c); } */ /*@ axiomatic MemSet { logic 𝔹 memset{L}(char *s, ℤ c, ℤ n) reads *(s + (0 .. n - 1)); axiom memset_def{L}: ∀ char *s; ∀ ℤ c; ∀ ℤ n; memset(s, c, n) ≡ \true ⇔ (∀ ℤ i; 0 ≤ i < n ⇒ *(s + i) ≡ c); } */ /*@ axiomatic StrLen { logic ℤ strlen{L}(char *s) reads *(s + (0 ..)); axiom strlen_pos_or_null{L}: ∀ char *s; ∀ ℤ i; 0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ '\000') ∧ *(s + i) ≡ '\000' ⇒ strlen(s) ≡ i; axiom strlen_neg{L}: ∀ char *s; (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ '\000') ⇒ strlen(s) < 0; axiom strlen_before_null{L}: ∀ char *s; ∀ ℤ i; 0 ≤ i < strlen(s) ⇒ *(s + i) ≢ '\000'; axiom strlen_at_null{L}: ∀ char *s; 0 ≤ strlen(s) ⇒ *(s + strlen(s)) ≡ '\000'; axiom strlen_not_zero{L}: ∀ char *s; ∀ ℤ i; 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≢ '\000' ⇒ i < strlen(s); axiom strlen_zero{L}: ∀ char *s; ∀ ℤ i; 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≡ '\000' ⇒ i ≡ strlen(s); axiom strlen_sup{L}: ∀ char *s; ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ '\000' ⇒ 0 ≤ strlen(s) ≤ i; axiom strlen_shift{L}: ∀ char *s; ∀ ℤ i; 0 ≤ i ≤ strlen(s) ⇒ strlen(s + i) ≡ strlen(s) - i; axiom strlen_create{L}: ∀ char *s; ∀ ℤ i; 0 ≤ i ∧ *(s + i) ≡ '\000' ⇒ 0 ≤ strlen(s) ≤ i; axiom strlen_create_shift{L}: ∀ char *s; ∀ ℤ i; ∀ ℤ k; 0 ≤ k ≤ i ∧ *(s + i) ≡ '\000' ⇒ 0 ≤ strlen(s + k) ≤ i - k; axiom memcmp_strlen_left{L}: ∀ char *s1, char *s2; ∀ ℤ n; memcmp{L, L}(s1, s2, n) ≡ 0 ∧ strlen(s1) < n ⇒ strlen(s1) ≡ strlen(s2); axiom memcmp_strlen_right{L}: ∀ char *s1, char *s2; ∀ ℤ n; memcmp{L, L}(s1, s2, n) ≡ 0 ∧ strlen(s2) < n ⇒ strlen(s1) ≡ strlen(s2); axiom memcmp_strlen_shift_left{L}: ∀ char *s1, char *s2; ∀ ℤ k, ℤ n; memcmp{L, L}(s1, s2 + k, n) ≡ 0 ≤ k ∧ strlen(s1) < n ⇒ 0 ≤ strlen(s2) ≤ k + strlen(s1); axiom memcmp_strlen_shift_right{L}: ∀ char *s1, char *s2; ∀ ℤ k, ℤ n; memcmp{L, L}(s1 + k, s2, n) ≡ 0 ≤ k ∧ strlen(s2) < n ⇒ 0 ≤ strlen(s1) ≤ k + strlen(s2); } */ /*@ axiomatic StrCmp { logic ℤ strcmp{L}(char *s1, char *s2) reads *(s1 + (0 .. strlen(s1))), *(s2 + (0 .. strlen(s2))); axiom strcmp_zero{L}: ∀ char *s1, char *s2; strcmp(s1, s2) ≡ 0 ⇔ strlen(s1) ≡ strlen(s2) ∧ (∀ ℤ i; 0 ≤ i ≤ strlen(s1) ⇒ *(s1 + i) ≡ *(s2 + i)); } */ /*@ axiomatic StrNCmp { logic ℤ strncmp{L}(char *s1, char *s2, ℤ n) reads *(s1 + (0 .. n - 1)), *(s2 + (0 .. n - 1)); axiom strncmp_zero{L}: ∀ char *s1, char *s2; ∀ ℤ n; strncmp(s1, s2, n) ≡ 0 ⇔ (strlen(s1) < n ∧ strcmp(s1, s2) ≡ 0) ∨ (∀ ℤ i; 0 ≤ i < n ⇒ *(s1 + i) ≡ *(s2 + i)); } */ /*@ axiomatic StrChr { logic 𝔹 strchr{L}(char *s, ℤ c) reads *(s + (0 .. strlen(s))); axiom strchr_def{L}: ∀ char *s; ∀ ℤ c; strchr(s, c) ≡ \true ⇔ (∃ ℤ i; 0 ≤ i ≤ strlen(s) ∧ *(s + i) ≡ (char)c); } */ /*@ axiomatic WMemChr { logic 𝔹 wmemchr{L}(wchar_t *s, wchar_t c, ℤ n) reads *(s + (0 .. n - 1)); logic ℤ wmemchr_off{L}(wchar_t *s, wchar_t c, ℤ n) reads *(s + (0 .. n - 1)); axiom wmemchr_def{L}: ∀ wchar_t *s; ∀ int c; ∀ ℤ n; wmemchr(s, c, n) ≡ \true ⇔ (∃ int i; 0 ≤ i < n ∧ *(s + i) ≡ c); } */ /*@ axiomatic WcsLen { logic ℤ wcslen{L}(wchar_t *s) reads *(s + (0 ..)); axiom wcslen_pos_or_null{L}: ∀ wchar_t *s; ∀ ℤ i; 0 ≤ i ∧ (∀ ℤ j; 0 ≤ j < i ⇒ *(s + j) ≢ 0) ∧ *(s + i) ≡ 0 ⇒ wcslen(s) ≡ i; axiom wcslen_neg{L}: ∀ wchar_t *s; (∀ ℤ i; 0 ≤ i ⇒ *(s + i) ≢ 0) ⇒ wcslen(s) < 0; axiom wcslen_before_null{L}: ∀ wchar_t *s; ∀ int i; 0 ≤ i < wcslen(s) ⇒ *(s + i) ≢ 0; axiom wcslen_at_null{L}: ∀ wchar_t *s; 0 ≤ wcslen(s) ⇒ *(s + wcslen(s)) ≡ 0; axiom wcslen_not_zero{L}: ∀ wchar_t *s; ∀ int i; 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≢ 0 ⇒ i < wcslen(s); axiom wcslen_zero{L}: ∀ wchar_t *s; ∀ int i; 0 ≤ i ≤ wcslen(s) ∧ *(s + i) ≡ 0 ⇒ i ≡ wcslen(s); axiom wcslen_sup{L}: ∀ wchar_t *s; ∀ int i; 0 ≤ i ∧ *(s + i) ≡ 0 ⇒ 0 ≤ wcslen(s) ≤ i; axiom wcslen_shift{L}: ∀ wchar_t *s; ∀ int i; 0 ≤ i ≤ wcslen(s) ⇒ wcslen(s + i) ≡ wcslen(s) - i; axiom wcslen_create{L}: ∀ wchar_t *s; ∀ int i; 0 ≤ i ∧ *(s + i) ≡ 0 ⇒ 0 ≤ wcslen(s) ≤ i; axiom wcslen_create_shift{L}: ∀ wchar_t *s; ∀ int i; ∀ int k; 0 ≤ k ≤ i ∧ *(s + i) ≡ 0 ⇒ 0 ≤ wcslen(s + k) ≤ i - k; } */ /*@ axiomatic WcsCmp { logic ℤ wcscmp{L}(wchar_t *s1, wchar_t *s2) reads *(s1 + (0 .. wcslen(s1))), *(s2 + (0 .. wcslen(s2))); axiom wcscmp_zero{L}: ∀ wchar_t *s1, wchar_t *s2; wcscmp(s1, s2) ≡ 0 ⇔ wcslen(s1) ≡ wcslen(s2) ∧ (∀ ℤ i; 0 ≤ i ≤ wcslen(s1) ⇒ *(s1 + i) ≡ *(s2 + i)); } */ /*@ axiomatic WcsNCmp { logic ℤ wcsncmp{L}(wchar_t *s1, wchar_t *s2, ℤ n) reads *(s1 + (0 .. n - 1)), *(s2 + (0 .. n - 1)); axiom wcsncmp_zero{L}: ∀ wchar_t *s1, wchar_t *s2; ∀ ℤ n; wcsncmp(s1, s2, n) ≡ 0 ⇔ (wcslen(s1) < n ∧ wcscmp(s1, s2) ≡ 0) ∨ (∀ ℤ i; 0 ≤ i < n ⇒ *(s1 + i) ≡ *(s2 + i)); } */ /*@ axiomatic WcsChr { logic 𝔹 wcschr{L}(wchar_t *wcs, ℤ wc) reads *(wcs + (0 .. wcslen(wcs))); axiom wcschr_def{L}: ∀ wchar_t *wcs; ∀ ℤ wc; wcschr(wcs, wc) ≡ \true ⇔ (∃ ℤ i; 0 ≤ i ≤ wcslen(wcs) ∧ *(wcs + i) ≡ (int)wc); } */ /*@ logic ℤ minimum(ℤ i, ℤ j) = i < j? i: j; */ /*@ logic ℤ maximum(ℤ i, ℤ j) = i < j? j: i; */ /*@ predicate valid_string{L}(char *s) = 0 ≤ strlen(s) ∧ \valid(s + (0 .. strlen(s))); */ /*@ predicate valid_read_string{L}(char *s) = 0 ≤ strlen(s) ∧ \valid_read(s + (0 .. strlen(s))); */ /*@ predicate valid_read_nstring{L}(char *s, ℤ n) = (\valid_read(s + (0 .. n - 1)) ∧ \initialized(s + (0 .. n - 1))) ∨ valid_read_string(s); */ /*@ predicate valid_string_or_null{L}(char *s) = s ≡ \null ∨ valid_string(s); */ /*@ predicate valid_wstring{L}(wchar_t *s) = 0 ≤ wcslen(s) ∧ \valid(s + (0 .. wcslen(s))); */ /*@ predicate valid_read_wstring{L}(wchar_t *s) = 0 ≤ wcslen(s) ∧ \valid_read(s + (0 .. wcslen(s))); */ /*@ predicate valid_read_nwstring{L}(wchar_t *s, ℤ n) = (\valid_read(s + (0 .. n - 1)) ∧ \initialized(s + (0 .. n - 1))) ∨ valid_read_wstring(s); */ /*@ predicate valid_wstring_or_null{L}(wchar_t *s) = s ≡ \null ∨ valid_wstring(s); */ /*@ ghost int __fc_fds[1024]; */ /*@ requires valid_string_path: valid_read_string(path); requires valid_amode: (amode & ~((4 | 2) | 1)) ≡ 0 ∨ amode ≡ 0; ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1; assigns \result; assigns \result \from (indirect: path), (indirect: *(path + (0 ..))), (indirect: amode); */ extern int access(char const *path, int amode); /*@ requires valid_string_path: valid_read_string(path); ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1; assigns \result; assigns \result \from (indirect: path), (indirect: *(path + (0 ..))); */ extern int chdir(char const *path); /*@ requires valid_string_path: valid_read_string(path); ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1; assigns \result; assigns \result \from (indirect: path), (indirect: *(path + (0 ..))); */ extern int chroot(char const *path); /*@ requires valid_string_path: valid_read_string(path); ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1; assigns \result; assigns \result \from (indirect: path), (indirect: *(path + (0 ..))), (indirect: owner), (indirect: group); */ extern int chown(char const *path, uid_t owner, gid_t group); /*@ requires valid_fd: 0 ≤ fd < 1024; ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1; assigns __fc_fds[fd], \result; assigns __fc_fds[fd] \from fd, __fc_fds[fd]; assigns \result \from (indirect: fd), (indirect: __fc_fds[fd]); */ extern int close(int fd); /*@ requires valid_fildes: 0 ≤ fildes < 1024; ensures result_valid_fildes_or_error: \result ≡ -1 ∨ (\old(fildes) ≤ \result < 1024); assigns __fc_fds[fildes ..], \result; assigns __fc_fds[fildes ..] \from fildes; assigns \result \from fildes; */ extern int dup(int fildes); /*@ requires valid_fildes: 0 ≤ fildes < 1024; requires valid_fildes2: 0 ≤ fildes2 < 1024; ensures result_fildes2_or_error: \result ≡ \old(fildes2) ∨ \result ≡ -1; assigns __fc_fds[fildes2], \result; assigns __fc_fds[fildes2] \from fildes, fildes2, __fc_fds[fildes2]; assigns \result \from fildes, fildes2, __fc_fds[fildes], __fc_fds[fildes2]; */ extern int dup2(int fildes, int fildes2); /*@ requires valid_string_path: valid_read_string(path); requires valid_string_arg: valid_read_string(arg); assigns \result; assigns \result \from *(path + (0 ..)), *(arg + (0 ..)); */ extern int execl(char const *path, char const *arg, void * const *__va_params); /*@ requires valid_string_path: valid_read_string(path); requires valid_string_arg: valid_read_string(arg); assigns \result; assigns \result \from *(path + (0 ..)), *(arg + (0 ..)); */ extern int execle(char const *path, char const *arg, void * const *__va_params); /*@ requires valid_string_path: valid_read_string(path); requires valid_string_arg: valid_read_string(arg); assigns \result; assigns \result \from *(path + (0 ..)), *(arg + (0 ..)); */ extern int execlp(char const *path, char const *arg, void * const *__va_params); /*@ requires valid_string_path: valid_read_string(path); requires valid_string_argv0: valid_read_string(*(argv + 0)); assigns \result; assigns \result \from *(path + (0 ..)), *(argv + (0 ..)); */ extern int execv(char const *path, char * const *argv); /*@ requires valid_path: valid_read_string(path); requires valid_argv0: valid_read_string(*(argv + 0)); assigns \result; assigns \result \from *(path + (0 ..)), *(argv + (0 ..)); */ extern int execve(char const *path, char * const *argv, char * const *env); /*@ requires valid_string_path: valid_read_string(path); requires valid_string_argv0: valid_read_string(*(argv + 0)); assigns \result; assigns \result \from *(path + (0 ..)), *(argv + (0 ..)); */ extern int execvp(char const *path, char * const *argv); /*@ ensures never_terminates: \false; assigns \nothing; */ extern __attribute__((__noreturn__)) void _exit(int); /*@ ensures result_ok_child_or_error: \result ≡ 0 ∨ \result > 0 ∨ \result ≡ -1; assigns \result; assigns \result \from \nothing; */ extern pid_t fork(void); /*@ requires valid_buf: \valid(buf + (0 .. size - 1)); ensures result_ok_or_error: \result ≡ \null ∨ \result ≡ \old(buf); assigns *(buf + (0 .. size - 1)), \result; assigns *(buf + (0 .. size - 1)) \from (indirect: buf), (indirect: size); assigns \result \from buf, (indirect: size); */ extern char *getcwd(char *buf, size_t size); /*@ assigns \result; assigns \result \from \nothing; */ extern gid_t getegid(void); /*@ assigns \result; assigns \result \from \nothing; */ extern uid_t geteuid(void); /*@ assigns \result; assigns \result \from \nothing; */ extern gid_t getgid(void); extern char volatile __fc_hostname[64]; /*@ requires name_has_room: \valid(name + (0 .. len - 1)); ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1; assigns \result, *(name + (0 .. len - 1)); assigns \result \from (indirect: __fc_hostname[0 .. len]), (indirect: len); assigns *(name + (0 .. len - 1)) \from (indirect: __fc_hostname[0 .. len]), (indirect: len); */ extern int gethostname(char *name, size_t len); /*@ requires name_valid_string: valid_read_nstring(name, len); requires bounded_len: len ≤ 64; ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1; assigns __fc_hostname[0 .. len], \result; assigns __fc_hostname[0 .. len] \from *(name + (0 .. len - 1)), (indirect: len); assigns \result \from (indirect: __fc_hostname[0 .. len]); */ extern int sethostname(char const *name, size_t len); /*@ assigns \result; assigns \result \from (indirect: pid); */ extern pid_t getpgid(pid_t pid); /*@ assigns \result; assigns \result \from \nothing; */ extern pid_t getpgrp(void); /*@ assigns \result; assigns \result \from \nothing; */ extern pid_t getpid(void); /*@ assigns \result; assigns \result \from \nothing; */ extern pid_t getppid(void); /*@ assigns \result; assigns \result \from \nothing; */ extern pid_t getsid(pid_t); /*@ assigns \result; assigns \result \from \nothing; */ extern uid_t getuid(void); /*@ ensures result_true_or_false: \result ≡ 0 ∨ \result ≡ 1; assigns \result; assigns \result \from (indirect: fd), (indirect: __fc_fds[fd]); */ extern int isatty(int fd); /*@ requires valid_fd: 0 ≤ fd < 1024; requires valid_whence: whence ≡ 0 ∨ whence ≡ 1 ∨ whence ≡ 2; ensures result_error_or_offset: \result ≡ -1 ∨ 0 ≤ \result; assigns \result, __fc_fds[fd]; assigns \result \from (indirect: fd), (indirect: __fc_fds[fd]), (indirect: offset), (indirect: whence); assigns __fc_fds[fd] \from (indirect: fd), __fc_fds[fd], (indirect: offset), (indirect: whence); */ extern off_t lseek(int fd, off_t offset, int whence); /*@ requires valid_path: valid_read_string(path); assigns \result; assigns \result \from (indirect: *(path + (0 ..))), (indirect: name); */ extern long pathconf(char const *path, int name); /*@ requires valid_pipefd: \valid(pipefd + (0 .. 1)); ensures initialization: pipefd: \initialized(\old(pipefd) + (0 .. 1)); ensures valid_fd0: 0 ≤ *(\old(pipefd) + 0) < 1024; ensures valid_fd1: 0 ≤ *(\old(pipefd) + 1) < 1024; ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1; assigns *(pipefd + (0 .. 1)), \result; assigns *(pipefd + (0 .. 1)) \from (indirect: __fc_fds[0 ..]); assigns \result \from (indirect: __fc_fds[0 ..]); */ extern int pipe(int * /*[2]*/ pipefd); /*@ requires valid_fd: 0 ≤ fd < 1024; requires buf_has_room: \valid((char *)buf + (0 .. count - 1)); ensures result_error_or_read_length: (0 ≤ \result ≤ \old(count)) ∨ \result ≡ -1; ensures initialization: buf: \initialized((char *)\old(buf) + (0 .. \result - 1)); assigns __fc_fds[fd], \result, *((char *)buf + (0 .. count - 1)); assigns __fc_fds[fd] \from __fc_fds[fd]; assigns \result \from (indirect: __fc_fds[fd]), (indirect: count); assigns *((char *)buf + (0 .. count - 1)) \from (indirect: __fc_fds[fd]), (indirect: count); */ extern ssize_t read(int fd, void *buf, size_t count); /*@ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1; assigns \result; assigns \result \from (indirect: gid); */ extern int setegid(gid_t gid); /*@ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1; assigns \result; assigns \result \from (indirect: uid); */ extern int seteuid(uid_t uid); /*@ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1; assigns \result; assigns \result \from (indirect: gid); */ extern int setgid(gid_t gid); /*@ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1; assigns \result; assigns \result \from (indirect: pid), (indirect: pgid); */ extern int setpgid(pid_t pid, pid_t pgid); /*@ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1; assigns \result; assigns \result \from (indirect: rgid), (indirect: egid); */ extern int setregid(gid_t rgid, gid_t egid); /*@ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1; assigns \result; assigns \result \from (indirect: ruid), (indirect: euid); */ extern int setreuid(uid_t ruid, uid_t euid); /*@ ensures result_pgid_or_error: \result ≡ -1 ∨ \result ≥ 0; assigns \result; assigns \result \from \nothing; */ extern pid_t setsid(void); /*@ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1; assigns \result; assigns \result \from (indirect: uid); */ extern int setuid(uid_t uid); /*@ assigns \nothing; */ extern void sync(void); /*@ assigns \result; assigns \result \from (indirect: name); */ extern long sysconf(int name); char volatile __fc_ttyname[32]; char volatile *__fc_p_ttyname = __fc_ttyname; /*@ requires valid_fildes: 0 ≤ fildes < 1024; ensures result_name_or_null: \result ≡ __fc_p_ttyname ∨ \result ≡ \null; assigns \result; assigns \result \from __fc_p_ttyname, (indirect: fildes); */ extern char *ttyname(int fildes); /*@ requires valid_string_path: valid_read_string(path); ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1; assigns \result; assigns \result \from *(path + (0 ..)); */ extern int unlink(char const *path); /*@ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1; assigns \result, Frama_C_entropy_source; assigns \result \from (indirect: usec), (indirect: Frama_C_entropy_source); assigns Frama_C_entropy_source \from Frama_C_entropy_source; */ extern int usleep(useconds_t usec); /*@ requires valid_fd: 0 ≤ fd < 1024; requires buf_has_room: \valid_read((char *)buf + (0 .. count - 1)); ensures result_error_or_written_bytes: \result ≡ -1 ∨ (0 ≤ \result ≤ \old(count)); assigns __fc_fds[fd], \result; assigns __fc_fds[fd] \from (indirect: fd), (indirect: count), __fc_fds[fd]; assigns \result \from (indirect: fd), (indirect: count), (indirect: __fc_fds[fd]); */ extern ssize_t write(int fd, void const *buf, size_t count); /*@ requires valid_ruid: \valid(ruid); requires valid_euid: \valid(suid); requires valid_suid: \valid(euid); ensures initialization: result_ok_or_error: (\result ≡ 0 ∧ \initialized(\old(ruid)) ∧ \initialized(\old(euid)) ∧ \initialized(\old(suid))) ∨ \result ≡ -1; assigns *ruid, *euid, *suid, \result; assigns *ruid \from \nothing; assigns *euid \from \nothing; assigns *suid \from \nothing; assigns \result \from (indirect: ruid), (indirect: euid), (indirect: suid); */ int getresuid(uid_t *ruid, uid_t *euid, uid_t *suid); /*@ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1; assigns \result; assigns \result \from (indirect: ruid), (indirect: euid), (indirect: suid); */ int setresuid(uid_t ruid, uid_t euid, uid_t suid); /*@ requires valid_rgid: \valid(rgid); requires valid_egid: \valid(sgid); requires valid_sgid: \valid(egid); ensures initialization: result_ok_or_error: (\result ≡ 0 ∧ \initialized(\old(rgid)) ∧ \initialized(\old(egid)) ∧ \initialized(\old(sgid))) ∨ \result ≡ -1; assigns *rgid, *egid, *sgid, \result; assigns *rgid \from \nothing; assigns *egid \from \nothing; assigns *sgid \from \nothing; assigns \result \from (indirect: rgid), (indirect: egid), (indirect: sgid); */ int getresgid(gid_t *rgid, gid_t *egid, gid_t *sgid); /*@ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1; assigns \result; assigns \result \from (indirect: rgid), (indirect: egid), (indirect: sgid); */ int setresgid(gid_t rgid, gid_t egid, gid_t sgid); extern char *optarg; int optind; extern int opterr; extern int optopt; /*@ assigns \result, *optarg, optind, opterr, optopt; assigns \result \from argc, *(argv + (0 .. argc - 1)), *(optstring + (0 ..)); assigns *optarg \from argc, *(argv + (0 .. argc - 1)), *(optstring + (0 ..)); assigns optind \from argc, *(argv + (0 .. argc - 1)), *(optstring + (0 ..)); assigns opterr \from argc, *(argv + (0 .. argc - 1)), *(optstring + (0 ..)); assigns optopt \from argc, *(argv + (0 .. argc - 1)), *(optstring + (0 ..)); */ extern int getopt(int argc, char * const *argv, char const *optstring); /*@ assigns \result, *optarg, optind, opterr, optopt, *((longopts + (0 ..))->flag); assigns \result \from argc, *(argv + (0 .. argc - 1)), *(shortopts + (0 ..)), *(longopts + (0 ..)); assigns *optarg \from argc, *(argv + (0 .. argc - 1)), *(shortopts + (0 ..)), *(longopts + (0 ..)); assigns optind \from argc, *(argv + (0 .. argc - 1)), *(shortopts + (0 ..)), *(longopts + (0 ..)); assigns opterr \from argc, *(argv + (0 .. argc - 1)), *(shortopts + (0 ..)), *(longopts + (0 ..)); assigns optopt \from argc, *(argv + (0 .. argc - 1)), *(shortopts + (0 ..)), *(longopts + (0 ..)); assigns *((longopts + (0 ..))->flag) \from argc, *(argv + (0 .. argc - 1)), *(shortopts + (0 ..)), *(longopts + (0 ..)); */ extern int getopt_long(int argc, char * const *argv, char const *shortopts, struct option const *longopts, int *longind); /*@ assigns \result, *optarg, optind, opterr, optopt, *((longopts + (0 ..))->flag); assigns \result \from argc, *(argv + (0 .. argc - 1)), *(shortopts + (0 ..)), *(longopts + (0 ..)); assigns *optarg \from argc, *(argv + (0 .. argc - 1)), *(shortopts + (0 ..)), *(longopts + (0 ..)); assigns optind \from argc, *(argv + (0 .. argc - 1)), *(shortopts + (0 ..)), *(longopts + (0 ..)); assigns opterr \from argc, *(argv + (0 .. argc - 1)), *(shortopts + (0 ..)), *(longopts + (0 ..)); assigns optopt \from argc, *(argv + (0 .. argc - 1)), *(shortopts + (0 ..)), *(longopts + (0 ..)); assigns *((longopts + (0 ..))->flag) \from argc, *(argv + (0 .. argc - 1)), *(shortopts + (0 ..)), *(longopts + (0 ..)); */ extern int getopt_long_only(int argc, char * const *argv, char const *shortopts, struct option const *longopts, int *longind); int optind = 1; int glob(char const *pattern, int flags, int (*errfunc)(char const *epath, int eerrno), glob_t *pglob); void globfree(glob_t *pglob); /*@ ghost extern int __fc_heap_status __attribute__((__FRAMA_C_MODEL__)); */ /*@ axiomatic dynamic_allocation { predicate is_allocable{L}(ℤ n) reads __fc_heap_status; axiom never_allocable{L}: ∀ ℤ i; i < 0 ∨ i > 4294967295U ⇒ ¬is_allocable(i); } */ /*@ requires valid_nptr: \valid_read(nptr); assigns \result; assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..))); */ extern double atof(char const *nptr); int atoi(char const *p); /*@ requires valid_nptr: \valid_read(nptr); assigns \result; assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..))); */ extern long atol(char const *nptr); /*@ requires valid_nptr: \valid_read(nptr); assigns \result; assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..))); */ extern long long atoll(char const *nptr); /*@ requires valid_nptr: \valid_read(nptr); requires separation: \separated(nptr, endptr); assigns \result, *endptr; assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..))); assigns *endptr \from nptr, (indirect: *(nptr + (0 ..))), (indirect: endptr); behavior no_storage: assumes null_endptr: endptr ≡ \null; assigns \result; assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..))); behavior store_position: assumes nonnull_endptr: endptr ≢ \null; requires valid_endptr: \valid(endptr); ensures initialization: \initialized(\old(endptr)); ensures valid_endptr: \valid_read(\old(endptr)); ensures position_subset: \subset(*\old(endptr), \old(nptr) + (0 ..)); assigns \result, *endptr; assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..))); assigns *endptr \from nptr, (indirect: *(nptr + (0 ..))), (indirect: endptr); complete behaviors store_position, no_storage; disjoint behaviors store_position, no_storage; */ extern double strtod(char const * __restrict nptr, char ** __restrict endptr); /*@ requires valid_nptr: \valid_read(nptr); requires separation: \separated(nptr, endptr); assigns \result, *endptr; assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..))); assigns *endptr \from nptr, (indirect: *(nptr + (0 ..))), (indirect: endptr); behavior no_storage: assumes null_endptr: endptr ≡ \null; assigns \result; assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..))); behavior store_position: assumes nonnull_endptr: endptr ≢ \null; requires valid_endptr: \valid(endptr); ensures initialization: \initialized(\old(endptr)); ensures valid_endptr: \valid_read(\old(endptr)); ensures position_subset: \subset(*\old(endptr), \old(nptr) + (0 ..)); assigns \result, *endptr; assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..))); assigns *endptr \from nptr, (indirect: *(nptr + (0 ..))), (indirect: endptr); complete behaviors store_position, no_storage; disjoint behaviors store_position, no_storage; */ extern float strtof(char const * __restrict nptr, char ** __restrict endptr); /*@ requires valid_nptr: \valid_read(nptr); requires separation: \separated(nptr, endptr); assigns \result, *endptr; assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..))); assigns *endptr \from nptr, (indirect: *(nptr + (0 ..))), (indirect: endptr); behavior no_storage: assumes null_endptr: endptr ≡ \null; assigns \result; assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..))); behavior store_position: assumes nonnull_endptr: endptr ≢ \null; requires valid_endptr: \valid(endptr); ensures initialization: \initialized(\old(endptr)); ensures valid_endptr: \valid_read(\old(endptr)); ensures position_subset: \subset(*\old(endptr), \old(nptr) + (0 ..)); assigns \result, *endptr; assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..))); assigns *endptr \from nptr, (indirect: *(nptr + (0 ..))), (indirect: endptr); complete behaviors store_position, no_storage; disjoint behaviors store_position, no_storage; */ extern long double strtold(char const * __restrict nptr, char ** __restrict endptr); /*@ requires valid_nptr: \valid_read(nptr); requires separation: \separated(nptr, endptr); requires base_range: base ≡ 0 ∨ (2 ≤ base ≤ 36); assigns \result, *endptr; assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..))), (indirect: base); assigns *endptr \from nptr, (indirect: *(nptr + (0 ..))), (indirect: endptr), (indirect: base); behavior no_storage: assumes null_endptr: endptr ≡ \null; assigns \result; assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..))), (indirect: base); behavior store_position: assumes nonnull_endptr: endptr ≢ \null; requires valid_endptr: \valid(endptr); ensures initialization: \initialized(\old(endptr)); ensures valid_endptr: \valid_read(\old(endptr)); ensures position_subset: \subset(*\old(endptr), \old(nptr) + (0 ..)); assigns \result, *endptr; assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..))), (indirect: base); assigns *endptr \from nptr, (indirect: *(nptr + (0 ..))), (indirect: endptr), (indirect: base); complete behaviors store_position, no_storage; disjoint behaviors store_position, no_storage; */ extern long strtol(char const * __restrict nptr, char ** __restrict endptr, int base); /*@ requires valid_nptr: \valid_read(nptr); requires separation: \separated(nptr, endptr); requires base_range: base ≡ 0 ∨ (2 ≤ base ≤ 36); assigns \result, *endptr; assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..))), (indirect: base); assigns *endptr \from nptr, (indirect: *(nptr + (0 ..))), (indirect: endptr), (indirect: base); behavior no_storage: assumes null_endptr: endptr ≡ \null; assigns \result; assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..))), (indirect: base); behavior store_position: assumes nonnull_endptr: endptr ≢ \null; requires valid_endptr: \valid(endptr); ensures initialization: \initialized(\old(endptr)); ensures valid_endptr: \valid_read(\old(endptr)); ensures position_subset: \subset(*\old(endptr), \old(nptr) + (0 ..)); assigns \result, *endptr; assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..))), (indirect: base); assigns *endptr \from nptr, (indirect: *(nptr + (0 ..))), (indirect: endptr), (indirect: base); complete behaviors store_position, no_storage; disjoint behaviors store_position, no_storage; */ extern long long strtoll(char const * __restrict nptr, char ** __restrict endptr, int base); /*@ requires valid_nptr: \valid_read(nptr); requires separation: \separated(nptr, endptr); requires base_range: base ≡ 0 ∨ (2 ≤ base ≤ 36); assigns \result, *endptr; assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..))), (indirect: base); assigns *endptr \from nptr, (indirect: *(nptr + (0 ..))), (indirect: endptr), (indirect: base); behavior no_storage: assumes null_endptr: endptr ≡ \null; assigns \result; assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..))), (indirect: base); behavior store_position: assumes nonnull_endptr: endptr ≢ \null; requires valid_endptr: \valid(endptr); ensures initialization: \initialized(\old(endptr)); ensures valid_endptr: \valid_read(\old(endptr)); ensures position_subset: \subset(*\old(endptr), \old(nptr) + (0 ..)); assigns \result, *endptr; assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..))), (indirect: base); assigns *endptr \from nptr, (indirect: *(nptr + (0 ..))), (indirect: endptr), (indirect: base); complete behaviors store_position, no_storage; disjoint behaviors store_position, no_storage; */ extern unsigned long strtoul(char const * __restrict nptr, char ** __restrict endptr, int base); /*@ requires valid_nptr: \valid_read(nptr); requires separation: \separated(nptr, endptr); requires base_range: base ≡ 0 ∨ (2 ≤ base ≤ 36); assigns \result, *endptr; assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..))), (indirect: base); assigns *endptr \from nptr, (indirect: *(nptr + (0 ..))), (indirect: endptr), (indirect: base); behavior no_storage: assumes null_endptr: endptr ≡ \null; assigns \result; assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..))), (indirect: base); behavior store_position: assumes nonnull_endptr: endptr ≢ \null; requires valid_endptr: \valid(endptr); ensures initialization: \initialized(\old(endptr)); ensures valid_endptr: \valid_read(\old(endptr)); ensures position_subset: \subset(*\old(endptr), \old(nptr) + (0 ..)); assigns \result, *endptr; assigns \result \from (indirect: nptr), (indirect: *(nptr + (0 ..))), (indirect: base); assigns *endptr \from nptr, (indirect: *(nptr + (0 ..))), (indirect: endptr), (indirect: base); complete behaviors store_position, no_storage; disjoint behaviors store_position, no_storage; */ extern unsigned long long strtoull(char const * __restrict nptr, char ** __restrict endptr, int base); /*@ ghost extern int __fc_random_counter __attribute__((__unused__, __FRAMA_C_MODEL__)); */ unsigned long const __fc_rand_max = (unsigned long)32767; /*@ ensures result_range: 0 ≤ \result ≤ __fc_rand_max; assigns \result, __fc_random_counter; assigns \result \from __fc_random_counter; assigns __fc_random_counter \from __fc_random_counter; */ extern int rand(void); /*@ assigns __fc_random_counter; assigns __fc_random_counter \from seed; */ extern void srand(unsigned int seed); /*@ ensures result_range: 0 ≤ \result ≤ __fc_rand_max; assigns \result; assigns \result \from __fc_random_counter; */ extern long random(void); /*@ assigns __fc_random_counter; assigns __fc_random_counter \from seed; */ extern void srandom(unsigned int seed); int __fc_random48_init __attribute__((__FRAMA_C_MODEL__)); unsigned short __fc_random48_counter[3] __attribute__((__FRAMA_C_MODEL__)); unsigned short *__fc_p_random48_counter = __fc_random48_counter; /*@ ensures random48_initialized: __fc_random48_init ≡ 1; assigns __fc_random48_counter[0 .. 2], __fc_random48_init; assigns __fc_random48_counter[0 .. 2] \from seed; assigns __fc_random48_init \from \nothing; */ extern void srand48(long seed); /*@ requires initialization: initialized_seed16v: \initialized(seed16v + (0 .. 2)); ensures random48_initialized: __fc_random48_init ≡ 1; ensures result_counter: \result ≡ __fc_p_random48_counter; assigns __fc_random48_counter[0 .. 2], __fc_random48_init, \result; assigns __fc_random48_counter[0 .. 2] \from (indirect: *(seed16v + (0 .. 2))); assigns __fc_random48_init \from \nothing; assigns \result \from __fc_p_random48_counter; */ extern unsigned short *seed48(unsigned short * /*[3]*/ seed16v); /*@ ensures random48_initialized: __fc_random48_init ≡ 1; assigns __fc_random48_counter[0 .. 2], __fc_random48_init; assigns __fc_random48_counter[0 .. 2] \from *(param + (0 .. 5)); assigns __fc_random48_init \from \nothing; */ extern void lcong48(unsigned short * /*[7]*/ param); /*@ requires random48_initialized: __fc_random48_init ≡ 1; ensures result_range: \is_finite(\result) ∧ 0.0 ≤ \result < 1.0; assigns __fc_random48_counter[0 .. 2], \result; assigns __fc_random48_counter[0 .. 2] \from __fc_random48_counter[0 .. 2]; assigns \result \from __fc_random48_counter[0 .. 2]; */ extern double drand48(void); /*@ requires initialization: initialized_xsubi: \initialized(xsubi + (0 .. 2)); ensures result_range: \is_finite(\result) ∧ 0.0 ≤ \result < 1.0; assigns __fc_random48_counter[0 .. 2], \result; assigns __fc_random48_counter[0 .. 2] \from __fc_random48_counter[0 .. 2]; assigns \result \from __fc_random48_counter[0 .. 2]; */ extern double erand48(unsigned short * /*[3]*/ xsubi); /*@ requires random48_initialized: __fc_random48_init ≡ 1; ensures result_range: 0 ≤ \result < 2147483648; assigns __fc_random48_counter[0 .. 2], \result; assigns __fc_random48_counter[0 .. 2] \from __fc_random48_counter[0 .. 2]; assigns \result \from __fc_random48_counter[0 .. 2]; */ extern long lrand48(void); /*@ requires initialization: initialized_xsubi: \initialized(xsubi + (0 .. 2)); ensures result_range: 0 ≤ \result < 2147483648; assigns __fc_random48_counter[0 .. 2], \result; assigns __fc_random48_counter[0 .. 2] \from __fc_random48_counter[0 .. 2]; assigns \result \from __fc_random48_counter[0 .. 2]; */ extern long nrand48(unsigned short * /*[3]*/ xsubi); /*@ requires random48_initialized: __fc_random48_init ≡ 1; ensures result_range: -2147483648 ≤ \result < 2147483648; assigns __fc_random48_counter[0 .. 2], \result; assigns __fc_random48_counter[0 .. 2] \from __fc_random48_counter[0 .. 2]; assigns \result \from __fc_random48_counter[0 .. 2]; */ extern long mrand48(void); /*@ requires initialization: initialized_xsubi: \initialized(xsubi + (0 .. 2)); ensures result_range: -2147483648 ≤ \result < 2147483648; assigns __fc_random48_counter[0 .. 2], \result; assigns __fc_random48_counter[0 .. 2] \from __fc_random48_counter[0 .. 2]; assigns \result \from __fc_random48_counter[0 .. 2]; */ extern long jrand48(unsigned short * /*[3]*/ xsubi); void *calloc(size_t nmemb, size_t size); /*@ assigns __fc_heap_status, \result; assigns __fc_heap_status \from size, __fc_heap_status; assigns \result \from (indirect: size), (indirect: __fc_heap_status); allocates \result; behavior allocation: assumes can_allocate: is_allocable(size); ensures allocation: \fresh{Old, Here}(\result,\old(size)); assigns __fc_heap_status, \result; assigns __fc_heap_status \from size, __fc_heap_status; assigns \result \from (indirect: size), (indirect: __fc_heap_status); behavior no_allocation: assumes cannot_allocate: ¬is_allocable(size); ensures null_result: \result ≡ \null; assigns \result; assigns \result \from \nothing; allocates \nothing; complete behaviors no_allocation, allocation; disjoint behaviors no_allocation, allocation; */ extern void *malloc(size_t size); /*@ requires freeable: p ≡ \null ∨ \freeable(p); assigns __fc_heap_status; assigns __fc_heap_status \from __fc_heap_status; frees p; behavior deallocation: assumes nonnull_p: p ≢ \null; ensures freed: \allocable(\old(p)); assigns __fc_heap_status; assigns __fc_heap_status \from __fc_heap_status; behavior no_deallocation: assumes null_p: p ≡ \null; assigns \nothing; allocates \nothing; complete behaviors no_deallocation, deallocation; disjoint behaviors no_deallocation, deallocation; */ extern void free(void *p); /*@ requires freeable: ptr ≡ \null ∨ \freeable(ptr); assigns __fc_heap_status, \result; assigns __fc_heap_status \from __fc_heap_status; assigns \result \from size, ptr, __fc_heap_status; frees ptr; allocates \result; behavior allocation: assumes can_allocate: is_allocable(size); ensures allocation: \fresh{Old, Here}(\result,\old(size)); assigns \result; assigns \result \from size, __fc_heap_status; allocates \result; behavior deallocation: assumes nonnull_ptr: ptr ≢ \null; assumes can_allocate: is_allocable(size); ensures freed: \allocable(\old(ptr)); ensures freeable: \result ≡ \null ∨ \freeable(\result); frees ptr; behavior fail: assumes cannot_allocate: ¬is_allocable(size); ensures null_result: \result ≡ \null; assigns \result; assigns \result \from size, __fc_heap_status; allocates \nothing; complete behaviors fail, deallocation, allocation; disjoint behaviors allocation, fail; disjoint behaviors deallocation, fail; */ extern void *realloc(void *ptr, size_t size); /*@ exits status: \exit_status ≢ 0; ensures never_terminates: \false; assigns \exit_status \from \nothing; */ extern __attribute__((__noreturn__)) void abort(void); /*@ assigns \result; assigns \result \from \nothing; */ extern int atexit(void (*func)(void)); /*@ assigns \result; assigns \result \from \nothing; */ extern int at_quick_exit(void (*func)(void)); /*@ exits status: \exit_status ≡ \old(status); ensures never_terminates: \false; assigns \exit_status \from status; */ extern __attribute__((__noreturn__)) void exit(int status); /*@ ensures never_terminates: \false; assigns \nothing; */ extern __attribute__((__noreturn__)) void _Exit(int status); char *__fc_env[4096] __attribute__((__FRAMA_C_MODEL__)); char *getenv(char const *name); int putenv(char *string); int setenv(char const *name, char const *value, int overwrite); int unsetenv(char const *name); /*@ ensures never_terminates: \false; assigns \nothing; */ extern __attribute__((__noreturn__)) void quick_exit(int status); /*@ requires null_or_valid_string_command: command ≡ \null ∨ valid_read_string(command); assigns \result; assigns \result \from (indirect: command), (indirect: *(command + (0 ..))); */ extern int system(char const *command); /*@ requires valid_function_compar: \valid_function(compar); ensures null_or_correct_result: \result ≡ \null ∨ \subset(\result, (void *)((char *)\old(base) + (0 .. \old(size) * (\old(nmemb) - 1)))); assigns \result; assigns \result \from (indirect: key), *((char *)key + (0 .. size - 1)), base, *((char *)base + (0 .. size * (nmemb - 1))), (indirect: nmemb), (indirect: size), (indirect: *compar); */ extern void *bsearch(void const *key, void const *base, size_t nmemb, size_t size, int (*compar)(void const *, void const *)); /*@ requires valid_function_compar: \valid_function(compar); assigns *((char *)base + (0 ..)); assigns *((char *)base + (0 ..)) \from (indirect: base), *((char *)base + (0 ..)), (indirect: nmemb), (indirect: size), (indirect: compar), (indirect: *compar); */ extern void qsort(void *base, size_t nmemb, size_t size, int (*compar)(void const *, void const *)); int abs(int i); /*@ requires abs_representable: j > -2147483647L - 1L; assigns \result; assigns \result \from j; behavior negative: assumes negative: j < 0; ensures opposite_result: \result ≡ -\old(j); behavior nonnegative: assumes nonnegative: j ≥ 0; ensures same_result: \result ≡ \old(j); complete behaviors nonnegative, negative; disjoint behaviors nonnegative, negative; */ extern long labs(long j); /*@ requires abs_representable: j > -9223372036854775807LL - 1LL; assigns \result; assigns \result \from j; behavior negative: assumes negative: j < 0; ensures opposite_result: \result ≡ -\old(j); behavior nonnegative: assumes nonnegative: j ≥ 0; ensures same_result: \result ≡ \old(j); complete behaviors nonnegative, negative; disjoint behaviors nonnegative, negative; */ extern long long llabs(long long j); /*@ assigns \result; assigns \result \from numer, denom; */ extern div_t div(int numer, int denom); /*@ assigns \result; assigns \result \from numer, denom; */ extern ldiv_t ldiv(long numer, long denom); /*@ assigns \result; assigns \result \from numer, denom; */ extern lldiv_t lldiv(long long numer, long long denom); /*@ ghost extern int __fc_mblen_state; */ /*@ assigns \result, __fc_mblen_state; assigns \result \from (indirect: s), (indirect: *(s + (0 ..))), (indirect: n), __fc_mblen_state; assigns __fc_mblen_state \from (indirect: s), (indirect: *(s + (0 ..))), (indirect: n), __fc_mblen_state; */ extern int mblen(char const *s, size_t n); /*@ ghost extern int __fc_mbtowc_state; */ /*@ requires separation: \separated(pwc, s); ensures consumed_range: \result ≤ \old(n); assigns \result, *(pwc + (0 .. \result - 1)), __fc_mbtowc_state; assigns \result \from (indirect: s), (indirect: *(s + (0 .. n - 1))), (indirect: n), __fc_mbtowc_state; assigns *(pwc + (0 .. \result - 1)) \from (indirect: s), *(s + (0 .. n - 1)), (indirect: n), __fc_mbtowc_state; assigns __fc_mbtowc_state \from (indirect: s), *(s + (0 .. n - 1)), (indirect: n), __fc_mbtowc_state; */ extern int mbtowc(wchar_t * __restrict pwc, char const * __restrict s, size_t n); /*@ ghost extern int __fc_wctomb_state; */ /*@ assigns \result, *(s + (0 ..)), __fc_wctomb_state; assigns \result \from (indirect: wc), __fc_wctomb_state; assigns *(s + (0 ..)) \from wc, __fc_wctomb_state; assigns __fc_wctomb_state \from wc, __fc_wctomb_state; */ extern int wctomb(char *s, wchar_t wc); /*@ requires separation: \separated(pwcs, s); assigns \result, *(pwcs + (0 .. n - 1)); assigns \result \from (indirect: s), (indirect: *(s + (0 .. n - 1))), (indirect: n); assigns *(pwcs + (0 .. n - 1)) \from (indirect: s), *(s + (0 .. n - 1)), (indirect: n); */ extern size_t mbstowcs(wchar_t * __restrict pwcs, char const * __restrict s, size_t n); /*@ requires separation: \separated(s, pwcs); assigns \result, *(s + (0 .. n - 1)); assigns \result \from (indirect: pwcs), (indirect: *(pwcs + (0 .. n - 1))), (indirect: n); assigns *(s + (0 .. n - 1)) \from (indirect: pwcs), *(pwcs + (0 .. n - 1)), (indirect: n); */ extern size_t wcstombs(char * __restrict s, wchar_t const * __restrict pwcs, size_t n); int posix_memalign(void **memptr, size_t alignment, size_t size); /*@ requires valid_template: valid_string(templat); ensures result_error_or_valid_fd: \result ≡ -1 ∨ (0 ≤ \result < 16); assigns *(templat + (0 ..)), \result; assigns *(templat + (0 ..)) \from \nothing; assigns \result \from \nothing; */ extern int mkstemp(char *templat); int glob(char const *pattern, int flags, int (*errfunc)(char const *epath, int eerrno), glob_t *pglob) { int __retres; int tmp; unsigned int tmp_0; char **tmp_1; int tmp_4; tmp = Frama_C_interval(0,10); pglob->gl_pathc = (unsigned int)tmp; if (flags & (1 << 3)) tmp_0 = pglob->gl_offs; else tmp_0 = (unsigned int)0; size_t reserve_offs = tmp_0; size_t prev_len = (unsigned int)0; if (flags & (1 << 5)) while (*(pglob->gl_pathv + (reserve_offs + prev_len))) prev_len += (size_t)1; if (flags & (1 << 5)) tmp_1 = pglob->gl_pathv; else tmp_1 = (char **)0; char **path = tmp_1; if (pglob->gl_pathc == (unsigned int)0) if (flags & (1 << 4)) { pglob->gl_pathv = (char **)realloc((void *)path, ((reserve_offs + prev_len) + (size_t)2) * sizeof(char *)); if (! pglob->gl_pathv) { __retres = 1; goto return_label; } { size_t i = (unsigned int)0; while (i < reserve_offs) { *(pglob->gl_pathv + i) = (char *)0; i += (size_t)1; } } *(pglob->gl_pathv + (reserve_offs + prev_len)) = (char *)pattern; *(pglob->gl_pathv + ((reserve_offs + prev_len) + (size_t)1)) = (char *)0; __retres = 0; goto return_label; } else { __retres = 3; goto return_label; } pglob->gl_pathv = (char **)realloc((void *)path, (((reserve_offs + prev_len) + pglob->gl_pathc) + (size_t)1) * sizeof(char *)); if (! pglob->gl_pathv) { __retres = 1; goto return_label; } { size_t i_0 = (unsigned int)0; while (i_0 < reserve_offs) { *(pglob->gl_pathv + i_0) = (char *)0; i_0 += (size_t)1; } } { size_t i_1 = (unsigned int)0; while (i_1 < pglob->gl_pathc) { *(pglob->gl_pathv + ((reserve_offs + prev_len) + i_1)) = (char *)"glob result"; i_1 += (size_t)1; } } *(pglob->gl_pathv + ((prev_len + reserve_offs) + pglob->gl_pathc)) = (char *)0; tmp_4 = Frama_C_nondet(0,1); if (tmp_4) { __retres = 0; goto return_label; } else { if (errfunc) { int tmp_3; int tmp_2; tmp_2 = Frama_C_interval(0,255); tmp_3 = (*errfunc)("glob.c error path",tmp_2); int res = tmp_3; if (res) { __retres = 2; goto return_label; } else if (flags & (1 << 0)) { __retres = 2; goto return_label; } } __retres = 0; goto return_label; } return_label: return __retres; } void globfree(glob_t *pglob) { if (pglob->gl_pathc > (unsigned int)0) free((void *)pglob->gl_pathv); return; } intmax_t imaxabs(intmax_t c); imaxdiv_t imaxdiv(intmax_t numer, intmax_t denom); /*@ assigns \result, *(endptr + (..)), __fc_errno; assigns \result \from *(nptr + (..)), base; assigns *(endptr + (..)) \from *(nptr + (..)), base; assigns __fc_errno \from *(nptr + (..)), base; */ extern intmax_t strtoimax(char const * __restrict nptr, char ** __restrict endptr, int base); /*@ requires abs_representable: (long long)(-c) ≢ c; assigns \result; assigns \result \from c; */ intmax_t imaxabs(intmax_t c) { intmax_t __retres; if (c > (intmax_t)0) { __retres = c; goto return_label; } else { __retres = - c; goto return_label; } return_label: return __retres; } /*@ requires no_div_by_zero: denom ≢ 0; requires no_overflow: denom ≢ -1 ∨ (long long)(-numer) ≢ numer; ensures correct_div: \result.quot ≡ \old(numer) / \old(denom); ensures correct_mod: \result.rem ≡ \old(numer) % \old(denom); assigns \result; assigns \result \from numer, denom; */ imaxdiv_t imaxdiv(intmax_t numer, intmax_t denom) { imaxdiv_t r; r.quot = numer / denom; r.rem = numer % denom; return r; } extern struct lconv *__fc_locale; extern char *__fc_locale_names[512]; char *setlocale(int category, char const *locale); struct lconv *localeconv(void); struct lconv __C_locale = {.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)127, .frac_digits = (char)127, .p_cs_precedes = (char)127, .p_sep_by_space = (char)127, .n_cs_precedes = (char)127, .n_sep_by_space = (char)127, .p_sign_posn = (char)127, .n_sign_posn = (char)127, .int_p_cs_precedes = (char)127, .int_p_sep_by_space = (char)127, .int_n_cs_precedes = (char)127, .int_n_sep_by_space = (char)127, .int_p_sign_posn = (char)127, .int_n_sign_posn = (char)127}; struct lconv *__frama_c_locale = & __C_locale; char *__frama_c_locale_names[512] = {(char *)"C"}; /*@ requires locale_null_or_valid_string: locale ≡ \null ∨ valid_read_string(locale); ensures result_null_or_locale_name: \result ≡ \null ∨ (\valid(\result) ∧ (∃ ℤ i; \result ≡ __fc_locale_names[i])); assigns __fc_locale, \result; assigns __fc_locale \from category, *(locale + (..)); assigns \result \from __fc_locale, category, *(locale + (..)); */ char *setlocale(int category, char const *locale) { char *__retres; if ((int)*locale == 'C') { __frama_c_locale = & __C_locale; __retres = __frama_c_locale_names[0]; goto return_label; } __retres = (char *)0; return_label: return __retres; } /*@ ensures result_current_locale: \result ≡ __fc_locale; assigns \nothing; */ struct lconv *localeconv(void) { return __frama_c_locale; } /*@ assigns \result; assigns \result \from x; behavior nan: assumes is_nan: \is_NaN(x); ensures fp_nan: \result ≡ 0; behavior inf: assumes is_infinite: ¬\is_NaN(x) ∧ ¬\is_finite(x); ensures fp_infinite: \result ≡ 1; behavior zero: assumes is_a_zero: x ≡ 0.0; ensures fp_zero: \result ≡ 2; behavior subnormal: assumes is_finite: \is_finite(x); assumes is_subnormal: (x > 0.0 ∧ x < 0x1p-126) ∨ (x < 0.0 ∧ x > -0x1p-126); ensures fp_subnormal: \result ≡ 3; behavior normal: assumes is_finite: \is_finite(x); assumes not_subnormal: x ≤ -0x1p-126 ∨ x ≥ 0x1p-126; ensures fp_normal: \result ≡ 4; complete behaviors normal, subnormal, zero, inf, nan; disjoint behaviors normal, subnormal, zero, inf, nan; */ int __fc_fpclassifyf(float x); /*@ assigns \result; assigns \result \from x; behavior nan: assumes is_nan: \is_NaN(x); ensures fp_nan: \result ≡ 0; behavior inf: assumes is_infinite: ¬\is_NaN(x) ∧ ¬\is_finite(x); ensures fp_infinite: \result ≡ 1; behavior zero: assumes is_a_zero: x ≡ 0.0; ensures fp_zero: \result ≡ 2; behavior subnormal: assumes is_finite: \is_finite(x); assumes is_subnormal: (x > 0.0 ∧ x < 0x1p-1022) ∨ (x < 0.0 ∧ x > -0x1p-1022); ensures fp_subnormal: \result ≡ 3; behavior normal: assumes is_finite: \is_finite(x); assumes not_subnormal: x ≤ -0x1p-1022 ∨ x ≥ 0x1p-1022; ensures fp_normal: \result ≡ 4; complete behaviors normal, subnormal, zero, inf, nan; disjoint behaviors normal, subnormal, zero, inf, nan; */ int __fc_fpclassify(double x); /*@ assigns __fc_errno, \result; assigns __fc_errno \from x; assigns \result \from x; behavior normal: assumes in_domain: \is_finite(x) ∧ \abs(x) ≤ 1; ensures positive_result: \is_finite(\result) ∧ \result ≥ 0; assigns \result; assigns \result \from x; behavior domain_error: assumes out_of_domain: \is_infinite(x) ∨ (\is_finite(x) ∧ \abs(x) > 1); ensures errno_set: __fc_errno ≡ 1; assigns __fc_errno, \result; assigns __fc_errno \from x; assigns \result \from x; disjoint behaviors domain_error, normal; */ extern double acos(double x); /*@ assigns __fc_errno, \result; assigns __fc_errno \from x; assigns \result \from x; behavior normal: assumes in_domain: \is_finite(x) ∧ \abs(x) ≤ 1; ensures positive_result: \is_finite(\result) ∧ \result ≥ 0; assigns \result; assigns \result \from x; behavior domain_error: assumes out_of_domain: \is_infinite(x) ∨ (\is_finite(x) ∧ \abs(x) > 1); ensures errno_set: __fc_errno ≡ 1; assigns __fc_errno, \result; assigns __fc_errno \from x; assigns \result \from x; disjoint behaviors domain_error, normal; */ extern float acosf(float x); /*@ assigns __fc_errno, \result; assigns __fc_errno \from x; assigns \result \from x; behavior normal: assumes in_domain: \is_finite(x) ∧ \abs(x) ≤ 1; ensures positive_result: \is_finite(\result) ∧ \result ≥ 0; assigns \result; assigns \result \from x; behavior domain_error: assumes out_of_domain: \is_infinite(x) ∨ (\is_finite(x) ∧ \abs(x) > 1); ensures errno_set: __fc_errno ≡ 1; assigns __fc_errno, \result; assigns __fc_errno \from x; assigns \result \from x; disjoint behaviors domain_error, normal; */ extern long double acosl(long double x); /*@ assigns __fc_errno, \result; assigns __fc_errno \from x; assigns \result \from x; behavior normal: assumes in_domain: \is_finite(x) ∧ \abs(x) ≤ 1; ensures finite_result: \is_finite(\result); assigns \result; assigns \result \from x; behavior domain_error: assumes out_of_domain: \is_infinite(x) ∨ (\is_finite(x) ∧ \abs(x) > 1); ensures errno_set: __fc_errno ≡ 1; assigns __fc_errno, \result; assigns __fc_errno \from x; assigns \result \from x; disjoint behaviors domain_error, normal; */ extern double asin(double x); /*@ assigns __fc_errno, \result; assigns __fc_errno \from x; assigns \result \from x; behavior normal: assumes in_domain: \is_finite(x) ∧ \abs(x) ≤ 1; ensures finite_result: \is_finite(\result); assigns \result; assigns \result \from x; behavior domain_error: assumes out_of_domain: \is_infinite(x) ∨ (\is_finite(x) ∧ \abs(x) > 1); ensures errno_set: __fc_errno ≡ 1; assigns __fc_errno, \result; assigns __fc_errno \from x; assigns \result \from x; disjoint behaviors domain_error, normal; */ extern float asinf(float x); /*@ assigns __fc_errno, \result; assigns __fc_errno \from x; assigns \result \from x; behavior normal: assumes in_domain: \is_finite(x) ∧ \abs(x) ≤ 1; ensures finite_result: \is_finite(\result); assigns \result; assigns \result \from x; behavior domain_error: assumes out_of_domain: \is_infinite(x) ∨ (\is_finite(x) ∧ \abs(x) > 1); ensures errno_set: __fc_errno ≡ 1; assigns __fc_errno, \result; assigns __fc_errno \from x; assigns \result \from x; disjoint behaviors domain_error, normal; */ extern long double asinl(long double x); /*@ requires finite_arg: \is_finite(x); ensures finite_result: \is_finite(\result); ensures result_domain: -1.571 ≤ \result ≤ 1.571; assigns \result; assigns \result \from x; */ extern float atanf(float x); /*@ requires finite_arg: \is_finite(x); ensures finite_result: \is_finite(\result); ensures result_domain: -1.571 ≤ \result ≤ 1.571; assigns \result; assigns \result \from x; */ extern double atan(double x); /*@ requires finite_arg: \is_finite(x); ensures finite_result: \is_finite(\result); ensures result_domain: -1.571 ≤ \result ≤ 1.571; assigns \result; assigns \result \from x; */ extern long double atanl(long double x); /*@ requires finite_args: \is_finite(x) ∧ \is_finite(y); requires finite_result: \is_finite(atan2(x, y)); ensures finite_result: \is_finite(\result); assigns \result; assigns \result \from x, y; */ extern double atan2(double y, double x); /*@ requires finite_args: \is_finite(x) ∧ \is_finite(y); requires finite_logic_result: \is_finite(atan2f(x, y)); ensures finite_result: \is_finite(\result); assigns \result; assigns \result \from x, y; */ extern float atan2f(float y, float x); /*@ requires finite_arg: \is_finite(x); ensures finite_result: \is_finite(\result); ensures result_domain: -1. ≤ \result ≤ 1.; assigns \result; assigns \result \from x; */ extern double cos(double x); /*@ requires finite_arg: \is_finite(x); ensures finite_result: \is_finite(\result); ensures result_domain: -1. ≤ \result ≤ 1.; assigns \result; assigns \result \from x; */ extern float cosf(float x); /*@ requires finite_arg: \is_finite(x); ensures finite_result: \is_finite(\result); ensures result_domain: -1. ≤ \result ≤ 1.; assigns \result; assigns \result \from x; */ extern long double cosl(long double x); /*@ requires finite_arg: \is_finite(x); ensures finite_result: \is_finite(\result); ensures result_domain: -1. ≤ \result ≤ 1.; assigns \result; assigns \result \from x; */ extern double sin(double x); /*@ requires finite_arg: \is_finite(x); ensures finite_result: \is_finite(\result); ensures result_domain: -1. ≤ \result ≤ 1.; assigns \result; assigns \result \from x; */ extern float sinf(float x); /*@ requires finite_arg: \is_finite(x); ensures finite_result: \is_finite(\result); ensures result_domain: -1. ≤ \result ≤ 1.; assigns \result; assigns \result \from x; */ extern long double sinl(long double x); /*@ assigns __fc_errno, \result; assigns __fc_errno \from x; assigns \result \from x; behavior normal: assumes in_domain: \is_finite(x) ∧ x ≥ 1; ensures positive_result: \is_finite(\result) ∧ \result ≥ 0; assigns \result; assigns \result \from x; behavior infinite: assumes is_plus_infinity: \is_plus_infinity(x); ensures result_plus_infinity: \is_plus_infinity(\result); assigns \result; assigns \result \from x; behavior domain_error: assumes out_of_domain: \is_minus_infinity(x) ∨ (\is_finite(x) ∧ x < 1); ensures errno_set: __fc_errno ≡ 1; assigns __fc_errno, \result; assigns __fc_errno \from x; assigns \result \from x; disjoint behaviors domain_error, infinite, normal; */ extern double acosh(double x); /*@ assigns __fc_errno, \result; assigns __fc_errno \from x; assigns \result \from x; behavior normal: assumes in_domain: \is_finite(x) ∧ x ≥ 1; ensures positive_result: \is_finite(\result) ∧ \result ≥ 0; assigns \result; assigns \result \from x; behavior infinite: assumes is_plus_infinity: \is_plus_infinity(x); ensures result_plus_infinity: \is_plus_infinity(\result); assigns \result; assigns \result \from x; behavior domain_error: assumes out_of_domain: \is_minus_infinity(x) ∨ (\is_finite(x) ∧ x < 1); ensures errno_set: __fc_errno ≡ 1; assigns __fc_errno, \result; assigns __fc_errno \from x; assigns \result \from x; disjoint behaviors domain_error, infinite, normal; */ extern float acoshf(float x); /*@ assigns __fc_errno, \result; assigns __fc_errno \from x; assigns \result \from x; behavior normal: assumes in_domain: \is_finite(x) ∧ x ≥ 1; ensures positive_result: \is_finite(\result) ∧ \result ≥ 0; assigns \result; assigns \result \from x; behavior infinite: assumes is_plus_infinity: \is_plus_infinity(x); ensures result_plus_infinity: \is_plus_infinity(\result); assigns \result; assigns \result \from x; behavior domain_error: assumes out_of_domain: \is_minus_infinity(x) ∨ (\is_finite(x) ∧ x < 1); ensures errno_set: __fc_errno ≡ 1; assigns __fc_errno, \result; assigns __fc_errno \from x; assigns \result \from x; disjoint behaviors domain_error, infinite, normal; */ extern long double acoshl(long double x); /*@ requires finite_arg: \is_finite(x); requires finite_domain: x ≤ 0x1.62e42fefa39efp+9; ensures res_finite: \is_finite(\result); ensures positive_result: \result > 0.; assigns \result; assigns \result \from x; */ extern double exp(double x); /*@ requires finite_arg: \is_finite(x); requires res_finite: x ≤ 0x1.62e42ep+6; ensures res_finite: \is_finite(\result); ensures positive_result: \result > 0.; assigns \result; assigns \result \from x; */ extern float expf(float x); /*@ requires finite_arg: \is_finite(x); requires arg_positive: x > 0; ensures finite_result: \is_finite(\result); assigns \result; assigns \result \from x; */ extern double log(double x); /*@ requires finite_arg: \is_finite(x); requires arg_positive: x > 0; ensures finite_result: \is_finite(\result); assigns \result; assigns \result \from x; */ extern float logf(float x); /*@ requires finite_arg: \is_finite(x); requires arg_pos: x > 0; ensures finite_result: \is_finite(\result); assigns \result; assigns \result \from x; */ extern long double logl(long double x); /*@ requires finite_arg: \is_finite(x); requires arg_positive: x > 0; ensures finite_result: \is_finite(\result); assigns \result; assigns \result \from x; */ extern double log10(double x); /*@ requires finite_arg: \is_finite(x); requires arg_positive: x > 0; ensures finite_result: \is_finite(\result); assigns \result; assigns \result \from x; */ extern float log10f(float x); /*@ requires finite_arg: \is_finite(x); requires arg_postive: x > 0; ensures finite_result: \is_finite(\result); assigns \result; assigns \result \from x; */ extern long double log10l(long double x); /*@ requires finite_arg: \is_finite(x); requires arg_positive: x > 0; ensures finite_result: \is_finite(\result); assigns \result; assigns \result \from x; */ extern double log2(double x); /*@ requires finite_arg: \is_finite(x); requires arg_positive: x > 0; ensures finite_result: \is_finite(\result); assigns \result; assigns \result \from x; */ extern float log2f(float x); /*@ requires finite_arg: \is_finite(x); requires arg_positive: x > 0; ensures finite_result: \is_finite(\result); assigns \result; assigns \result \from x; */ extern long double log2l(long double x); double fabs(double x); float fabsf(float x); /*@ requires finite_arg: \is_finite(x); ensures res_finite: \is_finite(\result); ensures positive_result: \result ≥ 0.; ensures equal_magnitude_result: \result ≡ \old(x) ∨ \result ≡ -\old(x); assigns \result; assigns \result \from x; */ extern long double fabsl(long double x); /*@ requires finite_args: \is_finite(x) ∧ \is_finite(y); requires finite_logic_res: \is_finite(pow(x, y)); ensures finite_result: \is_finite(\result); assigns \result; assigns \result \from x, y; */ extern double pow(double x, double y); /*@ requires finite_args: \is_finite(x) ∧ \is_finite(y); requires finite_logic_res: \is_finite(powf(x, y)); ensures finite_result: \is_finite(\result); assigns \result; assigns \result \from x, y; */ extern float powf(float x, float y); /*@ requires finite_arg: \is_finite(x); requires arg_positive: x ≥ -0.; ensures finite_result: \is_finite(\result); ensures positive_result: \result ≥ -0.; assigns \result; assigns \result \from x; */ extern double sqrt(double x); /*@ requires finite_arg: \is_finite(x); requires arg_positive: x ≥ -0.; ensures finite_result: \is_finite(\result); ensures positive_result: \result ≥ -0.; assigns \result; assigns \result \from x; */ extern float sqrtf(float x); /*@ requires finite_arg: \is_finite(x); requires arg_positive: x ≥ -0.; ensures finite_result: \is_finite(\result); ensures positive_result: \result ≥ -0.; assigns \result; assigns \result \from x; */ extern long double sqrtl(long double x); /*@ requires finite_arg: \is_finite(x); ensures finite_result: \is_finite(\result); assigns \result; assigns \result \from x; */ extern double ceil(double x); /*@ requires finite_arg: \is_finite(x); ensures finite_result: \is_finite(\result); assigns \result; assigns \result \from x; */ extern float ceilf(float x); /*@ requires finite_arg: \is_finite(x); ensures finite_result: \is_finite(\result); assigns \result; assigns \result \from x; */ extern long double ceill(long double x); /*@ requires finite_arg: \is_finite(x); ensures finite_result: \is_finite(\result); assigns \result; assigns \result \from x; */ extern double floor(double x); /*@ requires finite_arg: \is_finite(x); ensures finite_result: \is_finite(\result); assigns \result; assigns \result \from x; */ extern float floorf(float x); /*@ requires finite_arg: \is_finite(x); ensures finite_result: \is_finite(\result); assigns \result; assigns \result \from x; */ extern long double floorl(long double x); /*@ requires finite_arg: \is_finite(x); ensures finite_result: \is_finite(\result); assigns \result; assigns \result \from x; */ extern double round(double x); /*@ requires finite_arg: \is_finite(x); ensures finite_result: \is_finite(\result); assigns \result; assigns \result \from x; */ extern float roundf(float x); /*@ requires finite_arg: \is_finite(x); ensures finite_result: \is_finite(\result); assigns \result; assigns \result \from x; */ extern long double roundl(long double x); /*@ requires finite_arg: \is_finite(x); ensures finite_result: \is_finite(\result); assigns \result; assigns \result \from x; */ extern double trunc(double x); /*@ requires finite_arg: \is_finite(x); ensures finite_result: \is_finite(\result); assigns \result; assigns \result \from x; */ extern float truncf(float x); /*@ requires finite_arg: \is_finite(x); ensures finite_result: \is_finite(\result); assigns \result; assigns \result \from x; */ extern long double truncl(long double x); /*@ requires finite_args: \is_finite(x) ∧ \is_finite(y); requires finite_logic_result: \is_finite(fmod(x, y)); ensures finite_result: \is_finite(\result); assigns \result; assigns \result \from x, y; */ extern double fmod(double x, double y); /*@ requires finite_args: \is_finite(x) ∧ \is_finite(y); requires finite_logic_result: \is_finite(fmodf(x, y)); ensures finite_result: \is_finite(\result); assigns \result; assigns \result \from x, y; */ extern float fmodf(float x, float y); /*@ requires tagp_valid_string: valid_read_string(tagp); ensures result_is_nan: \is_NaN(\result); assigns \result; assigns \result \from (indirect: *(tagp + (0 ..))); */ extern double nan(char const *tagp); /*@ requires tagp_valid_string: valid_read_string(tagp); ensures result_is_nan: \is_NaN(\result); assigns \result; assigns \result \from (indirect: *(tagp + (0 ..))); */ extern float nanf(char const *tagp); /*@ requires tagp_valid_string: valid_read_string(tagp); ensures result_is_nan: \is_NaN(\result); assigns \result; assigns \result \from (indirect: *(tagp + (0 ..))); */ extern long double nanl(char const *tagp); int __finitef(float f); int __finite(double d); /*@ logic float __fc_infinity(ℤ x) = \plus_infinity; */ /*@ logic float __fc_nan(ℤ x) = \NaN; */ /*@ ensures result_is_infinity: \is_plus_infinity(\result); assigns \result; assigns \result \from \nothing; */ extern float __fc_infinity(int x); /*@ ensures result_is_nan: \is_NaN(\result); assigns \result; assigns \result \from \nothing; */ extern float __fc_nan(int x); /*@ requires finite_arg: \is_finite(x); ensures res_finite: \is_finite(\result); ensures positive_result: \result ≥ 0.; ensures equal_magnitude_result: \result ≡ \old(x) ∨ \result ≡ -\old(x); assigns \result; assigns \result \from x; */ double fabs(double x) { double __retres; if (x == 0.0) { __retres = 0.0; goto return_label; } if (x > 0.0) { __retres = x; goto return_label; } __retres = - x; return_label: return __retres; } /*@ requires finite_arg: \is_finite(x); ensures res_finite: \is_finite(\result); ensures positive_result: \result ≥ 0.; ensures equal_magnitude_result: \result ≡ \old(x) ∨ \result ≡ -\old(x); assigns \result; assigns \result \from x; */ float fabsf(float x) { float __retres; if (x == 0.0f) { __retres = 0.0f; goto return_label; } else if (x > 0.0f) { __retres = x; goto return_label; } else { __retres = - x; goto return_label; } return_label: return __retres; } int __finitef(float f) { int __retres; union __fc_u_finitef u; unsigned short usExp; u.f = f; usExp = (unsigned short)((int)u.w[1] & 0x7F80); usExp = (unsigned short)((int)usExp >> 7); __retres = ! ((int)usExp == 0xff); return __retres; } int __finite(double d) { int __retres; union __fc_u_finite u; unsigned short usExp; u.d = d; usExp = (unsigned short)((int)u.w[3] & 0x7F80); usExp = (unsigned short)((int)usExp >> 7); __retres = ! ((int)usExp == 0xff); return __retres; } /*@ assigns \nothing; */ extern void (*signal(int sig, void (*func)(int )))(int ); /*@ ensures never_terminates: \false; assigns \nothing; */ extern int raise(int sig); /*@ requires valid_set: \valid(set); ensures initialization: set: \initialized(\old(set)); ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1; assigns *set, \result; assigns *set \from \nothing; assigns \result \from \nothing; */ extern int sigemptyset(sigset_t *set); /*@ requires valid_set: \valid(set); ensures initialization: set: \initialized(\old(set)); ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1; assigns *set, \result; assigns *set \from \nothing; assigns \result \from \nothing; */ extern int sigfillset(sigset_t *set); /*@ requires valid_set: \valid(set); requires initialization: set: \initialized(set); ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1; assigns *set, \result; assigns *set \from (indirect: signum); assigns \result \from signum; */ extern int sigaddset(sigset_t *set, int signum); /*@ requires valid_set: \valid(set); requires initialization: set: \initialized(set); ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1; assigns *set, \result; assigns *set \from (indirect: signum); assigns \result \from signum; */ extern int sigdelset(sigset_t *set, int signum); /*@ requires valid_read_set: \valid_read(set); requires initialization: set: \initialized(set); ensures result_found_not_found_or_error: \result ≡ 0 ∨ \result ≡ 1 ∨ \result ≡ -1; assigns \result; assigns \result \from *set, signum; */ extern int sigismember(sigset_t const *set, int signum); struct sigaction __fc_sigaction[64 + 1]; struct sigaction *__fc_p_sigaction = __fc_sigaction; /*@ requires valid_signal: 0 ≤ signum ≤ 64; requires valid_oldact_or_null: oldact ≡ \null ∨ \valid(oldact); requires valid_read_act_or_null: act ≡ \null ∨ \valid_read(act); requires separation: separated_acts: \separated(act, oldact); ensures act_changed: \old(act) ≡ \null ∨ \subset(*(__fc_p_sigaction + \old(signum)), *\old(act)); ensures oldact_assigned: \old(oldact) ≡ \null ∨ *\old(oldact) ∈ *(__fc_p_sigaction + \old(signum)); ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1; assigns *oldact, *(__fc_p_sigaction + signum), \result; assigns *oldact \from __fc_p_sigaction; assigns *(__fc_p_sigaction + signum) \from *act; assigns \result \from (indirect: signum), (indirect: act), (indirect: *act), (indirect: oldact), (indirect: *oldact); */ extern int sigaction(int signum, struct sigaction const * __restrict act, struct sigaction * __restrict oldact); /*@ requires valid_set_or_null: set ≡ \null ∨ \valid_read(set); requires valid_how: set ≢ \null ⇒ how ∈ {0, 2, 1}; requires valid_oldset_or_null: oldset ≡ \null ∨ \valid(oldset); requires separation: (set ≡ oldset ≡ \null) ∨ \separated(set, oldset); ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1; ensures initialization: oldset_initialized: \old(oldset) ≢ \null ∧ \result ≡ 0 ⇒ \initialized(\old(oldset)); assigns \result, *oldset; assigns \result \from (indirect: how), (indirect: set), (indirect: oldset); assigns *oldset \from (indirect: how), (indirect: oldset); */ extern int sigprocmask(int how, sigset_t const * __restrict set, sigset_t * __restrict oldset); /*@ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1; assigns \result; assigns \result \from (indirect: pid), (indirect: sig); */ extern int kill(pid_t pid, int sig); /*@ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1; assigns \result; assigns \result \from (indirect: pgrp), (indirect: sig); */ extern int killpg(pid_t pgrp, int sig); /*@ requires valid_read_iov: \valid_read(iov + (0 .. iovcnt - 1)); assigns *((char *)(iov + (0 .. iovcnt - 1))->iov_base + (0 ..)); */ extern ssize_t readv(int fd, struct iovec const *iov, int iovcnt); /*@ ghost struct __fc_sockfds_type __fc_sockfds[1024]; */ /*@ ghost extern int __fc_socket_counter __attribute__((__FRAMA_C_MODEL__)); */ /*@ ghost int volatile __fc_open_sock_fds; */ /*@ requires valid_sockfd: 0 ≤ sockfd < 1024; ensures result_error_or_valid_new_sockfd: \result ≡ -1 ∨ (0 ≤ \result < 1024); assigns \result, *((char *)addr + (0 .. *addrlen - 1)), __fc_sockfds[sockfd]; assigns \result \from *addr, *addrlen, __fc_sockfds[sockfd]; assigns *((char *)addr + (0 .. *addrlen - 1)) \from *addr, *addrlen, __fc_sockfds[sockfd]; assigns __fc_sockfds[sockfd] \from *addr, *addrlen, __fc_sockfds[sockfd]; behavior addr_null: assumes addr_is_null: addr ≡ \null; requires addrlen_should_be_null: addrlen ≡ \null; assigns \result, __fc_sockfds[sockfd]; assigns \result \from __fc_sockfds[sockfd]; assigns __fc_sockfds[sockfd] \from __fc_sockfds[sockfd]; behavior addr_not_null: assumes addr_is_not_null: addr ≢ \null; requires valid_addrlen: \valid(addrlen); requires addr_has_room: \valid((char *)addr + (0 .. *addrlen - 1)); ensures initialization: addr: \initialized((char *)\old(addr) + (0 .. *\old(addrlen) - 1)); disjoint behaviors addr_not_null, addr_null; */ extern int accept(int sockfd, struct sockaddr *addr, socklen_t *addrlen); /*@ requires valid_sockfd: sockfd: 0 ≤ sockfd < 1024; requires valid_read_addr: \valid_read((char *)addr + (0 .. addrlen - 1)); ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1; assigns __fc_sockfds[sockfd], \result; assigns __fc_sockfds[sockfd] \from sockfd, *addr, addrlen, __fc_sockfds[sockfd]; assigns \result \from (indirect: sockfd), (indirect: *addr), (indirect: addrlen), (indirect: __fc_sockfds[sockfd]); */ extern int bind(int sockfd, struct sockaddr const *addr, socklen_t addrlen); /*@ requires valid_sockfd: 0 ≤ sockfd < 1024; requires valid_read_addr: \valid_read((char *)addr + (0 .. addrlen - 1)); ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1; assigns __fc_sockfds[sockfd], \result; assigns __fc_sockfds[sockfd] \from __fc_sockfds[sockfd], (indirect: sockfd), (indirect: addr), (indirect: *addr), (indirect: addrlen); assigns \result \from (indirect: __fc_sockfds[sockfd]), (indirect: sockfd), (indirect: addr), (indirect: *addr), (indirect: addrlen); */ extern int connect(int sockfd, struct sockaddr const *addr, socklen_t addrlen); /*@ requires valid_sockfd: 0 ≤ sockfd < 1024; requires valid_optlen: \valid(optlen); ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1; assigns *((char *)optval + (0 ..)), \result, *optlen; assigns *((char *)optval + (0 ..)) \from (indirect: sockfd), (indirect: level), (indirect: optname), (indirect: *optlen), (indirect: optval), (indirect: __fc_sockfds[sockfd]); assigns \result \from (indirect: sockfd), (indirect: level), (indirect: optname), (indirect: *optlen), (indirect: optval), (indirect: __fc_sockfds[sockfd]); assigns *optlen \from (indirect: sockfd), (indirect: level), (indirect: optname), *optlen, (indirect: optval), (indirect: __fc_sockfds[sockfd]); behavior so_error: assumes optname_is_error: level ≡ 1 ∧ optname ≡ 4; requires valid_optlen: \valid(optlen); requires optlen_value: *optlen ≡ sizeof(int); requires valid_optval: \valid((int *)optval); assigns *((int *)optval), \result; assigns *((int *)optval) \from (indirect: sockfd), (indirect: optlen), (indirect: __fc_sockfds[sockfd]); assigns \result \from (indirect: sockfd), (indirect: optlen), (indirect: __fc_sockfds[sockfd]); behavior other_options: assumes optname_not_error: ¬(level ≡ 1 ∧ optname ≡ 4); requires optval_null_or_valid: optval ≡ \null ∨ \valid((char *)optval + (0 ..)); assigns *((char *)optval + (0 ..)), \result, *optlen; assigns *((char *)optval + (0 ..)) \from (indirect: sockfd), (indirect: level), (indirect: optname), (indirect: *optlen), (indirect: optval), (indirect: __fc_sockfds[sockfd]); assigns \result \from (indirect: sockfd), (indirect: level), (indirect: optname), (indirect: *optlen), (indirect: optval), (indirect: __fc_sockfds[sockfd]); assigns *optlen \from (indirect: sockfd), (indirect: level), (indirect: optname), *optlen, (indirect: optval), (indirect: __fc_sockfds[sockfd]); complete behaviors other_options, so_error; disjoint behaviors other_options, so_error; */ extern int getsockopt(int sockfd, int level, int optname, void *optval, socklen_t *optlen); /*@ requires valid_sockfd: 0 ≤ sockfd < 1024; ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1; assigns \result, __fc_sockfds[sockfd]; assigns \result \from sockfd, __fc_sockfds[sockfd]; assigns __fc_sockfds[sockfd] \from sockfd, backlog, __fc_sockfds[sockfd]; */ extern int listen(int sockfd, int backlog); /*@ requires valid_sockfd: 0 ≤ sockfd < 1024; requires valid_buffer_length: \valid((char *)buf + (0 .. len - 1)); ensures result_error_or_received_length: \result ≡ -1 ∨ (0 ≤ \result ≤ \old(len)); ensures initialization: \initialized((char *)\old(buf) + (0 .. \result - 1)); assigns *((char *)buf + (0 .. len - 1)), __fc_sockfds[sockfd], \result; assigns *((char *)buf + (0 .. len - 1)) \from sockfd, len, flags, __fc_sockfds[sockfd]; assigns __fc_sockfds[sockfd] \from sockfd, len, flags, __fc_sockfds[sockfd]; assigns \result \from sockfd, len, flags, __fc_sockfds[sockfd]; */ extern ssize_t recv(int sockfd, void *buf, size_t len, int flags); /*@ requires valid_sockfd: 0 ≤ sockfd < 1024; requires msg_control_has_room: \valid((char *)hdr->msg_control + (0 .. hdr->msg_controllen - 1)); requires msg_iov_has_room: \valid(hdr->msg_iov + (0 .. hdr->msg_iovlen - 1)); requires msg_name_null_or_has_room: hdr->msg_name ≡ \null ∨ \valid((char *)hdr->msg_name + (0 .. hdr->msg_namelen - 1)); ensures result_error_or_received_length: \result ≡ -1 ∨ (0 ≤ \result ≤ \old(hdr)->msg_iovlen); assigns *((char *)hdr->msg_name + (0 .. hdr->msg_namelen - 1)), hdr->msg_namelen, *((char *)(hdr->msg_iov + (0 .. hdr->msg_iovlen - 1))->iov_base + (0 ..)), *((char *)hdr->msg_control + (0 .. hdr->msg_controllen - 1)), \result, hdr->msg_controllen, hdr->msg_flags, __fc_sockfds[sockfd]; assigns *((char *)hdr->msg_name + (0 .. hdr->msg_namelen - 1)) \from __fc_sockfds[sockfd]; assigns hdr->msg_namelen \from __fc_sockfds[sockfd]; assigns *((char *)(hdr->msg_iov + (0 .. hdr->msg_iovlen - 1))->iov_base + (0 ..)) \from __fc_sockfds[sockfd]; assigns *((char *)hdr->msg_control + (0 .. hdr->msg_controllen - 1)) \from __fc_sockfds[sockfd]; assigns \result \from __fc_sockfds[sockfd]; assigns hdr->msg_controllen \from __fc_sockfds[sockfd]; assigns hdr->msg_flags \from __fc_sockfds[sockfd]; assigns __fc_sockfds[sockfd] \from __fc_sockfds[sockfd]; */ extern ssize_t recvmsg(int sockfd, struct msghdr *hdr, int flags); /*@ requires available_sockfd: 0 ≤ sockfd < 1024; requires buf_len_ok: \valid_read((char *)buf + (0 .. len - 1)); ensures error_or_chars_sent: \result ≡ -1 ∨ (0 ≤ \result ≤ \old(len)); assigns __fc_errno, __fc_sockfds[sockfd], \result; assigns __fc_errno \from (indirect: sockfd), (indirect: __fc_sockfds[sockfd]), (indirect: *((char *)buf + (0 .. len))), flags; assigns __fc_sockfds[sockfd] \from __fc_sockfds[sockfd], *((char *)buf + (0 .. len)), flags; assigns \result \from (indirect: sockfd), (indirect: __fc_sockfds[sockfd]), (indirect: *((char *)buf + (0 .. len))), (indirect: flags); */ extern ssize_t send(int sockfd, void const *buf, size_t len, int flags); /*@ requires valid_sockfd: 0 ≤ sockfd < 1024; requires optval_null_or_has_room: optval ≡ \null ∨ \valid_read((char *)optval + (0 .. optlen - 1)); ensures result_error_or_ok: \result ≡ 0 ∨ \result ≡ -1; assigns \result, __fc_sockfds[sockfd]; assigns \result \from __fc_sockfds[sockfd], level, optname, *((char *)optval + (0 .. optlen - 1)), optlen; assigns __fc_sockfds[sockfd] \from __fc_sockfds[sockfd], level, optname, *((char *)optval + (0 .. optlen - 1)), optlen; */ extern int setsockopt(int sockfd, int level, int optname, void const *optval, socklen_t optlen); /*@ requires valid_sockfd: 0 ≤ sockfd < 1024; ensures result_error_or_ok: \result ≡ 0 ∨ \result ≡ -1; assigns \result, __fc_sockfds[sockfd]; assigns \result \from how, __fc_sockfds[sockfd]; assigns __fc_sockfds[sockfd] \from how, __fc_sockfds[sockfd]; */ extern int shutdown(int sockfd, int how); /*@ ensures result_error_or_valid_new_sockfd: (0 ≤ \result < 1024) ∨ \result ≡ -1; assigns \result, __fc_socket_counter; assigns \result \from (indirect: domain), (indirect: type), (indirect: protocol), (indirect: __fc_socket_counter); assigns __fc_socket_counter \from (indirect: domain), (indirect: type), (indirect: protocol), __fc_socket_counter; */ extern int socket(int domain, int type, int protocol); /*@ requires valid_socket_sector: \valid(sv + (0 .. 1)); ensures result_error_or_ok: \result ≡ 0 ∨ \result ≡ -1; ensures initialization: sv: \initialized(\old(sv) + (0 .. 1)); ensures valid_new_sockfd: sv0: 0 ≤ *(\old(sv) + 0) < 1024; ensures valid_new_sockfd: sv1: 0 ≤ *(\old(sv) + 1) < 1024; assigns \result, __fc_socket_counter, *(sv + (0 .. 1)); assigns \result \from __fc_socket_counter; assigns __fc_socket_counter \from __fc_socket_counter; assigns *(sv + (0 .. 1)) \from __fc_socket_counter; */ extern int socketpair(int domain, int type, int protocol, int * /*[2]*/ sv); struct in6_addr const in6addr_any = {.s6_addr = {(unsigned char)0}}; struct in6_addr const in6addr_loopback = {.s6_addr = {(unsigned char)0xFF, (unsigned char)0xFF, (unsigned char)0xFF, (unsigned char)0xFF, (unsigned char)0xFF, (unsigned char)0xFF, (unsigned char)0xFF, (unsigned char)0xFF, (unsigned char)0xFF, (unsigned char)0xFF, (unsigned char)0xFF, (unsigned char)0xFF, (unsigned char)0xFF, (unsigned char)0xFF, (unsigned char)0xFF, (unsigned char)0xFF}}; /*@ assigns \result; assigns \result \from arg; */ extern uint32_t htonl(uint32_t arg); /*@ assigns \result; assigns \result \from arg; */ extern uint16_t htons(uint16_t arg); /*@ assigns \result; assigns \result \from arg; */ extern uint32_t ntohl(uint32_t arg); /*@ assigns \result; assigns \result \from arg; */ extern uint16_t ntohs(uint16_t arg); /*@ requires valid_arg: valid_read_string(arg); assigns \result; assigns \result \from (indirect: *(arg + (0 ..))); */ extern in_addr_t inet_addr(char const *arg); char volatile __fc_inet_ntoa_array[16]; char *__fc_inet_ntoa = (char *)(__fc_inet_ntoa_array); /*@ ensures result_static_string: \result ≡ __fc_inet_ntoa; ensures result_null_terminated: *(\result + 15) ≡ 0; ensures result_valid_string: valid_read_string(\result); assigns \result, *(__fc_inet_ntoa + (0 ..)); assigns \result \from (indirect: arg), __fc_inet_ntoa; assigns *(__fc_inet_ntoa + (0 ..)) \from (indirect: arg); */ extern char *inet_ntoa(struct in_addr arg); /*@ assigns \result, *(dst + (0 .. size - 1)); assigns \result \from dst, af, *((char *)src + (0 ..)); assigns *(dst + (0 .. size - 1)) \from af, *((char *)src + (0 ..)); */ extern char const *inet_ntop(int af, void const *src, char *dst, socklen_t size); /*@ assigns \result, *((char *)dst + (0 ..)); assigns \result \from af, *(src + (..)); assigns *((char *)dst + (0 ..)) \from af, *(src + (0 ..)); */ extern int inet_pton(int af, char const *src, void *dst); int h_errno; /*@ requires addrinfo_valid: \valid(addrinfo); ensures allocation: \allocable(\old(addrinfo)); assigns \nothing; frees addrinfo; */ extern void freeaddrinfo(struct addrinfo *addrinfo); char *__fc_gai_strerror = (char *)""; /*@ ensures result_string: \result ≡ __fc_gai_strerror; ensures result_valid_string: valid_read_string(\result); assigns \result; assigns \result \from (indirect: errcode), __fc_gai_strerror; */ extern char const *gai_strerror(int errcode); int getaddrinfo(char const * __restrict nodename, char const * __restrict servname, struct addrinfo const * __restrict hints, struct addrinfo ** __restrict res); struct hostent *gethostbyname(char const *name); /*@ predicate non_escaping{L}(void *s, size_t n) = ∀ unsigned int i; 0 ≤ i < n ⇒ ¬\dangling((char *)s + i); */ /*@ predicate empty_block{L}(void *s) = \block_length((char *)s) ≡ 0 ∧ \offset((char *)s) ≡ 0; */ /*@ predicate valid_or_empty{L}(void *s, size_t n) = (empty_block(s) ∨ \valid_read((char *)s)) ∧ \valid((char *)s + (0 .. n - 1)); */ /*@ predicate valid_read_or_empty{L}(void *s, size_t n) = (empty_block(s) ∨ \valid_read((char *)s)) ∧ \valid_read((char *)s + (1 .. n - 1)); */ int memcmp(void const *s1, void const *s2, size_t n); void *memchr(void const *s, int c, size_t n); void *memcpy(void * __restrict dest, void const * __restrict src, size_t n); void *memmove(void *dest, void const *src, size_t n); void *memset(void *s, int c, size_t n); size_t strlen(char const *s); size_t strnlen(char const *s, size_t maxlen); int strcmp(char const *s1, char const *s2); int strncmp(char const *s1, char const *s2, size_t n); /*@ requires valid_string_s1: valid_read_string(s1); requires valid_string_s2: valid_read_string(s2); assigns \result; assigns \result \from (indirect: *(s1 + (0 ..))), (indirect: *(s2 + (0 ..))); */ extern int strcoll(char const *s1, char const *s2); char *strchr(char const *s, int c); char *strrchr(char const *s, int c); /*@ requires valid_string_s: valid_read_string(s); requires valid_string_reject: valid_read_string(reject); ensures result_bounded: 0 ≤ \result ≤ strlen(\old(s)); assigns \result; assigns \result \from (indirect: *(s + (0 ..))), (indirect: *(reject + (0 ..))); */ extern size_t strcspn(char const *s, char const *reject); /*@ requires valid_string_s: valid_read_string(s); requires valid_string_accept: valid_read_string(accept); ensures result_bounded: 0 ≤ \result ≤ strlen(\old(s)); assigns \result, \result; assigns \result \from *(s + (0 ..)), *(accept + (0 ..)); assigns \result \from (indirect: *(s + (0 ..))), (indirect: *(accept + (0 ..))); */ extern size_t strspn(char const *s, char const *accept); /*@ requires valid_string_s: valid_read_string(s); requires valid_string_accept: valid_read_string(accept); ensures result_null_or_same_base: \result ≡ \null ∨ \base_addr(\result) ≡ \base_addr(\old(s)); assigns \result; assigns \result \from s, *(s + (0 ..)), *(accept + (0 ..)); */ extern char *strpbrk(char const *s, char const *accept); char *strstr(char const *haystack, char const *needle); /*@ requires valid_string_haystack: valid_read_string(haystack); requires valid_string_needle: valid_read_string(needle); ensures result_null_or_in_haystack: \result ≡ \null ∨ (\subset(\result, \old(haystack) + (0 ..)) ∧ \valid_read(\result)); assigns \result; assigns \result \from haystack, (indirect: *(haystack + (0 ..))), (indirect: *(needle + (0 ..))); */ extern char *strcasestr(char const *haystack, char const *needle); char *__fc_strtok_ptr; /*@ requires valid_string_delim: valid_read_string(delim); assigns *(s + (0 ..)), *(__fc_strtok_ptr + (0 ..)), \result, __fc_strtok_ptr; assigns *(s + (0 ..)) \from *(s + (0 ..)), (indirect: s), (indirect: __fc_strtok_ptr), (indirect: *(delim + (0 ..))); assigns *(__fc_strtok_ptr + (0 ..)) \from *(__fc_strtok_ptr + (0 ..)), (indirect: s), (indirect: __fc_strtok_ptr), (indirect: *(delim + (0 ..))); assigns \result \from s, __fc_strtok_ptr, (indirect: *(s + (0 ..))), (indirect: *(__fc_strtok_ptr + (0 ..))), (indirect: *(delim + (0 ..))); assigns __fc_strtok_ptr \from \old(__fc_strtok_ptr), s, (indirect: *(__fc_strtok_ptr + (0 ..))), (indirect: *(delim + (0 ..))); behavior new_str: assumes s_not_null: s ≢ \null; requires valid_string_s_or_delim_not_found: valid_string(s) ∨ (valid_read_string(s) ∧ (∀ int i; 0 ≤ i < strlen(delim) ⇒ ¬(strchr(s, *(delim + i)) ≡ \true))); ensures result_subset: \result ≡ \null ∨ \subset(\result, \old(s) + (0 ..)); ensures ptr_subset: \subset(__fc_strtok_ptr, \old(s) + (0 ..)); assigns __fc_strtok_ptr, *(s + (0 ..)), \result; assigns __fc_strtok_ptr \from s, (indirect: *(s + (0 ..))), (indirect: *(delim + (0 ..))); assigns *(s + (0 ..)) \from *(s + (0 ..)), (indirect: s), (indirect: *(delim + (0 ..))); assigns \result \from s, (indirect: *(s + (0 ..))), (indirect: *(delim + (0 ..))); behavior resume_str: assumes s_null: s ≡ \null; requires not_first_call: __fc_strtok_ptr ≢ \null; ensures result_subset: \result ≡ \null ∨ \subset(\result, \old(__fc_strtok_ptr) + (0 ..)); ensures ptr_subset: \subset(__fc_strtok_ptr, \old(__fc_strtok_ptr) + (0 ..)); assigns *(__fc_strtok_ptr + (0 ..)), __fc_strtok_ptr, \result; assigns *(__fc_strtok_ptr + (0 ..)) \from *(__fc_strtok_ptr + (0 ..)), (indirect: __fc_strtok_ptr), (indirect: *(delim + (0 ..))); assigns __fc_strtok_ptr \from \old(__fc_strtok_ptr), (indirect: *(__fc_strtok_ptr + (0 ..))), (indirect: *(delim + (0 ..))); assigns \result \from __fc_strtok_ptr, (indirect: *(__fc_strtok_ptr + (0 ..))), (indirect: *(delim + (0 ..))); complete behaviors resume_str, new_str; disjoint behaviors resume_str, new_str; */ extern char *strtok(char * __restrict s, char const * __restrict delim); /*@ requires valid_string_delim: valid_read_string(delim); requires valid_saveptr: \valid(saveptr); assigns *(s + (0 ..)), *(*saveptr + (0 ..)), \result, *saveptr; assigns *(s + (0 ..)) \from *(s + (0 ..)), (indirect: s), (indirect: *saveptr), (indirect: *(delim + (0 ..))); assigns *(*saveptr + (0 ..)) \from *(*saveptr + (0 ..)), (indirect: s), (indirect: *saveptr), (indirect: *(delim + (0 ..))); assigns \result \from s, *saveptr, (indirect: *(s + (0 ..))), (indirect: *(*saveptr + (0 ..))), (indirect: *(delim + (0 ..))); assigns *saveptr \from \old(*saveptr), s, (indirect: *(*saveptr + (0 ..))), (indirect: *(delim + (0 ..))); behavior new_str: assumes s_not_null: s ≢ \null; requires valid_string_s_or_delim_not_found: valid_string(s) ∨ (valid_read_string(s) ∧ (∀ int i; 0 ≤ i < strlen(delim) ⇒ ¬(strchr(s, *(delim + i)) ≡ \true))); ensures result_subset: \result ≡ \null ∨ \subset(\result, \old(s) + (0 ..)); ensures initialization: \initialized(\old(saveptr)); ensures saveptr_subset: \subset(*\old(saveptr), \old(s) + (0 ..)); assigns *saveptr, *(s + (0 ..)), \result; assigns *saveptr \from s, (indirect: *(s + (0 ..))), (indirect: *(delim + (0 ..))); assigns *(s + (0 ..)) \from *(s + (0 ..)), (indirect: s), (indirect: *(delim + (0 ..))); assigns \result \from s, (indirect: *(s + (0 ..))), (indirect: *(delim + (0 ..))); behavior resume_str: assumes s_null: s ≡ \null; requires not_first_call: *saveptr ≢ \null; requires initialization: saveptr: \initialized(saveptr); ensures result_subset: \result ≡ \null ∨ \subset(\result, \old(*saveptr) + (0 ..)); ensures saveptr_subset: \subset(*\old(saveptr), \old(*saveptr) + (0 ..)); assigns *(*saveptr + (0 ..)), *saveptr, \result; assigns *(*saveptr + (0 ..)) \from *(*saveptr + (0 ..)), (indirect: *saveptr), (indirect: *(delim + (0 ..))); assigns *saveptr \from \old(*saveptr), (indirect: *(*saveptr + (0 ..))), (indirect: *(delim + (0 ..))); assigns \result \from *saveptr, (indirect: *(*saveptr + (0 ..))), (indirect: *(delim + (0 ..))); complete behaviors resume_str, new_str; disjoint behaviors resume_str, new_str; */ extern char *strtok_r(char * __restrict s, char const * __restrict delim, char ** __restrict saveptr); /*@ requires valid_string_stringp: \valid(stringp) ∧ valid_string(*stringp); requires valid_string_delim: valid_read_string(delim); assigns *stringp, \result; assigns *stringp \from *(delim + (..)), *(*(stringp + (..))); assigns \result \from *(delim + (..)), *(*(stringp + (..))); */ extern char *strsep(char **stringp, char const *delim); char __fc_strerror[64]; char * const __fc_p_strerror = __fc_strerror; char *strerror(int errnum); char *strcpy(char *dest, char const *src); char *strncpy(char *dest, char const *src, size_t n); /*@ requires valid_string_src: valid_read_string(src); requires room_nstring: \valid(dest + (0 .. n - 1)); requires separation: \separated( dest + (0 .. n - 1), src + (0 .. \max(n - 1, strlen(src))) ); ensures initialization: \initialized(\old(dest) + (0 .. \min(strlen(\old(src)), \old(n) - 1))); ensures bounded_result: \result ≡ strlen(\old(src)); assigns *(dest + (0 .. n - 1)), \result; assigns *(dest + (0 .. n - 1)) \from *(src + (0 .. n - 1)); assigns \result \from (indirect: src), (indirect: *(src + (0 .. n - 1))), (indirect: n); */ size_t strlcpy(char * __restrict dest, char const * __restrict src, size_t n); /*@ requires valid_string_src: valid_read_string(src); requires room_string: \valid(dest + (0 .. strlen(src))); requires separation: \separated(dest + (0 .. strlen(src)), src + (0 .. strlen(src))); ensures equal_contents: strcmp(\old(dest), \old(src)) ≡ 0; ensures points_to_end: \result ≡ \old(dest) + strlen(\old(dest)); assigns *(dest + (0 .. strlen{Old}(src))), \result; assigns *(dest + (0 .. strlen{Old}(src))) \from *(src + (0 .. strlen{Old}(src))); assigns \result \from dest; */ extern char *stpcpy(char * __restrict dest, char const * __restrict src); char *strcat(char *dest, char const *src); char *strncat(char *dest, char const *src, size_t n); /*@ requires valid_string_src: valid_read_string(src); requires valid_string_dest: valid_string(dest); requires room_nstring: \valid(dest + (0 .. n - 1)); ensures bounded_result: \result ≡ strlen(\old(dest)) + strlen(\old(src)); assigns *(dest + (strlen{Old}(dest) .. n)), \result; assigns *(dest + (strlen{Old}(dest) .. n)) \from (indirect: n), *(src + (0 .. strlen{Old}(src))); assigns \result \from (indirect: src), (indirect: *(src + (0 .. n - 1))), (indirect: n); */ extern size_t strlcat(char * __restrict dest, char const * __restrict src, size_t n); /*@ requires valid_dest: \valid(dest + (0 .. n - 1)); requires valid_string_src: valid_read_string(src); assigns *(dest + (0 .. n - 1)), \result; assigns *(dest + (0 .. n - 1)) \from (indirect: *(src + (0 ..))), (indirect: n); assigns \result \from dest; */ extern size_t strxfrm(char * __restrict dest, char const * __restrict src, size_t n); char *strdup(char const *s); char *strndup(char const *s, size_t n); char __fc_strsignal[64]; char * const __fc_p_strsignal = __fc_strsignal; char *strsignal(int signum); /*@ requires valid_memory_area: \valid((char *)s + (0 .. n - 1)); ensures s_initialized: initialization: \initialized((char *)\old(s) + (0 .. \old(n) - 1)); ensures zero_initialized: \subset(*((char *)\old(s) + (0 .. \old(n) - 1)), {0}); assigns *((char *)s + (0 .. n - 1)); assigns *((char *)s + (0 .. n - 1)) \from \nothing; */ extern void bzero(void *s, size_t n); int strcasecmp(char const *s1, char const *s2); /*@ requires valid_string_s1: valid_read_nstring(s1, n); requires valid_string_s2: valid_read_nstring(s2, n); assigns \result; assigns \result \from (indirect: n), (indirect: *(s1 + (0 .. n - 1))), (indirect: *(s2 + (0 .. n - 1))); */ extern int strncasecmp(char const *s1, char const *s2, size_t n); static unsigned int volatile getaddrinfo_net_state; /*@ requires nodename_string: nodename ≡ \null ∨ valid_read_string(nodename); requires servname_string: servname ≡ \null ∨ valid_read_string(servname); requires hints_option: hints ≡ \null ∨ \valid_read(hints); requires valid_res: \valid(res); assigns *res, \result, __fc_errno; assigns *res \from (indirect: nodename), (indirect: servname), (indirect: hints); assigns \result \from (indirect: nodename), (indirect: servname), (indirect: hints); assigns __fc_errno \from (indirect: nodename), (indirect: servname), (indirect: hints); allocates *\old(res); behavior empty_request: assumes empty: nodename ≡ \null ∧ servname ≡ \null; ensures no_name: \result ≡ -2; assigns \result; assigns \result \from (indirect: nodename), (indirect: servname); behavior normal_request: assumes has_name: nodename ≢ \null ∨ servname ≢ \null; ensures initialization: allocation: success_or_error: (\result ≡ 0 ∧ \fresh{Old, Here}(*\old(res),sizeof(*\old(res))) ∧ \initialized(*\old(res))) ∨ \result ≡ -3 ∨ \result ≡ -1 ∨ \result ≡ -4 ∨ \result ≡ -6 ∨ \result ≡ -10 ∨ \result ≡ -8 ∨ \result ≡ -7 ∨ \result ≡ -11; complete behaviors normal_request, empty_request; disjoint behaviors normal_request, empty_request; */ int getaddrinfo(char const * __restrict nodename, char const * __restrict servname, struct addrinfo const * __restrict hints, struct addrinfo ** __restrict res) { int __retres; if (nodename == (char const *)0) if (servname == (char const *)0) { __retres = -2; goto return_label; } switch (getaddrinfo_net_state) { case (unsigned int)0: __retres = -1; goto return_label; case (unsigned int)1: __retres = -3; goto return_label; case (unsigned int)2: __retres = -4; goto return_label; case (unsigned int)3: __retres = -6; goto return_label; case (unsigned int)5: __retres = -8; goto return_label; case (unsigned int)6: __retres = -7; goto return_label; case (unsigned int)7: { __fc_errno = 5; __retres = -11; goto return_label; } default: { struct addrinfo *tmp_0; struct sockaddr *tmp_2; int tmp_3; struct addrinfo *ai = malloc(sizeof(*tmp_0)); if (! ai) { __retres = -10; goto return_label; } struct sockaddr *sa = malloc(sizeof(*tmp_2)); if (! sa) { __retres = -10; goto return_label; } tmp_3 = Frama_C_interval(0,43); sa->sa_family = (unsigned short)tmp_3; /*@ slevel 15; */ { int i = 0; while (i < 14) { { int tmp_4; tmp_4 = Frama_C_interval(-128,127); sa->sa_data[i] = (char)tmp_4; } i ++; } } /*@ slevel default; */ ai->ai_flags = 0; ai->ai_family = (int)sa->sa_family; ai->ai_socktype = Frama_C_interval(0,5); ai->ai_protocol = Frama_C_interval(0,IPPROTO_MAX); ai->ai_addrlen = sizeof(*sa); ai->ai_addr = sa; ai->ai_canonname = (char *)"dummy"; ai->ai_next = (struct addrinfo *)0; *res = ai; __retres = 0; goto return_label; } } return_label: return __retres; } struct __fc_gethostbyname __fc_ghbn; int res_search(char const *dname, int class, int type, char *answer, int anslen) { int tmp; { int i = 0; while (i < anslen - 1) { *(answer + i) = Frama_C_char_interval((char)(-128),(char)127); i ++; } } *(answer + (anslen - 1)) = (char)0; tmp = Frama_C_interval(-1,anslen); return tmp; } struct hostent *gethostbyname(char const *name) { struct hostent *__retres; char buf[128]; char const *cp; int n; int tmp; __fc_ghbn.host.h_addrtype = 2; __fc_ghbn.host.h_length = (int)sizeof(struct in_addr); if ((int)*name >= '0') if ((int)*name <= '9') { cp = name; while (1) { if (! *cp) { struct in_addr addr; cp --; ; if ((int)*cp == '.') break; addr.s_addr = inet_addr(name); if (addr.s_addr == 0xffffffff) { __retres = (struct hostent *)0; goto return_label; } memcpy((void *)(__fc_ghbn.host_addr),(void const *)(& addr), (unsigned int)__fc_ghbn.host.h_length); strncpy(__fc_ghbn.hostbuf,name,(unsigned int)(128 - 1)); __fc_ghbn.hostbuf[128 - 1] = (char)'\000'; __fc_ghbn.host.h_name = __fc_ghbn.hostbuf; __fc_ghbn.host.h_aliases = __fc_ghbn.host_aliases; __fc_ghbn.host_aliases[0] = (char *)0; __fc_ghbn.h_addr_ptrs[0] = (char *)(__fc_ghbn.host_addr); __fc_ghbn.h_addr_ptrs[1] = (char *)0; __fc_ghbn.host.h_addr_list = __fc_ghbn.h_addr_ptrs; __retres = & __fc_ghbn.host; goto return_label; } if ((int)*cp < '0') if ((int)*cp > '9') if ((int)*cp != '.') break; cp ++; } } n = res_search(name,1,1,buf,(int)sizeof(buf)); if (n < 0) { __retres = (struct hostent *)0; goto return_label; } tmp = Frama_C_nondet(0,1); if (tmp) { __retres = (struct hostent *)0; goto return_label; } else { struct in_addr addr_0; addr_0.s_addr = inet_addr(name); memcpy((void *)(__fc_ghbn.host_addr),(void const *)(& addr_0), (unsigned int)__fc_ghbn.host.h_length); strncpy(__fc_ghbn.hostbuf,name,(unsigned int)(128 - 1)); __fc_ghbn.hostbuf[128 - 1] = (char)'\000'; __fc_ghbn.host.h_name = __fc_ghbn.hostbuf; __fc_ghbn.host.h_aliases = __fc_ghbn.host_aliases; __fc_ghbn.host_aliases[0] = (char *)0; __fc_ghbn.h_addr_ptrs[0] = (char *)(__fc_ghbn.host_addr); __fc_ghbn.h_addr_ptrs[1] = (char *)0; __fc_ghbn.host.h_addr_list = __fc_ghbn.h_addr_ptrs; __retres = & __fc_ghbn.host; goto return_label; } return_label: return __retres; } FILE *__fc_stderr; FILE *__fc_stdin; FILE *__fc_stdout; /*@ requires valid_filename: valid_read_string(filename); ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1; assigns \result; assigns \result \from (indirect: *(filename + (0 .. strlen{Old}(filename)))); */ extern int remove(char const *filename); /*@ requires valid_old_name: valid_read_string(old_name); requires valid_new_name: valid_read_string(new_name); ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1; assigns \result; assigns \result \from (indirect: *(old_name + (0 .. strlen{Old}(old_name)))), (indirect: *(new_name + (0 .. strlen{Old}(new_name)))); */ extern int rename(char const *old_name, char const *new_name); FILE __fc_fopen[16]; FILE * const __fc_p_fopen = __fc_fopen; /*@ ensures result_null_or_valid_fd: \result ≡ \null ∨ \subset(\result, &__fc_fopen[0 .. 16 - 1]); assigns \result; assigns \result \from __fc_p_fopen; */ extern FILE *tmpfile(void); char __fc_tmpnam[2048]; char * const __fc_p_tmpnam = __fc_tmpnam; /*@ requires valid_s_or_null: s ≡ \null ∨ \valid(s + (0 .. 2048)); ensures result_string_or_null: \result ≡ \null ∨ \result ≡ \old(s) ∨ \result ≡ __fc_p_tmpnam; assigns *(__fc_p_tmpnam + (0 .. 2048)), *(s + (0 .. 2048)), \result; assigns *(__fc_p_tmpnam + (0 .. 2048)) \from *(__fc_p_tmpnam + (0 .. 2048)), (indirect: s); assigns *(s + (0 .. 2048)) \from (indirect: s), *(__fc_p_tmpnam + (0 .. 2048)); assigns \result \from s, __fc_p_tmpnam; */ extern char *tmpnam(char *s); /*@ requires valid_stream: \valid(stream); ensures result_zero_or_EOF: \result ≡ 0 ∨ \result ≡ -1; assigns \result; assigns \result \from (indirect: stream), (indirect: *stream); */ extern int fclose(FILE *stream); /*@ requires null_or_valid_stream: stream ≡ \null ∨ \valid_read(stream); ensures result_zero_or_EOF: \result ≡ 0 ∨ \result ≡ -1; assigns \result, *stream, __fc_fopen[0 .. 16 - 1]; assigns \result \from (indirect: *stream), (indirect: __fc_fopen[0 .. 16 - 1]); assigns *stream \from (indirect: stream), *stream, __fc_fopen[0 .. 16 - 1]; assigns __fc_fopen[0 .. 16 - 1] \from (indirect: stream), *stream, __fc_fopen[0 .. 16 - 1]; behavior flush_all: assumes all_streams: stream ≡ \null; assigns __fc_fopen[0 .. 16 - 1], \result; assigns __fc_fopen[0 .. 16 - 1] \from __fc_fopen[0 .. 16 - 1]; assigns \result \from (indirect: __fc_fopen[0 .. 16 - 1]); behavior flush_stream: assumes single_stream: stream ≢ \null; assigns *stream, \result; assigns *stream \from *stream; assigns \result \from (indirect: *stream); complete behaviors flush_stream, flush_all; disjoint behaviors flush_stream, flush_all; */ extern int fflush(FILE *stream); /*@ requires valid_filename: valid_read_string(filename); requires valid_mode: valid_read_string(mode); ensures result_null_or_valid_fd: \result ≡ \null ∨ \subset(\result, &__fc_fopen[0 .. 16 - 1]); assigns \result; assigns \result \from (indirect: *(filename + (0 .. strlen{Old}(filename)))), (indirect: *(mode + (0 .. strlen{Old}(mode)))), __fc_p_fopen; */ extern FILE *fopen(char const * __restrict filename, char const * __restrict mode); /*@ requires valid_mode: valid_read_string(mode); ensures result_null_or_valid_fd: \result ≡ \null ∨ \subset(\result, &__fc_fopen[0 .. 16 - 1]); assigns \result, __fc_fopen[fd]; assigns \result \from (indirect: fd), (indirect: *(mode + (0 .. strlen{Old}(mode)))), (indirect: __fc_fopen[fd]), __fc_p_fopen; assigns __fc_fopen[fd] \from (indirect: fd), (indirect: *(mode + (0 .. strlen{Old}(mode)))), (indirect: __fc_fopen[fd]), __fc_p_fopen; */ extern FILE *fdopen(int fd, char const *mode); /*@ requires valid_filename: valid_read_string(filename); requires valid_mode: valid_read_string(mode); requires valid_stream: \valid(stream); ensures result_null_or_valid_fd: \result ≡ \null ∨ \result ∈ &__fc_fopen[0 .. 16 - 1]; ensures stream_opened: *\old(stream) ∈ __fc_fopen[0 .. 16 - 1]; assigns \result, *stream; assigns \result \from (indirect: *(filename + (..))), (indirect: *(mode + (..))), __fc_p_fopen, (indirect: stream); assigns *stream \from (indirect: *(filename + (..))), (indirect: *(mode + (..))), __fc_p_fopen, (indirect: stream); */ extern FILE *freopen(char const * __restrict filename, char const * __restrict mode, FILE * __restrict stream); /*@ assigns *stream; assigns *stream \from buf; */ extern void setbuf(FILE * __restrict stream, char * __restrict buf); /*@ assigns *stream; assigns *stream \from buf, mode, size; */ extern int setvbuf(FILE * __restrict stream, char * __restrict buf, int mode, size_t size); /*@ axiomatic format_length { logic ℤ format_length{L}(char *format) ; } */ /*@ assigns *stream; assigns *stream \from *(format + (..)), arg; */ extern int vfprintf(FILE * __restrict stream, char const * __restrict format, va_list arg); /*@ assigns *stream; assigns *stream \from *(format + (..)), *stream; */ extern int vfscanf(FILE * __restrict stream, char const * __restrict format, va_list arg); /*@ assigns *__fc_stdout; assigns *__fc_stdout \from arg; */ extern int vprintf(char const * __restrict format, va_list arg); /*@ assigns *__fc_stdin; assigns *__fc_stdin \from *(format + (..)); */ extern int vscanf(char const * __restrict format, va_list arg); /*@ assigns *(s + (0 .. n - 1)); assigns *(s + (0 .. n - 1)) \from *(format + (..)), arg; */ extern int vsnprintf(char * __restrict s, size_t n, char const * __restrict format, va_list arg); /*@ assigns *(s + (0 ..)); assigns *(s + (0 ..)) \from *(format + (..)), arg; */ extern int vsprintf(char * __restrict s, char const * __restrict format, va_list arg); /*@ requires valid_stream: \valid(stream); ensures result_uchar_or_eof: (0 ≤ \result ≤ 255) ∨ \result ≡ -1; assigns *stream, \result; assigns *stream \from *stream; assigns \result \from (indirect: *stream); */ extern int fgetc(FILE *stream); /*@ requires valid_stream: \valid(stream); requires room_s: \valid(s + (0 .. size - 1)); ensures result_null_or_same: \result ≡ \null ∨ \result ≡ \old(s); ensures initialization: at_least_one: \result ≢ \null ⇒ \initialized(\old(s) + 0); ensures terminated_string_on_success: \result ≢ \null ⇒ valid_string(\old(s)); assigns *(s + (0 .. size - 1)), \result; assigns *(s + (0 .. size - 1)) \from (indirect: size), (indirect: *stream); assigns \result \from s, (indirect: size), (indirect: *stream); */ extern char *fgets(char * __restrict s, int size, FILE * __restrict stream); /*@ requires valid_stream: \valid(stream); assigns *stream, \result; assigns *stream \from c, *stream; assigns \result \from (indirect: *stream); */ extern int fputc(int c, FILE *stream); /*@ requires valid_string_s: valid_read_string(s); assigns *stream, \result; assigns *stream \from *(s + (0 .. strlen{Old}(s))), *stream; assigns \result \from (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: *stream); */ extern int fputs(char const * __restrict s, FILE * __restrict stream); /*@ requires valid_stream: \valid(stream); assigns \result, *stream; assigns \result \from *stream; assigns *stream \from *stream; */ extern int getc(FILE *stream); /*@ assigns \result, *__fc_stdin; assigns \result \from *__fc_stdin; assigns *__fc_stdin \from *__fc_stdin; */ extern int getchar(void); /*@ axiomatic GetsLength { logic size_t gets_length{L} reads *__fc_stdin; } */ /*@ requires room_s: \valid(s + (0 .. gets_length)); ensures result_null_or_same: \result ≡ \old(s) ∨ \result ≡ \null; assigns *(s + (0 .. gets_length{Old})), \result, *__fc_stdin; assigns *(s + (0 .. gets_length{Old})) \from *__fc_stdin; assigns \result \from s, *__fc_stdin; assigns *__fc_stdin \from *__fc_stdin; */ extern char *gets(char *s); /*@ requires valid_stream: \valid(stream); assigns *stream, \result; assigns *stream \from c, *stream; assigns \result \from (indirect: *stream); */ extern int putc(int c, FILE *stream); /*@ assigns *__fc_stdout, \result; assigns *__fc_stdout \from c, *__fc_stdout; assigns \result \from (indirect: *__fc_stdout); */ extern int putchar(int c); /*@ requires valid_string_s: valid_read_string(s); assigns *__fc_stdout, \result; assigns *__fc_stdout \from *(s + (0 .. strlen{Old}(s))), *__fc_stdout; assigns \result \from (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: *__fc_stdout); */ extern int puts(char const *s); /*@ requires valid_stream: \valid(stream); ensures result_ok_or_error: \result ≡ \old(c) ∨ \result ≡ -1; assigns *stream, \result; assigns *stream \from (indirect: c); assigns \result \from (indirect: c), (indirect: *stream); */ extern int ungetc(int c, FILE *stream); /*@ requires valid_ptr_block: \valid((char *)ptr + (0 .. nmemb * size - 1)); requires valid_stream: \valid(stream); ensures size_read: \result ≤ \old(nmemb); ensures initialization: \initialized((char *)\old(ptr) + (0 .. \result * \old(size) - 1)); assigns *((char *)ptr + (0 .. nmemb * size - 1)), *stream, \result; assigns *((char *)ptr + (0 .. nmemb * size - 1)) \from (indirect: size), (indirect: nmemb), (indirect: *stream); assigns *stream \from (indirect: size), (indirect: nmemb), (indirect: *stream); assigns \result \from size, (indirect: *stream); */ extern size_t fread(void * __restrict ptr, size_t size, size_t nmemb, FILE * __restrict stream); /*@ requires valid_ptr_block: \valid_read((char *)ptr + (0 .. nmemb * size - 1)); requires valid_stream: \valid(stream); ensures size_written: \result ≤ \old(nmemb); assigns *stream, \result; assigns *stream \from (indirect: *((char *)ptr + (0 .. nmemb * size - 1))); assigns \result \from (indirect: *((char *)ptr + (0 .. nmemb * size - 1))); */ extern size_t fwrite(void const * __restrict ptr, size_t size, size_t nmemb, FILE * __restrict stream); /*@ requires valid_stream: \valid(stream); requires valid_pos: \valid(pos); requires initialization: pos: \initialized(pos); assigns *pos, \result; assigns *pos \from (indirect: *stream); assigns \result \from (indirect: *stream); */ extern int fgetpos(FILE * __restrict stream, fpos_t * __restrict pos); /*@ requires valid_stream: \valid(stream); requires whence_enum: whence ≡ 0 ∨ whence ≡ 1 ∨ whence ≡ 2; assigns *stream, \result, __fc_errno; assigns *stream \from *stream, (indirect: offset), (indirect: whence); assigns \result \from (indirect: *stream), (indirect: offset), (indirect: whence); assigns __fc_errno \from (indirect: *stream), (indirect: offset), (indirect: whence); */ extern int fseek(FILE *stream, long offset, int whence); /*@ requires valid_stream: \valid(stream); requires valid_pos: \valid_read(pos); requires initialization: pos: \initialized(pos); assigns *stream; assigns *stream \from *pos; */ extern int fsetpos(FILE *stream, fpos_t const *pos); /*@ requires valid_stream: \valid(stream); ensures success_or_error: \result ≡ -1 ∨ (\result ≥ 0 ∧ __fc_errno ≡ \old(__fc_errno)); assigns \result, __fc_errno; assigns \result \from (indirect: *stream); assigns __fc_errno \from (indirect: *stream); */ extern long ftell(FILE *stream); /*@ requires valid_stream: \valid(stream); assigns *stream; assigns *stream \from \nothing; */ extern void rewind(FILE *stream); /*@ requires valid_stream: \valid(stream); assigns *stream; assigns *stream \from \nothing; */ extern void clearerr(FILE *stream); /*@ requires valid_stream: \valid(stream); assigns \result; assigns \result \from (indirect: *stream); */ extern int feof(FILE *stream); /*@ requires valid_stream: \valid(stream); assigns \result; assigns \result \from (indirect: *stream); */ extern int fileno(FILE *stream); /*@ requires valid_stream: \valid(stream); assigns *stream; assigns *stream \from \nothing; */ extern void flockfile(FILE *stream); /*@ requires valid_stream: \valid(stream); assigns *stream; assigns *stream \from \nothing; */ extern void funlockfile(FILE *stream); /*@ requires valid_stream: \valid(stream); assigns \result, *stream; assigns \result \from \nothing; assigns *stream \from \nothing; */ extern int ftrylockfile(FILE *stream); /*@ requires valid_stream: \valid(stream); assigns \result; assigns \result \from (indirect: *stream); */ extern int ferror(FILE *stream); /*@ requires valid_string_s: valid_read_string(s); assigns __fc_stdout; assigns __fc_stdout \from __fc_errno, *(s + (0 .. strlen{Old}(s))); */ extern void perror(char const *s); /*@ requires valid_stream: \valid(stream); assigns \result, *stream; assigns \result \from *stream; assigns *stream \from *stream; */ extern int getc_unlocked(FILE *stream); /*@ assigns \result; assigns \result \from *__fc_stdin; */ extern int getchar_unlocked(void); /*@ requires valid_stream: \valid(stream); assigns *stream, \result; assigns *stream \from c; assigns \result \from (indirect: *stream); */ extern int putc_unlocked(int c, FILE *stream); /*@ assigns *__fc_stdout, \result; assigns *__fc_stdout \from c; assigns \result \from (indirect: *__fc_stdout); */ extern int putchar_unlocked(int c); /*@ requires valid_stream: \valid(stream); assigns *stream; assigns *stream \from \nothing; */ extern void clearerr_unlocked(FILE *stream); /*@ requires valid_stream: \valid(stream); assigns \result; assigns \result \from (indirect: *stream); */ extern int feof_unlocked(FILE *stream); /*@ requires valid_stream: \valid(stream); assigns \result; assigns \result \from (indirect: *stream); */ extern int ferror_unlocked(FILE *stream); /*@ requires valid_stream: \valid(stream); assigns \result; assigns \result \from (indirect: *stream); */ extern int fileno_unlocked(FILE *stream); /*@ axiomatic pipe_streams { predicate is_open_pipe{L}(FILE *stream) ; } */ /*@ requires valid_command: valid_read_string(command); requires valid_type: valid_read_string(type); ensures result_error_or_valid_open_pipe: \result ≡ \null ∨ (\subset(\result, &__fc_fopen[0 .. 16 - 1]) ∧ is_open_pipe(\result)); assigns \result, __fc_fopen[0 ..]; assigns \result \from (indirect: *command), (indirect: *type), __fc_p_fopen; assigns __fc_fopen[0 ..] \from (indirect: *command), (indirect: *type), __fc_fopen[0 ..]; */ extern FILE *popen(char const *command, char const *type); /*@ requires valid_stream: \valid(stream); requires open_pipe: is_open_pipe(stream); ensures closed_stream: ¬is_open_pipe(\old(stream)); assigns \result; assigns \result \from (indirect: *stream); */ extern int pclose(FILE *stream); ssize_t getline(char **lineptr, size_t *n, FILE *stream); FILE __fc_initial_stdout = {.__fc_FILE_id = (unsigned int)1, .__fc_FILE_data = 0U}; FILE *__fc_stdout = & __fc_initial_stdout; FILE __fc_initial_stderr = {.__fc_FILE_id = (unsigned int)2, .__fc_FILE_data = 0U}; FILE *__fc_stderr = & __fc_initial_stderr; FILE __fc_initial_stdin = {.__fc_FILE_id = (unsigned int)0, .__fc_FILE_data = 0U}; FILE *__fc_stdin = & __fc_initial_stdin; ssize_t getline(char **lineptr, size_t *n, FILE *stream) { ssize_t __retres; int tmp; if (! lineptr) goto _LOR; else if (! n) goto _LOR; else if (! stream) { _LOR: { __fc_errno = 22; __retres = -1; goto return_label; } } tmp = ferror(stream); if (tmp) goto _LOR_0; else { int tmp_0; tmp_0 = feof(stream); if (tmp_0) { _LOR_0: { __retres = -1; goto return_label; } } } if (! *lineptr) goto _LOR_1; else if (*n == (size_t)0) { _LOR_1: { *lineptr = (char *)malloc((unsigned int)2); if (! lineptr) { __fc_errno = 12; __retres = -1; goto return_label; } *n = (unsigned int)2; } } size_t cur = (unsigned int)0; while (1) { int tmp_3; tmp_3 = ferror(stream); if (tmp_3) break; else { int tmp_4; tmp_4 = feof(stream); if (tmp_4) break; } { while (cur < *n - (size_t)1) { int tmp_1; tmp_1 = fgetc(stream); char c = (char)tmp_1; if ((int)c == -1) if (cur == (size_t)0) { __retres = -1; goto return_label; } if ((int)c != -1) { size_t tmp_2; tmp_2 = cur; cur += (size_t)1; *(*lineptr + tmp_2) = c; } if ((int)c == '\n') goto _LOR_2; else if ((int)c == -1) { _LOR_2: { *(*lineptr + cur) = (char)'\000'; __retres = (int)cur; goto return_label; } } } if (*n == (size_t)2147483647) { __fc_errno = 75; __retres = -1; goto return_label; } size_t new_size = *n + (size_t)1; *lineptr = (char *)realloc((void *)*lineptr,new_size); if (! *lineptr) { __fc_errno = 12; __retres = -1; goto return_label; } *n = new_size; } } __retres = -1; return_label: return __retres; } /*@ requires abs_representable: i > -2147483647 - 1; assigns \result; assigns \result \from i; behavior negative: assumes negative: i < 0; ensures opposite_result: \result ≡ -\old(i); behavior nonnegative: assumes nonnegative: i ≥ 0; ensures same_result: \result ≡ \old(i); complete behaviors nonnegative, negative; disjoint behaviors nonnegative, negative; */ int abs(int i) { int __retres; if (i < 0) { __retres = - i; goto return_label; } __retres = i; return_label: return __retres; } /*@ requires valid_nptr: \valid_read(p); assigns \result; assigns \result \from (indirect: p), (indirect: *(p + (0 ..))); */ int atoi(char const *p) { int __retres; int n; int c; int tmp_1; int tmp_3; int neg = 0; unsigned char *up = (unsigned char *)p; c = (int)*up; tmp_1 = isdigit(c); if (! tmp_1) { int tmp_0; while (1) { int tmp; tmp = isspace(c); if (! tmp) break; up ++; c = (int)*up; } switch (c) { case '-': neg ++; case '+': { /* sequence */ up ++; c = (int)*up; } } tmp_0 = isdigit(c); if (! tmp_0) { __retres = 0; goto return_label; } } n = '0' - c; while (1) { int tmp_2; up ++; c = (int)*up; tmp_2 = isdigit(c); if (! tmp_2) break; n *= 10; n += '0' - c; } if (neg) tmp_3 = n; else tmp_3 = - n; __retres = tmp_3; return_label: return __retres; } /*@ assigns __fc_heap_status, \result; assigns __fc_heap_status \from (indirect: nmemb), (indirect: size), __fc_heap_status; assigns \result \from (indirect: nmemb), (indirect: size), (indirect: __fc_heap_status); allocates \result; behavior allocation: assumes can_allocate: is_allocable(nmemb * size); ensures allocation: \fresh{Old, Here}(\result,\old(nmemb) * \old(size)); ensures initialization: \initialized((char *)\result + (0 .. \old(nmemb) * \old(size) - 1)); ensures zero_initialization: \subset(*((char *)\result + (0 .. \old(nmemb) * \old(size) - 1)), {0}); behavior no_allocation: assumes cannot_allocate: ¬is_allocable(nmemb * size); ensures null_result: \result ≡ \null; assigns \result; assigns \result \from \nothing; allocates \nothing; complete behaviors no_allocation, allocation; disjoint behaviors no_allocation, allocation; */ void *calloc(size_t nmemb, size_t size) { void *__retres; size_t l = nmemb * size; if (size != (size_t)0) if (l / size != nmemb) { __retres = (void *)0; goto return_label; } char *p = malloc(l); if (p) memset((void *)p,0,l); __retres = (void *)p; return_label: return __retres; } static char __fc_env_strings[64]; static char __fc_initenv_init; static void __fc_initenv(void) { if (! __fc_initenv_init) { Frama_C_make_unknown(__fc_env_strings,(unsigned int)(64 - 1)); { int i = 0; while (i < 4096) { { int tmp; tmp = Frama_C_interval(0,64 - 1); __fc_env[i] = & __fc_env_strings[tmp]; } i ++; } } __fc_initenv_init = (char)1; } return; } /*@ requires valid_name: valid_read_string(name); ensures null_or_valid_result: \result ≡ \null ∨ \valid(\result); assigns \result; assigns \result \from __fc_env[0 ..], (indirect: name), *(name + (0 ..)); */ char *getenv(char const *name) { char *__retres; int tmp_0; /*@ assert ¬(strchr(name, '=') ≡ \true); */ ; __fc_initenv(); tmp_0 = Frama_C_nondet(0,1); if (tmp_0) { int tmp; tmp = Frama_C_interval(0,4096 - 1); ; __retres = __fc_env[tmp]; goto return_label; } else { __retres = (char *)0; goto return_label; } return_label: return __retres; } /*@ requires valid_string: valid_read_string(string); assigns __fc_env[0 ..], \result; assigns __fc_env[0 ..] \from __fc_env[0 ..], string; assigns \result \from (indirect: __fc_env[0 ..]), (indirect: string); */ int putenv(char *string) { int __retres; int tmp_3; char *separator = strchr((char const *)string,'='); /*@ assert string_contains_separator: separator ≢ \null; */ ; /*@ assert name_is_not_empty: separator ≢ string; */ ; __fc_initenv(); tmp_3 = Frama_C_nondet(0,1); if (tmp_3) { int tmp_1; int tmp_2; tmp_1 = Frama_C_nondet(0,1); if (tmp_1) { int tmp_0; tmp_0 = Frama_C_interval(-2147483647 - 1,2147483647); __retres = tmp_0; goto return_label; } tmp_2 = Frama_C_interval(0,4096 - 1); __fc_env[tmp_2] = string; } __retres = 0; return_label: return __retres; } /*@ requires valid_name: valid_read_string(name); requires valid_value: valid_read_string(value); ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1; assigns \result, __fc_env[0 ..]; assigns \result \from __fc_env[0 ..], (indirect: name), (indirect: *(name + (0 ..))), (indirect: value), (indirect: *(value + (0 ..))), (indirect: overwrite); assigns __fc_env[0 ..] \from __fc_env[0 ..], (indirect: name), (indirect: *(name + (0 ..))), (indirect: value), (indirect: *(value + (0 ..))), (indirect: overwrite); */ int setenv(char const *name, char const *value, int overwrite) { int __retres; char *tmp; int tmp_4; tmp = strchr(name,'='); if (tmp) { __retres = -1; goto return_label; } size_t namelen = strlen(name); if (namelen == (size_t)0) { __retres = -1; goto return_label; } __fc_initenv(); tmp_4 = Frama_C_nondet(0,1); if (tmp_4) { __retres = -1; goto return_label; } else { int tmp_1; int tmp_2; int tmp_3; tmp_1 = Frama_C_nondet(0,1); if (tmp_1) Frama_C_make_unknown(__fc_env_strings,(unsigned int)(64 - 1)); tmp_2 = Frama_C_interval(0,4096 - 1); tmp_3 = Frama_C_interval(0,64 - 1); __fc_env[tmp_2] = & __fc_env_strings[tmp_3]; __retres = 0; goto return_label; } return_label: return __retres; } /*@ requires valid_name: valid_read_string(name); ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1; assigns \result, __fc_env[0 ..]; assigns \result \from __fc_env[0 ..], (indirect: name), (indirect: *(name + (0 ..))); assigns __fc_env[0 ..] \from __fc_env[0 ..], (indirect: name), (indirect: *(name + (0 ..))); */ int unsetenv(char const *name) { int __retres; char *tmp; int tmp_2; tmp = strchr(name,'='); if (tmp) { __retres = -1; goto return_label; } size_t namelen = strlen(name); if (namelen == (size_t)0) { __retres = -1; goto return_label; } __fc_initenv(); tmp_2 = Frama_C_nondet(0,1); if (tmp_2) { int tmp_1; tmp_1 = Frama_C_interval(0,4096 - 1); __fc_env[tmp_1] = (char *)0; } __retres = 0; return_label: return __retres; } /*@ requires valid_memptr: \valid(memptr); requires alignment_is_a_suitable_power_of_two: alignment ≥ sizeof(void *) ∧ ((size_t)alignment & ((size_t)alignment - 1)) ≡ 0; assigns __fc_heap_status, \result; assigns __fc_heap_status \from (indirect: alignment), size, __fc_heap_status; assigns \result \from (indirect: alignment), (indirect: size), (indirect: __fc_heap_status); allocates *\old(memptr); behavior allocation: assumes can_allocate: is_allocable(size); ensures allocation: \fresh{Old, Here}(*\old(memptr),\old(size)); ensures result_zero: \result ≡ 0; assigns __fc_heap_status, \result; assigns __fc_heap_status \from (indirect: alignment), size, __fc_heap_status; assigns \result \from (indirect: alignment), (indirect: size), (indirect: __fc_heap_status); behavior no_allocation: assumes cannot_allocate: ¬is_allocable(size); ensures result_non_zero: \result < 0 ∨ \result > 0; assigns \result; assigns \result \from (indirect: alignment); allocates \nothing; complete behaviors no_allocation, allocation; disjoint behaviors no_allocation, allocation; */ int posix_memalign(void **memptr, size_t alignment, size_t size) { int __retres; /*@ assert alignment_is_a_suitable_power_of_two: alignment ≥ sizeof(void *) ∧ ((size_t)alignment & ((size_t)alignment - 1)) ≡ 0; */ ; *memptr = malloc(size); if (! *memptr) { __retres = 12; goto return_label; } __retres = 0; return_label: return __retres; } /*@ requires valid_dest: valid_or_empty(dest, n); requires valid_src: valid_read_or_empty(src, n); requires separation: \separated((char *)dest + (0 .. n - 1), (char *)src + (0 .. n - 1)); ensures copied_contents: memcmp{Post, Pre}((char *)\old(dest), (char *)\old(src), \old(n)) ≡ 0; ensures result_ptr: \result ≡ \old(dest); assigns *((char *)dest + (0 .. n - 1)), \result; assigns *((char *)dest + (0 .. n - 1)) \from *((char *)src + (0 .. n - 1)); assigns \result \from dest; */ void *memcpy(void * __restrict dest, void const * __restrict src, size_t n) { { size_t i = (unsigned int)0; /*@ loop invariant no_eva: 0 ≤ i ≤ n; loop invariant no_eva: ∀ ℤ k; 0 ≤ k < i ⇒ *((char *)dest + k) ≡ *((char *)src + k); loop assigns i, *((char *)dest + (0 .. n - 1)); loop variant n - i; */ while (i < n) { *((char *)dest + i) = *((char *)src + i); i += (size_t)1; } } return dest; } /*@ assigns \result; assigns \result \from (indirect: p), (indirect: q), (indirect: n); behavior separated: assumes separation: no_overlap: \separated(p + (0 .. n - 1), q + (0 .. n - 1)); ensures result_no_overlap: \result ≡ 0; behavior not_separated_lt: assumes separation: overlap: ¬\separated(p + (0 .. n - 1), q + (0 .. n - 1)); assumes p_before_q: p ≤ q < p + n; ensures result_p_before_q: \result ≡ -1; behavior not_separated_gt: assumes separation: overlap: ¬\separated(p + (0 .. n - 1), q + (0 .. n - 1)); assumes p_after_q: q < p ≤ q + n; ensures result_p_after_q: \result ≡ 1; complete behaviors not_separated_gt, not_separated_lt, separated; disjoint behaviors not_separated_gt, not_separated_lt, separated; */ static int memoverlap(char const *p, char const *q, size_t n) { int __retres; uintptr_t p1 = (unsigned int)p; uintptr_t p2 = (unsigned int)(p + n); uintptr_t q1 = (unsigned int)q; uintptr_t q2 = (unsigned int)(q + n); if (p1 <= q1) { if (p2 > q1) { __retres = -1; goto return_label; } else goto _LAND; } else { _LAND: ; if (q1 <= p1) if (q2 > p1) { __retres = 1; goto return_label; } else { __retres = 0; goto return_label; } else { __retres = 0; goto return_label; } } return_label: return __retres; } /*@ requires valid_dest: valid_or_empty(dest, n); requires valid_src: valid_read_or_empty(src, n); ensures copied_contents: memcmp{Post, Pre}((char *)\old(dest), (char *)\old(src), \old(n)) ≡ 0; ensures result_ptr: \result ≡ \old(dest); assigns *((char *)dest + (0 .. n - 1)), \result; assigns *((char *)dest + (0 .. n - 1)) \from *((char *)src + (0 .. n - 1)); assigns \result \from dest; */ void *memmove(void *dest, void const *src, size_t n) { void *__retres; int tmp; if (n == (size_t)0) { __retres = dest; goto return_label; } char *s = (char *)src; char *d = (char *)dest; tmp = memoverlap((char const *)dest,(char const *)src,n); if (tmp <= 0) { size_t i = (unsigned int)0; /*@ loop invariant no_eva: 0 ≤ i ≤ n; loop invariant no_eva: ∀ ℤ k; 0 ≤ k < i ⇒ *((char *)dest + k) ≡ \at(*((char *)src + k),LoopEntry); loop invariant no_eva: ∀ ℤ k; i ≤ k < n ⇒ *((char *)src + k) ≡ \at(*((char *)src + k),LoopEntry); loop assigns i, *((char *)dest + (0 .. n - 1)); loop variant n - i; */ while (i < n) { *(d + i) = *(s + i); i += (size_t)1; } } else { { size_t i_0 = n - (size_t)1; /*@ loop invariant no_eva: 0 ≤ i_0 < n; loop invariant no_eva: ∀ ℤ k; i_0 < k < n ⇒ *((char *)dest + k) ≡ \at(*((char *)src + k),LoopEntry); loop invariant no_eva: ∀ ℤ k; 0 ≤ k ≤ i_0 ⇒ *((char *)src + k) ≡ \at(*((char *)src + k),LoopEntry); loop assigns i_0, *((char *)dest + (0 .. n - 1)); loop variant i_0; */ while (i_0 > (size_t)0) { *(d + i_0) = *(s + i_0); i_0 -= (size_t)1; } } *(d + 0) = *(s + 0); } __retres = dest; return_label: return __retres; } /*@ requires valid_string_s: valid_read_string(s); ensures acsl_c_equiv: \result ≡ strlen(\old(s)); assigns \result; assigns \result \from (indirect: *(s + (0 ..))); */ size_t strlen(char const *s) { size_t i; i = (unsigned int)0; while ((int)*(s + i) != 0) i += (size_t)1; return i; } /*@ requires valid_string_s: valid_read_nstring(s, maxlen); ensures result_bounded: \result ≡ strlen(\old(s)) ∨ \result ≡ \old(maxlen); assigns \result; assigns \result \from (indirect: *(s + (0 .. maxlen - 1))), (indirect: maxlen); */ size_t strnlen(char const *s, size_t maxlen) { size_t i; i = (unsigned int)0; while (1) { if (i < maxlen) { if (! ((int)*(s + i) != 0)) break; } else break; i += (size_t)1; } return i; } /*@ requires valid_s: valid_or_empty(s, n); ensures acsl_c_equiv: memset((char *)\old(s), \old(c), \old(n)) ≡ \true; ensures result_ptr: \result ≡ \old(s); assigns *((char *)s + (0 .. n - 1)), \result; assigns *((char *)s + (0 .. n - 1)) \from c; assigns \result \from s; */ void *memset(void *s, int c, size_t n) { unsigned char *p = (unsigned char *)s; { size_t i = (unsigned int)0; while (i < n) { *(p + i) = (unsigned char)c; i += (size_t)1; } } return s; } /*@ requires valid_string_s1: valid_read_string(s1); requires valid_string_s2: valid_read_string(s2); ensures acsl_c_equiv: \result ≡ strcmp(\old(s1), \old(s2)); assigns \result; assigns \result \from (indirect: *(s1 + (0 ..))), (indirect: *(s2 + (0 ..))); */ int strcmp(char const *s1, char const *s2) { int __retres; size_t i; i = (unsigned int)0; while ((int)*(s1 + i) == (int)*(s2 + i)) { if ((int)*(s1 + i) == 0) { __retres = 0; goto return_label; } i += (size_t)1; } __retres = (int)*((unsigned char *)s1 + i) - (int)*((unsigned char *)s2 + i); return_label: return __retres; } /*@ requires valid_string_s1: valid_read_nstring(s1, n); requires valid_string_s2: valid_read_nstring(s2, n); ensures acsl_c_equiv: \result ≡ strncmp(\old(s1), \old(s2), \old(n)); assigns \result; assigns \result \from (indirect: *(s1 + (0 .. n - 1))), (indirect: *(s2 + (0 .. n - 1))), (indirect: n); */ int strncmp(char const *s1, char const *s2, size_t n) { int __retres; { size_t i = (unsigned int)0; while (i < n) { if ((int)*(s1 + i) != (int)*(s2 + i)) { __retres = (int)*((unsigned char *)s1 + i) - (int)*((unsigned char *)s2 + i); goto return_label; } if ((int)*(s1 + i) == 0) { __retres = 0; goto return_label; } i += (size_t)1; } } __retres = 0; return_label: return __retres; } /*@ requires valid_s1: valid_read_or_empty(s1, n); requires valid_s2: valid_read_or_empty(s2, n); requires initialization: s1: \initialized((char *)s1 + (0 .. n - 1)); requires initialization: s2: \initialized((char *)s2 + (0 .. n - 1)); requires danglingness: s1: non_escaping(s1, n); requires danglingness: s2: non_escaping(s2, n); ensures logic_spec: \result ≡ memcmp{Pre, Pre}((char *)\old(s1), (char *)\old(s2), \old(n)); assigns \result; assigns \result \from (indirect: *((char *)s1 + (0 .. n - 1))), (indirect: *((char *)s2 + (0 .. n - 1))); */ int memcmp(void const *s1, void const *s2, size_t n) { int __retres; unsigned char const *p1; unsigned char const *p2; p1 = (unsigned char const *)s1; p2 = (unsigned char const *)s2; { size_t i = (unsigned int)0; while (i < n) { if ((int)*(p1 + i) != (int)*(p2 + i)) { __retres = (int)*(p1 + i) - (int)*(p2 + i); goto return_label; } i += (size_t)1; } } __retres = 0; return_label: return __retres; } static int char_equal_ignore_case(char c1, char c2) { int __retres; if ((int)c1 >= 'A') if ((int)c1 <= 'Z') c1 = (char)((int)c1 - ('A' - 'a')); if ((int)c2 >= 'A') if ((int)c2 <= 'Z') c2 = (char)((int)c2 - ('A' - 'a')); if ((int)c1 == (int)c2) { __retres = 0; goto return_label; } else { __retres = (int)((unsigned char)c2) - (int)((unsigned char)c1); goto return_label; } return_label: return __retres; } /*@ requires valid_string_s1: valid_read_string(s1); requires valid_string_s2: valid_read_string(s2); assigns \result; assigns \result \from (indirect: *(s1 + (0 ..))), (indirect: *(s2 + (0 ..))); */ int strcasecmp(char const *s1, char const *s2) { int __retres; size_t i; i = (unsigned int)0; while (1) { if ((int)*(s1 + i) != 0) { if (! ((int)*(s2 + i) != 0)) break; } else break; { int res = char_equal_ignore_case(*(s1 + i),*(s2 + i)); if (res != 0) { __retres = res; goto return_label; } } i += (size_t)1; } if ((int)*(s1 + i) == 0) { if ((int)*(s2 + i) == 0) { __retres = 0; goto return_label; } else goto _LAND; } else { _LAND: ; if ((int)*(s1 + i) == 0) { __retres = -1; goto return_label; } else { __retres = 1; goto return_label; } } return_label: return __retres; } /*@ requires valid_string_src: valid_read_string(src); requires valid_string_dest: valid_string(dest); requires room_string: \valid(dest + (0 .. strlen(dest) + strlen(src))); ensures sum_of_lengths: strlen(\old(dest)) ≡ \old(strlen(dest) + strlen(src)); ensures initialization: dest: \initialized(\old(dest) + (0 .. \old(strlen(dest) + strlen(src)))); ensures dest_null_terminated: *(\old(dest) + \old(strlen(dest) + strlen(src))) ≡ 0; ensures result_ptr: \result ≡ \old(dest); assigns *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + strlen{Old}(src))), \result; assigns *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + strlen{Old}(src))) \from *(src + (0 .. strlen{Old}(src))); assigns \result \from dest; */ char *strcat(char *dest, char const *src) { size_t i; size_t n = strlen((char const *)dest); i = (unsigned int)0; while ((int)*(src + i) != 0) { *(dest + (n + i)) = *(src + i); i += (size_t)1; } *(dest + (n + i)) = (char)0; return dest; } /*@ requires valid_nstring_src: valid_read_nstring(src, n); requires valid_string_dest: valid_string(dest); ensures result_ptr: \result ≡ \old(dest); assigns *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + n)), \result; assigns *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + n)) \from *(src + (0 .. n)); assigns \result \from dest; behavior complete: assumes valid_string_src_fits: valid_read_string(src) ∧ strlen(src) ≤ n; requires room_string: \valid((dest + strlen(dest)) + (0 .. strlen(src))); ensures sum_of_lengths: strlen(\old(dest)) ≡ \old(strlen(dest) + strlen(src)); assigns *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + strlen{Old}(src))), \result; assigns *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + strlen{Old}(src))) \from *(src + (0 .. strlen{Old}(src))); assigns \result \from dest; behavior partial: assumes valid_string_src_too_large: ¬(valid_read_string(src) ∧ strlen(src) ≤ n); requires room_string: \valid((dest + strlen(dest)) + (0 .. n)); ensures sum_of_bounded_lengths: strlen(\old(dest)) ≡ \old(strlen(dest)) + \old(n); assigns *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + n)), \result; assigns *(dest + (strlen{Old}(dest) .. strlen{Old}(dest) + n)) \from *(src + (0 .. strlen{Old}(src))); assigns \result \from dest; */ char *strncat(char *dest, char const *src, size_t n) { size_t i; size_t dest_len = strlen((char const *)dest); i = (unsigned int)0; while (i < n) { if ((int)*(src + i) == 0) break; *(dest + (dest_len + i)) = *(src + i); i += (size_t)1; } *(dest + (dest_len + i)) = (char)0; return dest; } /*@ requires valid_string_src: valid_read_string(src); requires room_string: \valid(dest + (0 .. strlen(src))); requires separation: \separated(dest + (0 .. strlen(src)), src + (0 .. strlen(src))); ensures equal_contents: strcmp(\old(dest), \old(src)) ≡ 0; ensures result_ptr: \result ≡ \old(dest); assigns *(dest + (0 .. strlen{Old}(src))), \result; assigns *(dest + (0 .. strlen{Old}(src))) \from *(src + (0 .. strlen{Old}(src))); assigns \result \from dest; */ char *strcpy(char *dest, char const *src) { size_t i; i = (unsigned int)0; while ((int)*(src + i) != 0) { *(dest + i) = *(src + i); i += (size_t)1; } *(dest + i) = (char)0; return dest; } /*@ requires valid_string_src: valid_read_string(src); requires room_nstring: \valid(dest + (0 .. n - 1)); requires separation: \separated(dest + (0 .. n - 1), src + (0 .. n - 1)); ensures result_ptr: \result ≡ \old(dest); ensures initialization: \initialized(\old(dest) + (0 .. \old(n) - 1)); assigns *(dest + (0 .. n - 1)), \result; assigns *(dest + (0 .. n - 1)) \from *(src + (0 .. n - 1)); assigns \result \from dest; behavior complete: assumes src_fits: strlen(src) < n; ensures equal_after_copy: strcmp(\old(dest), \old(src)) ≡ 0; behavior partial: assumes src_too_long: n ≤ strlen(src); ensures equal_prefix: memcmp{Post, Post}(\old(dest), \old(src), \old(n)) ≡ 0; */ char *strncpy(char *dest, char const *src, size_t n) { size_t i; i = (unsigned int)0; while (i < n) { *(dest + i) = *(src + i); if ((int)*(src + i) == 0) break; i += (size_t)1; } while (i < n) { *(dest + i) = (char)0; i += (size_t)1; } return dest; } /*@ requires valid_string_s: valid_read_string(s); assigns \result; assigns \result \from s, *(s + (0 ..)), c; behavior found: assumes char_found: strchr(s, c) ≡ \true; ensures result_char: *\result ≡ (char)\old(c); ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s)); ensures result_in_length: \old(s) ≤ \result ≤ \old(s) + strlen(\old(s)); ensures result_valid_string: valid_read_string(\result); ensures result_first_occur: ∀ char *p; \old(s) ≤ p < \result ⇒ *p ≢ (char)\old(c); behavior not_found: assumes char_not_found: ¬(strchr(s, c) ≡ \true); ensures result_null: \result ≡ \null; behavior default: ensures result_null_or_same_base: \result ≡ \null ∨ \base_addr(\result) ≡ \base_addr(\old(s)); */ char *strchr(char const *s, int c) { char *__retres; size_t i; char const ch = (char)c; i = (unsigned int)0; while ((int)*(s + i) != (int)ch) { if ((int)*(s + i) == 0) { __retres = (char *)0; goto return_label; } i += (size_t)1; } __retres = (char *)(s + i); return_label: return __retres; } /*@ requires valid_string_s: valid_read_string(s); assigns \result; assigns \result \from s, *(s + (0 ..)), c; behavior found: assumes char_found: strchr(s, c) ≡ \true; ensures result_char: (int)*\result ≡ \old(c); ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s)); ensures result_valid_string: valid_read_string(\result); behavior not_found: assumes char_not_found: ¬(strchr(s, c) ≡ \true); ensures result_null: \result ≡ \null; behavior default: ensures result_null_or_same_base: \result ≡ \null ∨ \base_addr(\result) ≡ \base_addr(\old(s)); */ char *strrchr(char const *s, int c) { char *__retres; char const ch = (char)c; { size_t tmp; tmp = strlen(s); size_t i = tmp + (size_t)1; while (i > (size_t)0) { if ((int)*(s + (i - (size_t)1)) == (int)ch) { __retres = (char *)(s + (i - (size_t)1)); goto return_label; } i -= (size_t)1; } } __retres = (char *)0; return_label: return __retres; } /*@ requires valid: valid_read_or_empty(s, n) ∨ \valid_read((unsigned char *)s + (0 .. memchr_off((char *)s, c, n))); requires initialization: \initialized((unsigned char *)s + (0 .. n - 1)) ∨ \initialized((unsigned char *)s + (0 .. memchr_off((char *)s, c, n))); requires danglingness: non_escaping(s, n) ∨ non_escaping(s, (unsigned int)(memchr_off((char *)s, c, n) + 1)); assigns \result; assigns \result \from s, c, *((unsigned char *)s + (0 .. n - 1)); behavior found: assumes char_found: memchr((char *)s, c, n) ≡ \true; ensures result_same_base: \base_addr(\result) ≡ \base_addr(\old(s)); ensures result_char: (int)*((char *)\result) ≡ \old(c); ensures result_in_str: ∀ ℤ i; 0 ≤ i < \old(n) ⇒ *((unsigned char *)\old(s) + i) ≡ \old(c) ⇒ \result ≤ \old(s) + i; behavior not_found: assumes char_not_found: ¬(memchr((char *)s, c, n) ≡ \true); ensures result_null: \result ≡ \null; */ void *memchr(void const *s, int c, size_t n) { void *__retres; unsigned char const ch = (unsigned char)c; unsigned char const *ss = (unsigned char const *)s; { size_t i = (unsigned int)0; while (i < n) { if ((int)*(ss + i) == (int)ch) { __retres = (void *)(ss + i); goto return_label; } i += (size_t)1; } } __retres = (void *)0; return_label: return __retres; } void *memrchr(void const *s, int c, size_t n) { void *__retres; unsigned char const ch = (unsigned char)c; unsigned char const *ss = (unsigned char const *)s; { size_t i = n; while (i > (size_t)0) { if ((int)*(ss + (i - (size_t)1)) == (int)ch) { __retres = (void *)(ss + (i - (size_t)1)); goto return_label; } i -= (size_t)1; } } __retres = (void *)0; return_label: return __retres; } /*@ requires valid_string_haystack: valid_read_string(haystack); requires valid_string_needle: valid_read_string(needle); ensures result_null_or_in_haystack: \result ≡ \null ∨ (\subset(\result, \old(haystack) + (0 ..)) ∧ \valid_read(\result) ∧ memcmp{Pre, Pre}(\result, \old(needle), strlen(\old(needle))) ≡ 0); assigns \result; assigns \result \from haystack, (indirect: *(haystack + (0 ..))), (indirect: *(needle + (0 ..))); */ char *strstr(char const *haystack, char const *needle) { char *__retres; if ((int)*(needle + 0) == 0) { __retres = (char *)haystack; goto return_label; } { size_t i = (unsigned int)0; while ((int)*(haystack + i) != 0) { { size_t j; j = (unsigned int)0; while ((int)*(haystack + (i + j)) != 0) { if ((int)*(haystack + (i + j)) != (int)*(needle + j)) break; j += (size_t)1; } if ((int)*(needle + j) == 0) { __retres = (char *)(haystack + i); goto return_label; } } i += (size_t)1; } } __retres = (char *)0; return_label: return __retres; } static int __fc_strerror_init; /*@ ensures result_internal_str: \result ≡ __fc_p_strerror; ensures result_nul_terminated: *(\result + 63) ≡ 0; ensures result_valid_string: valid_read_string(\result); assigns \result; assigns \result \from __fc_p_strerror, (indirect: errnum); */ char *strerror(int errnum) { char *__retres; if (! __fc_strerror_init) { Frama_C_make_unknown(__fc_strerror,(unsigned int)63); __fc_strerror[63] = (char)0; __fc_strerror_init = 1; } __retres = __fc_strerror; return __retres; } /*@ requires valid_string_s: valid_read_string(s); assigns \result; assigns \result \from (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: __fc_heap_status); allocates \result; behavior allocation: assumes can_allocate: is_allocable(strlen(s)); ensures allocation: \fresh{Old, Here}(\result,strlen(\old(s))); ensures result_valid_string_and_same_contents: valid_string(\result) ∧ strcmp(\result, \old(s)) ≡ 0; assigns __fc_heap_status, \result; assigns __fc_heap_status \from (indirect: s), __fc_heap_status; assigns \result \from (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: __fc_heap_status); behavior no_allocation: assumes cannot_allocate: ¬is_allocable(strlen(s)); ensures result_null: \result ≡ \null; assigns \result; assigns \result \from \nothing; allocates \nothing; */ char *strdup(char const *s) { char *__retres; size_t tmp; tmp = strlen(s); size_t l = tmp + (size_t)1; char *p = malloc(l); if (! p) { __fc_errno = 12; __retres = (char *)0; goto return_label; } memcpy((void *)p,(void const *)s,l); __retres = p; return_label: return __retres; } /*@ assigns \result; assigns \result \from (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: n), (indirect: __fc_heap_status); allocates \result; behavior allocation: assumes can_allocate: is_allocable(\min(strlen(s), n + 1)); ensures allocation: \fresh{Old, Here}(\result,\min(strlen(\old(s)), \old(n) + 1)); ensures result_valid_string_bounded_and_same_prefix: \valid(\result + (0 .. \min(strlen(\old(s)), \old(n)))) ∧ valid_string(\result) ∧ strlen(\result) ≤ \old(n) ∧ strncmp(\result, \old(s), \old(n)) ≡ 0; assigns __fc_heap_status, \result; assigns __fc_heap_status \from (indirect: s), (indirect: n), __fc_heap_status; assigns \result \from (indirect: *(s + (0 .. strlen{Old}(s)))), (indirect: n), (indirect: __fc_heap_status); behavior no_allocation: assumes cannot_allocate: ¬is_allocable(\min(strlen(s), n + 1)); ensures result_null: \result ≡ \null; assigns \result; assigns \result \from \nothing; allocates \nothing; */ char *strndup(char const *s, size_t n) { char *__retres; size_t l; l = (unsigned int)0; while (l < n) { if ((int)*(s + l) == 0) break; l += (size_t)1; } char *p = malloc(l + (size_t)1); if (! p) { __fc_errno = 12; __retres = (char *)0; goto return_label; } memcpy((void *)p,(void const *)s,l); *(p + l) = (char)0; __retres = p; return_label: return __retres; } static int __fc_strsignal_init; /*@ ensures result_internal_str: \result ≡ __fc_p_strsignal; ensures result_nul_terminated: *(\result + 63) ≡ 0; ensures result_valid_string: valid_read_string(\result); assigns \result; assigns \result \from __fc_p_strsignal, (indirect: signum); */ char *strsignal(int signum) { char *__retres; if (! __fc_strsignal_init) { Frama_C_make_unknown(__fc_strsignal,(unsigned int)63); __fc_strsignal[63] = (char)0; __fc_strsignal_init = 1; } __retres = __fc_strsignal; return __retres; } /*@ ghost unsigned int volatile __fc_time __attribute__((__FRAMA_C_MODEL__)); */ /*@ assigns \result; assigns \result \from __fc_time; */ extern clock_t clock(void); /*@ assigns \result; assigns \result \from time1, time0; */ extern double difftime(time_t time1, time_t time0); /*@ requires valid_timeptr: \valid(timeptr); assigns *timeptr, \result; assigns *timeptr \from *timeptr; assigns \result \from (indirect: *timeptr); */ extern time_t mktime(struct tm *timeptr); /*@ assigns *timer, \result; assigns *timer \from __fc_time; assigns \result \from __fc_time; behavior null: assumes timer_null: timer ≡ \null; assigns \result; assigns \result \from __fc_time; behavior not_null: assumes timer_non_null: timer ≢ \null; requires valid_timer: \valid(timer); ensures initialization: timer: \initialized(\old(timer)); assigns *timer, \result; assigns *timer \from __fc_time; assigns \result \from __fc_time; complete behaviors not_null, null; disjoint behaviors not_null, null; */ extern time_t time(time_t *timer); char __fc_ctime[26]; char * const __fc_p_ctime = __fc_ctime; /*@ requires valid_timer: \valid_read(timer); requires initialization: init_timer: \initialized(timer); ensures result_points_to_ctime: \result ≡ __fc_p_ctime; ensures result_valid_string: valid_read_string(__fc_p_ctime); assigns __fc_ctime[0 .. 25], \result; assigns __fc_ctime[0 .. 25] \from (indirect: *timer), (indirect: __fc_time); assigns \result \from (indirect: *timer), (indirect: __fc_time), __fc_p_ctime; */ extern char *ctime(time_t const *timer); struct tm __fc_time_tm; struct tm * const __fc_p_time_tm = & __fc_time_tm; /*@ requires valid_timer: \valid_read(timer); ensures result_null_or_internal_tm: \result ≡ &__fc_time_tm ∨ \result ≡ \null; assigns \result, __fc_time_tm; assigns \result \from __fc_p_time_tm; assigns __fc_time_tm \from *timer; */ extern struct tm *gmtime(time_t const *timer); /*@ requires valid_timer: \valid_read(timer); ensures result_null_or_internal_tm: \result ≡ &__fc_time_tm ∨ \result ≡ \null; assigns \result, __fc_time_tm; assigns \result \from __fc_p_time_tm; assigns __fc_time_tm \from *timer; */ extern struct tm *localtime(time_t const *timer); /*@ requires dst_has_room: \valid(s + (0 .. max - 1)); requires valid_format: valid_read_string(format); requires valid_tm: \valid_read(tm); ensures result_bounded: \result ≤ \old(max); assigns *(s + (0 .. max - 1)), \result; assigns *(s + (0 .. max - 1)) \from (indirect: max), (indirect: *(format + (0 ..))), (indirect: *tm); assigns \result \from (indirect: max), (indirect: *(format + (0 ..))), (indirect: *tm); */ extern size_t strftime(char * __restrict s, size_t max, char const * __restrict format, struct tm const * __restrict tm); /*@ requires tp: \valid(tp); assigns \result, *tp, __fc_time; assigns \result \from __fc_time; assigns *tp \from __fc_time; assigns __fc_time \from __fc_time; behavior realtime_clock: assumes realtime: clk_id ≡ 666; ensures success: \result ≡ 0; ensures initialization: \initialized(\old(tp)); behavior monotonic_clock: assumes monotonic: clk_id ≡ 1; ensures success: \result ≡ 0; ensures initialization: \initialized(\old(tp)); behavior bad_clock_id: assumes bad_id: clk_id ≢ 666 ∧ clk_id ≢ 1; ensures error: \result ≡ 22; assigns \result; assigns \result \from clk_id; complete behaviors bad_clock_id, monotonic_clock, realtime_clock; disjoint behaviors bad_clock_id, monotonic_clock, realtime_clock; */ extern int clock_gettime(clockid_t clk_id, struct timespec *tp); /*@ axiomatic nanosleep_predicates { predicate abs_clock_in_range{L}(clockid_t id, struct timespec *tm) reads __fc_time; predicate valid_clock_id{L}(clockid_t id) reads __fc_time; } */ /*@ ghost int volatile __fc_interrupted __attribute__((__FRAMA_C_MODEL__)); */ /*@ requires valid_request: \valid_read(rqtp); requires initialization: initialized_request: \initialized(&rqtp->tv_sec) ∧ \initialized(&rqtp->tv_nsec); requires valid_nanosecs: 0 ≤ rqtp->tv_nsec < 1000000000; requires valid_remaining_or_null: rmtp ≡ \null ∨ \valid(rmtp); assigns \result; assigns \result \from (indirect: __fc_time), (indirect: __fc_interrupted), (indirect: clock_id), (indirect: flags), (indirect: rqtp), (indirect: *rqtp); behavior absolute: assumes absolute_time: (flags & 1) ≢ 0; assumes no_einval: abs_clock_in_range(clock_id, rqtp) ∧ valid_clock_id(clock_id); ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ 4 ∨ \result ≡ 22 ∨ \result ≡ 95; assigns \result; assigns \result \from (indirect: __fc_time), (indirect: __fc_interrupted), (indirect: clock_id), (indirect: rqtp), (indirect: *rqtp); behavior relative_interrupted: assumes relative_time: (flags & 1) ≡ 0; assumes interrupted: __fc_interrupted ≢ 0; assumes no_einval: valid_clock_id(clock_id); ensures result_interrupted: \result ≡ 4; ensures initialization: interrupted_remaining: \old(rmtp) ≢ \null ⇒ \initialized(&\old(rmtp)->tv_sec) ∧ \initialized(&\old(rmtp)->tv_nsec); ensures interrupted_remaining_decreases: \old(rmtp) ≢ \null ⇒ \old(rqtp)->tv_sec * 1000000000 + \old(rqtp)->tv_nsec ≥ \old(rmtp)->tv_sec * 1000000000 + \old(rmtp)->tv_nsec; ensures remaining_valid: \old(rmtp) ≢ \null ⇒ 0 ≤ \old(rmtp)->tv_nsec < 1000000000; assigns \result, *rmtp; assigns \result \from (indirect: __fc_time), (indirect: clock_id), (indirect: rqtp), (indirect: *rqtp); assigns *rmtp \from __fc_time, (indirect: clock_id), (indirect: rqtp), (indirect: *rqtp), (indirect: rmtp); behavior relative_no_error: assumes relative_time: (flags & 1) ≡ 0; assumes not_interrupted: __fc_interrupted ≡ 0; assumes no_einval: valid_clock_id(clock_id); ensures result_ok: \result ≡ 0; assigns \result; assigns \result \from (indirect: __fc_time), (indirect: clock_id), (indirect: rqtp), (indirect: *rqtp); behavior relative_invalid_clock_id: assumes relative_time: (flags & 1) ≡ 0; assumes not_interrupted: __fc_interrupted ≡ 0; assumes einval: ¬valid_clock_id(clock_id); ensures result_einval: \result ≡ 22; assigns \result; assigns \result \from (indirect: __fc_time), (indirect: clock_id), (indirect: rqtp), (indirect: *rqtp); complete behaviors relative_invalid_clock_id, relative_no_error, relative_interrupted, absolute; disjoint behaviors relative_invalid_clock_id, relative_no_error, relative_interrupted, absolute; */ extern int clock_nanosleep(clockid_t clock_id, int flags, struct timespec const *rqtp, struct timespec *rmtp); /*@ requires valid_request: \valid_read(rqtp); requires initialization: initialized_request: \initialized(&rqtp->tv_sec) ∧ \initialized(&rqtp->tv_nsec); requires valid_nanosecs: 0 ≤ rqtp->tv_nsec < 1000000000; requires valid_remaining_or_null: rmtp ≡ \null ∨ \valid(rmtp); ensures result_elapsed_or_interrupted: \result ≡ 0 ∨ \result ≡ -1; ensures initialization: interrupted_remaining: \old(rmtp) ≢ \null ∧ \result ≡ -1 ⇒ \initialized(&\old(rmtp)->tv_sec) ∧ \initialized(&\old(rmtp)->tv_nsec); ensures interrupted_remaining_decreases: \old(rmtp) ≢ \null ∧ \result ≡ -1 ⇒ \old(rqtp)->tv_sec * 1000000000 + \old(rqtp)->tv_nsec ≥ \old(rmtp)->tv_sec * 1000000000 + \old(rmtp)->tv_nsec; ensures interrupted_remaining_valid: \old(rmtp) ≢ \null ∧ \result ≡ -1 ⇒ 0 ≤ \old(rmtp)->tv_nsec < 1000000000; assigns \result, *rmtp; assigns \result \from (indirect: __fc_time), (indirect: rqtp), (indirect: *rqtp); assigns *rmtp \from (indirect: __fc_time), (indirect: rqtp), (indirect: *rqtp), (indirect: rmtp); */ extern int nanosleep(struct timespec const *rqtp, struct timespec *rmtp); extern char *tzname[2]; /*@ assigns *(tzname[0 .. 1] + (0 ..)); assigns *(tzname[0 .. 1] + (0 ..)) \from \nothing; */ extern void tzset(void); /*@ requires valid: valid_read_or_empty((void *)s, (unsigned int)(sizeof(wchar_t) * n)) ∨ \valid_read((unsigned char *)s + (0 .. wmemchr_off(s, c, n))); requires initialization: \initialized(s + (0 .. n - 1)) ∨ \initialized(s + (0 .. wmemchr_off(s, c, n))); requires danglingness: non_escaping((void *)s, (unsigned int)(sizeof(wchar_t) * n)) ∨ non_escaping((void *)s, (unsigned int)(sizeof(wchar_t) * (wmemchr_off(s, c, n) + 1))); ensures result_null_or_inside_s: \result ≡ \null ∨ \subset(\result, \old(s) + (0 .. \old(n) - 1)); assigns \result; assigns \result \from s, (indirect: *(s + (0 .. n - 1))), (indirect: c), (indirect: n); */ extern wchar_t *wmemchr(wchar_t const *s, wchar_t c, size_t n); /*@ requires valid_s1: valid_read_or_empty((void *)s1, (unsigned int)(sizeof(wchar_t) * n)); requires valid_s2: valid_read_or_empty((void *)s2, (unsigned int)(sizeof(wchar_t) * n)); requires initialization: s1: \initialized(s1 + (0 .. n - 1)); requires initialization: s2: \initialized(s2 + (0 .. n - 1)); requires danglingness: s1: non_escaping((void *)s1, (unsigned int)(sizeof(wchar_t) * n)); requires danglingness: s2: non_escaping((void *)s2, (unsigned int)(sizeof(wchar_t) * n)); assigns \result; assigns \result \from (indirect: *(s1 + (0 .. n - 1))), (indirect: *(s2 + (0 .. n - 1))), (indirect: n); */ extern int wmemcmp(wchar_t const *s1, wchar_t const *s2, size_t n); wchar_t *wmemcpy(wchar_t *dest, wchar_t const *src, size_t n); /*@ requires valid_src: \valid_read(src + (0 .. n - 1)); requires valid_dest: \valid(dest + (0 .. n - 1)); ensures result_ptr: \result ≡ \old(dest); assigns *(dest + (0 .. n - 1)), \result; assigns *(dest + (0 .. n - 1)) \from *(src + (0 .. n - 1)), (indirect: src), (indirect: n); assigns \result \from dest; */ extern wchar_t *wmemmove(wchar_t *dest, wchar_t const *src, size_t n); wchar_t *wmemset(wchar_t *dest, wchar_t val, size_t len); wchar_t *wcscat(wchar_t *dest, wchar_t const *src); /*@ requires valid_wstring_src: valid_read_wstring(wcs); ensures result_null_or_inside_wcs: \result ≡ \null ∨ \subset(\result, \old(wcs) + (0 ..)); assigns \result; assigns \result \from wcs, (indirect: *(wcs + (0 ..))), (indirect: wc); */ extern wchar_t *wcschr(wchar_t const *wcs, wchar_t wc); /*@ requires valid_wstring_s1: valid_read_wstring(s1); requires valid_wstring_s2: valid_read_wstring(s2); assigns \result; assigns \result \from (indirect: *(s1 + (0 ..))), (indirect: *(s2 + (0 ..))); */ extern int wcscmp(wchar_t const *s1, wchar_t const *s2); wchar_t *wcscpy(wchar_t *dest, wchar_t const *src); /*@ requires valid_wstring_wcs: valid_read_wstring(wcs); requires valid_wstring_accept: valid_read_wstring(accept); assigns \result; assigns \result \from (indirect: *(wcs + (0 ..))), (indirect: *(accept + (0 ..))); */ extern size_t wcscspn(wchar_t const *wcs, wchar_t const *accept); /*@ requires valid_nwstring_src: valid_read_nwstring(src, n); requires valid_wstring_dest: valid_wstring(dest); requires room_for_concatenation: \valid(dest + (wcslen(dest) .. wcslen(dest) + \min(wcslen(src), n))); requires separation: \separated( dest + (0 .. wcslen(dest) + wcslen(src)), src + (0 .. wcslen(src)) ); assigns *(dest + (0 ..)), \result; assigns *(dest + (0 ..)) \from *(dest + (0 ..)), (indirect: dest), *(src + (0 .. n - 1)), (indirect: src), (indirect: n); assigns \result \from (indirect: *(dest + (0 ..))), (indirect: *(src + (0 .. n - 1))), (indirect: n); */ extern size_t wcslcat(wchar_t * __restrict dest, wchar_t const * __restrict src, size_t n); /*@ requires valid_wstring_src: valid_read_wstring(src); requires room_nwstring: \valid(dest + (0 .. n)); requires separation: dest: src: \separated(dest + (0 .. n - 1), src + (0 .. n - 1)); assigns *(dest + (0 .. n - 1)), \result; assigns *(dest + (0 .. n - 1)) \from *(src + (0 .. n - 1)), (indirect: src), (indirect: n); assigns \result \from (indirect: *(dest + (0 .. n - 1))), (indirect: dest), (indirect: *(src + (0 .. n - 1))), (indirect: src), (indirect: n); */ extern size_t wcslcpy(wchar_t *dest, wchar_t const *src, size_t n); size_t wcslen(wchar_t const *str); wchar_t *wcsncat(wchar_t *dest, wchar_t const *src, size_t n); /*@ requires valid_wstring_s1: valid_read_wstring(s1); requires valid_wstring_s2: valid_read_wstring(s2); assigns \result; assigns \result \from (indirect: *(s1 + (0 .. n - 1))), (indirect: *(s2 + (0 .. n - 1))), (indirect: n); */ extern int wcsncmp(wchar_t const *s1, wchar_t const *s2, size_t n); wchar_t *wcsncpy(wchar_t *dest, wchar_t const *src, size_t n); /*@ requires valid_wstring_wcs: valid_read_wstring(wcs); requires valid_wstring_accept: valid_read_wstring(accept); ensures result_null_or_inside_wcs: \result ≡ \null ∨ \subset(\result, \old(wcs) + (0 ..)); assigns \result; assigns \result \from wcs, (indirect: *(wcs + (0 ..))), (indirect: *(accept + (0 ..))); */ extern wchar_t *wcspbrk(wchar_t const *wcs, wchar_t const *accept); /*@ requires valid_wstring_wcs: valid_read_wstring(wcs); ensures result_null_or_inside_wcs: \result ≡ \null ∨ \subset(\result, \old(wcs) + (0 ..)); assigns \result; assigns \result \from wcs, (indirect: *(wcs + (0 .. wcslen{Old}(wcs)))), (indirect: wc); */ extern wchar_t *wcsrchr(wchar_t const *wcs, wchar_t wc); /*@ requires valid_wstring_wcs: valid_read_wstring(wcs); requires valid_wstring_accept: valid_read_wstring(accept); assigns \result; assigns \result \from (indirect: *(wcs + (0 .. wcslen{Old}(wcs)))), (indirect: *(accept + (0 .. wcslen{Old}(accept)))); */ extern size_t wcsspn(wchar_t const *wcs, wchar_t const *accept); /*@ requires valid_wstring_haystack: valid_read_wstring(haystack); requires valid_wstring_needle: valid_read_wstring(needle); ensures result_null_or_inside_haystack: \result ≡ \null ∨ \subset(\result, \old(haystack) + (0 ..)); assigns \result; assigns \result \from haystack, (indirect: *(haystack + (0 ..))), (indirect: *(needle + (0 ..))); */ extern wchar_t *wcsstr(wchar_t const *haystack, wchar_t const *needle); /*@ requires room_nwstring: \valid(ws + (0 .. n - 1)); requires valid_stream: \valid(stream); ensures result_null_or_same: \result ≡ \null ∨ \result ≡ \old(ws); ensures terminated_string_on_success: \result ≢ \null ⇒ valid_wstring(\old(ws)); assigns *(ws + (0 .. n - 1)), \result; assigns *(ws + (0 .. n - 1)) \from (indirect: n), (indirect: *stream); assigns \result \from ws, (indirect: n), (indirect: *stream); */ extern wchar_t *fgetws(wchar_t * __restrict ws, int n, FILE * __restrict stream); /*@ axiomatic wformat_length { logic ℤ wformat_length{L}(wchar_t *format) ; } */ /*@ requires valid_dest: valid_or_empty((void *)dest, (unsigned int)(sizeof(wchar_t) * n)); requires valid_src: valid_read_or_empty((void *)src, (unsigned int)(sizeof(wchar_t) * n)); requires separation: dest: src: \separated(dest + (0 .. n - 1), src + (0 .. n - 1)); ensures result_ptr: \result ≡ \old(dest); assigns *(dest + (0 .. n - 1)), \result; assigns *(dest + (0 .. n - 1)) \from *(src + (0 .. n - 1)), (indirect: src), (indirect: n); assigns \result \from dest; */ wchar_t *wmemcpy(wchar_t *dest, wchar_t const *src, size_t n) { { size_t i = (unsigned int)0; while (i < n) { *(dest + i) = *(src + i); i += (size_t)1; } } return dest; } /*@ requires valid_wcs: \valid(dest + (0 .. len - 1)); ensures result_ptr: \result ≡ \old(dest); ensures initialization: wcs: \initialized(\old(dest) + (0 .. \old(len) - 1)); ensures contents_equal_wc: \subset(*(\old(dest) + (0 .. \old(len) - 1)), \old(val)); assigns *(dest + (0 .. len - 1)), \result; assigns *(dest + (0 .. len - 1)) \from val, (indirect: len); assigns \result \from dest; */ wchar_t *wmemset(wchar_t *dest, wchar_t val, size_t len) { { size_t i = (unsigned int)0; while (i < len) { *(dest + i) = val; i += (size_t)1; } } return dest; } /*@ requires valid_wstring_src: valid_read_wstring(src); requires room_wstring: \valid(dest + (0 .. wcslen(src))); requires separation: \separated(dest + (0 .. wcslen(src)), src + (0 .. wcslen(src))); ensures result_ptr: \result ≡ \old(dest); assigns *(dest + (0 .. wcslen{Old}(src))), \result; assigns *(dest + (0 .. wcslen{Old}(src))) \from *(src + (0 .. wcslen{Old}(src))), (indirect: src); assigns \result \from dest; */ wchar_t *wcscpy(wchar_t *dest, wchar_t const *src) { size_t i; i = (unsigned int)0; while (*(src + i) != 0) { *(dest + i) = *(src + i); i += (size_t)1; } *(dest + i) = 0; return dest; } /*@ requires valid_string_s: valid_read_wstring(str); ensures result_is_length: \result ≡ wcslen(\old(str)); assigns \result; assigns \result \from (indirect: *(str + (0 .. wcslen{Old}(str)))); */ size_t wcslen(wchar_t const *str) { size_t i; i = (unsigned int)0; while (*(str + i) != 0) i += (size_t)1; return i; } /*@ requires valid_wstring_src: valid_read_wstring(src); requires room_nwstring: \valid(dest + (0 .. n - 1)); requires separation: dest: src: \separated(dest + (0 .. n - 1), src + (0 .. n - 1)); ensures result_ptr: \result ≡ \old(dest); ensures initialization: \initialized(\old(dest) + (0 .. \old(n) - 1)); assigns *(dest + (0 .. n - 1)), \result; assigns *(dest + (0 .. n - 1)) \from *(src + (0 .. n - 1)), (indirect: src), (indirect: n); assigns \result \from dest; */ wchar_t *wcsncpy(wchar_t *dest, wchar_t const *src, size_t n) { size_t i; i = (unsigned int)0; while (i < n) { *(dest + i) = *(src + i); if (*(src + i) == 0) break; i += (size_t)1; } while (i < n) { *(dest + i) = 0; i += (size_t)1; } return dest; } /*@ requires valid_wstring_src: valid_read_wstring(src); requires valid_wstring_dest: valid_wstring(dest); requires room_for_concatenation: \valid(dest + (wcslen(dest) .. wcslen(dest) + wcslen(src))); requires separation: \separated( dest + (0 .. wcslen(dest) + wcslen(src)), src + (0 .. wcslen(src)) ); ensures result_ptr: \result ≡ \old(dest); assigns *(dest + (0 ..)), \result; assigns *(dest + (0 ..)) \from *(dest + (0 ..)), (indirect: dest), *(src + (0 ..)), (indirect: src); assigns \result \from dest; */ wchar_t *wcscat(wchar_t *dest, wchar_t const *src) { size_t i; size_t n = wcslen((wchar_t const *)dest); i = (unsigned int)0; while (*(src + i) != 0) { *(dest + (n + i)) = *(src + i); i += (size_t)1; } *(dest + (n + i)) = 0; return dest; } /*@ requires valid_nwstring_src: valid_read_nwstring(src, n); requires valid_wstring_dest: valid_wstring(dest); requires room_for_concatenation: \valid(dest + (wcslen(dest) .. wcslen(dest) + \min(wcslen(src), n))); requires separation: \separated( dest + (0 .. wcslen(dest) + wcslen(src)), src + (0 .. wcslen(src)) ); ensures result_ptr: \result ≡ \old(dest); assigns *(dest + (0 ..)), \result; assigns *(dest + (0 ..)) \from *(dest + (0 ..)), (indirect: dest), *(src + (0 .. n - 1)), (indirect: src), (indirect: n); assigns \result \from dest; */ wchar_t *wcsncat(wchar_t *dest, wchar_t const *src, size_t n) { size_t i; size_t dest_len = wcslen((wchar_t const *)dest); i = (unsigned int)0; while (1) { if (i < n) { if (! (*(src + i) != 0)) break; } else break; *(dest + (dest_len + i)) = *(src + i); i += (size_t)1; } *(dest + (dest_len + i)) = 0; return dest; } /*@ ghost extern int __fc_stack_status __attribute__((__FRAMA_C_MODEL__)); */ /*@ ensures allocation: \fresh{Old, Here}(\result,\old(size)); assigns __fc_stack_status, \result; assigns __fc_stack_status \from size, __fc_stack_status; assigns \result \from (indirect: size), (indirect: __fc_stack_status); allocates \result; */ extern void *alloca(size_t size); DIR __fc_opendir[16]; DIR * const __fc_p_opendir = __fc_opendir; /*@ requires dirp_valid_dir_stream: \subset(dirp, &__fc_opendir[0 .. 16 - 1]); ensures err_or_closed_on_success: (\result ≡ 0 ∧ \old(dirp)->__fc_dir_inode ≡ \null) ∨ \result ≡ -1; assigns \result, __fc_errno, *dirp; assigns \result \from dirp, *dirp, __fc_p_opendir; assigns __fc_errno \from dirp, *dirp, __fc_p_opendir; assigns *dirp \from dirp, *dirp, __fc_p_opendir; */ extern int closedir(DIR *dirp); /*@ ensures result_null_or_valid: \result ≡ \null ∨ \valid(\result); ensures valid_dir_stream_on_success: \result ≢ \null ⇒ \result ≡ &__fc_opendir[\result->__fc_dir_id]; ensures stream_positioned_on_success: \result ≢ \null ⇒ \result->__fc_dir_inode ≢ \null; assigns \result, __fc_errno; assigns \result \from *(path + (0 ..)), __fc_p_opendir; assigns __fc_errno \from *(path + (0 ..)), __fc_p_opendir; */ extern DIR *opendir(char const *path); /*@ requires dirp_valid_dir_stream: \subset(dirp, &__fc_opendir[0 .. 16 - 1]); ensures result_null_or_valid: \result ≡ \null ∨ \valid(\result); assigns \result, dirp->__fc_dir_position, __fc_errno; assigns \result \from *dirp, __fc_p_opendir; assigns dirp->__fc_dir_position \from dirp->__fc_dir_position; assigns __fc_errno \from dirp, *dirp, __fc_p_opendir; */ extern struct dirent *readdir(DIR *dirp); /*@ requires valid_fdset: \valid(fdset); requires initialization: \initialized(fdset); assigns *fdset; assigns *fdset \from *fdset, (indirect: fd); */ extern void FD_CLR(int fd, fd_set *fdset); /*@ requires valid_fdset: \valid_read(fdset); requires initialization: \initialized(fdset); assigns \result; assigns \result \from (indirect: *fdset), (indirect: fd); */ extern int FD_ISSET(int fd, fd_set const *fdset); /*@ requires valid_fdset: \valid(fdset); requires initialization: \initialized(fdset); assigns *fdset; assigns *fdset \from *fdset, (indirect: fd); */ extern void FD_SET(int fd, fd_set *fdset); /*@ requires valid_fdset: \valid(fdset); ensures initialization: \initialized(\old(fdset)); assigns *fdset; assigns *fdset \from \nothing; */ extern void FD_ZERO(fd_set *fdset); /*@ requires valid_res: \valid(res); ensures initialization: res: \initialized(\old(res)); ensures res_wrapped: *\old(res) ≡ (int)(\old(a) + \old(b)); ensures result_overflow: \old(a) + \old(b) ≡ (int)(\old(a) + \old(b))? \result ≡ 0: \result ≡ 1; assigns \result, *res; assigns \result \from a, b; assigns *res \from a, b; */ _Bool __builtin_sadd_overflow(int a, int b, int *res); /*@ requires valid_res: \valid(res); ensures initialization: res: \initialized(\old(res)); ensures res_wrapped: *\old(res) ≡ (long)(\old(a) + \old(b)); ensures result_overflow: \old(a) + \old(b) ≡ (long)(\old(a) + \old(b))? \result ≡ 0: \result ≡ 1; assigns \result, *res; assigns \result \from a, b; assigns *res \from a, b; */ _Bool __builtin_saddl_overflow(long a, long b, long *res); /*@ requires valid_res: \valid(res); ensures initialization: res: \initialized(\old(res)); ensures res_wrapped: *\old(res) ≡ (long long)(\old(a) + \old(b)); ensures result_overflow: \old(a) + \old(b) ≡ (long long)(\old(a) + \old(b))? \result ≡ 0: \result ≡ 1; assigns \result, *res; assigns \result \from a, b; assigns *res \from a, b; */ _Bool __builtin_saddll_overflow(long long a, long long b, long long *res); /*@ requires valid_res: \valid(res); ensures initialization: res: \initialized(\old(res)); ensures res_wrapped: *\old(res) ≡ (unsigned int)(\old(a) + \old(b)); ensures result_overflow: \old(a) + \old(b) ≡ (unsigned int)(\old(a) + \old(b))? \result ≡ 0: \result ≡ 1; assigns \result, *res; assigns \result \from a, b; assigns *res \from a, b; */ _Bool __builtin_uadd_overflow(unsigned int a, unsigned int b, unsigned int *res); /*@ requires valid_res: \valid(res); ensures initialization: res: \initialized(\old(res)); ensures res_wrapped: *\old(res) ≡ (unsigned long)(\old(a) + \old(b)); ensures result_overflow: \old(a) + \old(b) ≡ (unsigned long)(\old(a) + \old(b))? \result ≡ 0: \result ≡ 1; assigns \result, *res; assigns \result \from a, b; assigns *res \from a, b; */ _Bool __builtin_uaddl_overflow(unsigned long a, unsigned long b, unsigned long *res); /*@ requires valid_res: \valid(res); ensures initialization: res: \initialized(\old(res)); ensures res_wrapped: *\old(res) ≡ (unsigned long long)(\old(a) + \old(b)); ensures result_overflow: \old(a) + \old(b) ≡ (unsigned long long)(\old(a) + \old(b))? \result ≡ 0: \result ≡ 1; assigns \result, *res; assigns \result \from a, b; assigns *res \from a, b; */ _Bool __builtin_uaddll_overflow(unsigned long long a, unsigned long long b, unsigned long long *res); /*@ requires valid_res: \valid(res); ensures initialization: res: \initialized(\old(res)); ensures res_wrapped: *\old(res) ≡ (int)(\old(a) - \old(b)); ensures result_overflow: \old(a) - \old(b) ≡ (int)(\old(a) - \old(b))? \result ≡ 0: \result ≡ 1; assigns \result, *res; assigns \result \from a, b; assigns *res \from a, b; */ _Bool __builtin_ssub_overflow(int a, int b, int *res); /*@ requires valid_res: \valid(res); ensures initialization: res: \initialized(\old(res)); ensures res_wrapped: *\old(res) ≡ (long)(\old(a) - \old(b)); ensures result_overflow: \old(a) - \old(b) ≡ (long)(\old(a) - \old(b))? \result ≡ 0: \result ≡ 1; assigns \result, *res; assigns \result \from a, b; assigns *res \from a, b; */ _Bool __builtin_ssubl_overflow(long a, long b, long *res); /*@ requires valid_res: \valid(res); ensures initialization: res: \initialized(\old(res)); ensures res_wrapped: *\old(res) ≡ (long long)(\old(a) - \old(b)); ensures result_overflow: \old(a) - \old(b) ≡ (long long)(\old(a) - \old(b))? \result ≡ 0: \result ≡ 1; assigns \result, *res; assigns \result \from a, b; assigns *res \from a, b; */ _Bool __builtin_ssubll_overflow(long long a, long long b, long long *res); /*@ requires valid_res: \valid(res); ensures initialization: res: \initialized(\old(res)); ensures res_wrapped: *\old(res) ≡ (unsigned int)(\old(a) - \old(b)); ensures result_overflow: \old(a) - \old(b) ≡ (unsigned int)(\old(a) - \old(b))? \result ≡ 0: \result ≡ 1; assigns \result, *res; assigns \result \from a, b; assigns *res \from a, b; */ _Bool __builtin_usub_overflow(unsigned int a, unsigned int b, unsigned int *res); /*@ requires valid_res: \valid(res); ensures initialization: res: \initialized(\old(res)); ensures res_wrapped: *\old(res) ≡ (unsigned long)(\old(a) - \old(b)); ensures result_overflow: \old(a) - \old(b) ≡ (unsigned long)(\old(a) - \old(b))? \result ≡ 0: \result ≡ 1; assigns \result, *res; assigns \result \from a, b; assigns *res \from a, b; */ _Bool __builtin_usubl_overflow(unsigned long a, unsigned long b, unsigned long *res); /*@ requires valid_res: \valid(res); ensures initialization: res: \initialized(\old(res)); ensures res_wrapped: *\old(res) ≡ (unsigned long long)(\old(a) - \old(b)); ensures result_overflow: \old(a) - \old(b) ≡ (unsigned long long)(\old(a) - \old(b))? \result ≡ 0: \result ≡ 1; assigns \result, *res; assigns \result \from a, b; assigns *res \from a, b; */ _Bool __builtin_usubll_overflow(unsigned long long a, unsigned long long b, unsigned long long *res); /*@ requires valid_res: \valid(res); ensures initialization: res: \initialized(\old(res)); ensures res_wrapped: *\old(res) ≡ (int)(\old(a) * \old(b)); ensures result_overflow: \old(a) * \old(b) ≡ (int)(\old(a) * \old(b))? \result ≡ 0: \result ≡ 1; assigns \result, *res; assigns \result \from a, b; assigns *res \from a, b; */ _Bool __builtin_smul_overflow(int a, int b, int *res); /*@ requires valid_res: \valid(res); ensures initialization: res: \initialized(\old(res)); ensures res_wrapped: *\old(res) ≡ (long)(\old(a) * \old(b)); ensures result_overflow: \old(a) * \old(b) ≡ (long)(\old(a) * \old(b))? \result ≡ 0: \result ≡ 1; assigns \result, *res; assigns \result \from a, b; assigns *res \from a, b; */ _Bool __builtin_smull_overflow(long a, long b, long *res); /*@ requires valid_res: \valid(res); ensures initialization: res: \initialized(\old(res)); ensures res_wrapped: *\old(res) ≡ (long long)(\old(a) * \old(b)); ensures result_overflow: \old(a) * \old(b) ≡ (long long)(\old(a) * \old(b))? \result ≡ 0: \result ≡ 1; assigns \result, *res; assigns \result \from a, b; assigns *res \from a, b; */ _Bool __builtin_smulll_overflow(long long a, long long b, long long *res); /*@ requires valid_res: \valid(res); ensures initialization: res: \initialized(\old(res)); ensures res_wrapped: *\old(res) ≡ (unsigned int)(\old(a) * \old(b)); ensures result_overflow: \old(a) * \old(b) ≡ (unsigned int)(\old(a) * \old(b))? \result ≡ 0: \result ≡ 1; assigns \result, *res; assigns \result \from a, b; assigns *res \from a, b; */ _Bool __builtin_umul_overflow(unsigned int a, unsigned int b, unsigned int *res); /*@ requires valid_res: \valid(res); ensures initialization: res: \initialized(\old(res)); ensures res_wrapped: *\old(res) ≡ (unsigned long)(\old(a) * \old(b)); ensures result_overflow: \old(a) * \old(b) ≡ (unsigned long)(\old(a) * \old(b))? \result ≡ 0: \result ≡ 1; assigns \result, *res; assigns \result \from a, b; assigns *res \from a, b; */ _Bool __builtin_umull_overflow(unsigned long a, unsigned long b, unsigned long *res); /*@ requires valid_res: \valid(res); ensures initialization: res: \initialized(\old(res)); ensures res_wrapped: *\old(res) ≡ (unsigned long long)(\old(a) * \old(b)); ensures result_overflow: \old(a) * \old(b) ≡ (unsigned long long)(\old(a) * \old(b))? \result ≡ 0: \result ≡ 1; assigns \result, *res; assigns \result \from a, b; assigns *res \from a, b; */ _Bool __builtin_umulll_overflow(unsigned long long a, unsigned long long b, unsigned long long *res); /*@ requires valid_filename: valid_read_string(filename); assigns \result; assigns \result \from (indirect: *(filename + (0 ..))), (indirect: mode); */ extern int creat(char const *filename, mode_t mode); /*@ assigns \result; assigns \result \from fd, cmd; */ extern int fcntl(int fd, int cmd, void * const *__va_params); /*@ requires valid_filename: valid_read_string(filename); assigns \result; assigns \result \from (indirect: *(filename + (0 ..))), (indirect: flags); */ extern int open(char const *filename, int flags, void * const *__va_params); /*@ requires valid_filename: valid_read_string(filename); assigns \result; assigns \result \from (indirect: dirfd), (indirect: *(filename + (0 ..))), (indirect: flags); */ extern int openat(int dirfd, char const *filename, int flags, void * const *__va_params); /*@ requires cmd_has_void_arg: cmd ≡ 1 ∨ cmd ≡ 3 ∨ cmd ≡ 9; assigns \result; assigns \result \from fd, cmd; */ extern int __va_fcntl_void(int fd, int cmd); /*@ requires cmd_has_int_arg: cmd ≡ 0 ∨ cmd ≡ 0x406 ∨ cmd ≡ 4 ∨ cmd ≡ 8 ∨ cmd ≡ 2; assigns \result; assigns \result \from fd, cmd, arg; */ extern int __va_fcntl_int(int fd, int cmd, int arg); /*@ requires cmd_as_flock_arg: cmd ≡ 5 ∨ cmd ≡ 6 ∨ cmd ≡ 7; requires valid_arg: \valid(arg); assigns \result, *arg; assigns \result \from fd, cmd, *arg; assigns *arg \from fd, cmd, *arg; */ extern int __va_fcntl_flock(int fd, int cmd, struct flock *arg); /*@ requires valid_filename: valid_read_string(filename); requires flag_not_CREAT: (flags & 0x40) ≡ 0; assigns \result; assigns \result \from (indirect: *(filename + (0 ..))), (indirect: flags); */ extern int __va_open_void(char const *filename, int flags); /*@ requires valid_filename: valid_read_string(filename); assigns \result; assigns \result \from (indirect: *(filename + (0 ..))), (indirect: flags), (indirect: mode); */ extern int __va_open_mode_t(char const *filename, int flags, mode_t mode); /*@ requires valid_filename: valid_read_string(filename); requires flag_not_CREAT: (flags & 0x40) ≡ 0; assigns \result; assigns \result \from (indirect: dirfd), (indirect: *(filename + (0 ..))), (indirect: flags); */ extern int __va_openat_void(int dirfd, char const *filename, int flags); /*@ requires valid_filename: valid_read_string(filename); assigns \result; assigns \result \from (indirect: dirfd), (indirect: *(filename + (0 ..))), (indirect: flags), (indirect: mode); */ extern int __va_openat_mode_t(int dirfd, char const *filename, int flags, mode_t mode); /*@ ghost extern int __fc_tz __attribute__((__FRAMA_C_MODEL__)); */ /*@ requires valid_path: valid_read_string(path); requires valid_times_or_null: \valid_read(times + (0 .. 1)) ∨ times ≡ \null; assigns \result; assigns \result \from (indirect: *(path + (0 .. strlen{Old}(path)))), (indirect: times), (indirect: *(times + (0 .. 1))); */ extern int utimes(char const *path, struct timeval const * /*[2]*/ times); /*@ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1; assigns tv->tv_sec, tv->tv_usec, *((struct timezone *)tz), \result; assigns tv->tv_sec \from __fc_time; assigns tv->tv_usec \from __fc_time; assigns *((struct timezone *)tz) \from __fc_tz; assigns \result \from (indirect: tv), (indirect: tz), *tv, *((struct timezone *)tz), __fc_tz; behavior tv_and_tz_null: assumes null_tv_tz: tv ≡ \null ∧ tz ≡ \null; assigns \result; assigns \result \from (indirect: __fc_tz); behavior tv_not_null: assumes non_null_tv_null_tz: tv ≢ \null ∧ tz ≡ \null; ensures initialization: tv_sec: tv_usec: \initialized(&\old(tv)->tv_sec) ∧ \initialized(&\old(tv)->tv_usec); ensures tv_usec_bounded: 0 ≤ \old(tv)->tv_usec ≤ 999999; assigns tv->tv_sec, tv->tv_usec, \result; assigns tv->tv_sec \from (indirect: __fc_time); assigns tv->tv_usec \from (indirect: __fc_time); assigns \result \from (indirect: *tv), (indirect: __fc_tz); behavior tz_not_null: assumes null_tv_non_null_tz: tv ≡ \null ∧ tz ≢ \null; ensures initialization: tz: \initialized((struct timezone *)\old(tz)); assigns *((struct timezone *)tz), \result; assigns *((struct timezone *)tz) \from __fc_tz; assigns \result \from (indirect: *((struct timezone *)tz)), (indirect: __fc_tz); behavior tv_and_tz_not_null: assumes non_null_tv_tz: tv ≢ \null ∧ tz ≢ \null; ensures initialization: tv_sec: tv_usec: \initialized(&\old(tv)->tv_sec) ∧ \initialized(&\old(tv)->tv_usec); ensures initialization: tz: \initialized((struct timezone *)\old(tz)); assigns tv->tv_sec, tv->tv_usec, *((struct timezone *)tz), \result; assigns tv->tv_sec \from (indirect: __fc_time); assigns tv->tv_usec \from (indirect: __fc_time); assigns *((struct timezone *)tz) \from __fc_tz; assigns \result \from (indirect: *tv), (indirect: *((struct timezone *)tz)), (indirect: __fc_tz); complete behaviors tv_and_tz_not_null, tz_not_null, tv_not_null, tv_and_tz_null; disjoint behaviors tv_and_tz_not_null, tz_not_null, tv_not_null, tv_and_tz_null; */ extern int gettimeofday(struct timeval * __restrict tv, void * __restrict tz); /*@ requires valid_tv_or_null: \valid_read(tv) ∨ tv ≡ \null; requires valid_tz_or_null: \valid_read(tz) ∨ tz ≡ \null; ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1; assigns __fc_time, __fc_tz, \result; assigns __fc_time \from tv->tv_sec, tv->tv_usec, tz->tz_dsttime, tz->tz_minuteswest; assigns __fc_tz \from tv->tv_sec, tv->tv_usec, tz->tz_dsttime, tz->tz_minuteswest; assigns \result \from (indirect: *tv), (indirect: *tz); */ extern int settimeofday(struct timeval const *tv, struct timezone const *tz); /*@ ghost struct itimerval volatile __fc_itimer_real __attribute__((__FRAMA_C_MODEL__)); */ /*@ ghost struct itimerval volatile __fc_itimer_virtual __attribute__((__FRAMA_C_MODEL__)); */ /*@ ghost struct itimerval volatile __fc_itimer_prof __attribute__((__FRAMA_C_MODEL__)); */ /*@ requires valid_curr_value: \valid(curr_value); ensures initialization: curr_value: \initialized(\old(curr_value)); assigns \result, *curr_value; assigns \result \from (indirect: which); assigns *curr_value \from __fc_itimer_real, __fc_itimer_virtual, __fc_itimer_prof; behavior real: assumes itimer_real: which ≡ 0; ensures result_ok: \result ≡ 0; assigns \result, *curr_value; assigns \result \from \nothing; assigns *curr_value \from __fc_itimer_real; behavior virtual: assumes itimer_virtual: which ≡ 1; ensures result_ok: \result ≡ 0; assigns \result, *curr_value; assigns \result \from \nothing; assigns *curr_value \from __fc_itimer_virtual; behavior prof: assumes itimer_prof: which ≡ 2; ensures result_ok: \result ≡ 0; assigns \result, *curr_value; assigns \result \from \nothing; assigns *curr_value \from __fc_itimer_prof; behavior invalid: assumes invalid_which: which ≢ 0 ∧ which ≢ 1 ∧ which ≢ 2; ensures result_error: \result ≡ -1; assigns \result; assigns \result \from \nothing; complete behaviors invalid, prof, virtual, real; disjoint behaviors invalid, prof, virtual, real; */ extern int getitimer(int which, struct itimerval *curr_value); /*@ requires valid_new_value: \valid_read(new_value); requires old_value_null_or_valid: old_value ≡ \null ∨ \valid(old_value); ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1; assigns *old_value, \result; assigns *old_value \from (indirect: which), (indirect: old_value), (indirect: new_value), __fc_itimer_real, __fc_itimer_virtual, __fc_itimer_prof; assigns \result \from (indirect: which), (indirect: new_value), (indirect: *new_value); behavior real: assumes itimer_real_and_valid: which ≡ 0 ≤ new_value->it_value.tv_usec ≤ 999999 ∧ 0 ≤ new_value->it_interval.tv_usec ≤ 999999; ensures result_ok: \result ≡ 0; ensures initialization: old_value: \initialized(\old(old_value)); assigns \result, *old_value, __fc_itimer_real; assigns \result \from \nothing; assigns *old_value \from __fc_itimer_real; assigns __fc_itimer_real \from *new_value; behavior virtual: assumes itimer_virtual_and_valid: which ≡ 1 ∧ 0 ≤ new_value->it_value.tv_usec ≤ 999999 ∧ 0 ≤ new_value->it_interval.tv_usec ≤ 999999; ensures result_ok: \result ≡ 0; ensures initialization: old_value: \initialized(\old(old_value)); assigns \result, *old_value; assigns \result \from \nothing; assigns *old_value \from __fc_itimer_virtual; behavior prof: assumes itimer_prof_and_valid: which ≡ 2 ∧ 0 ≤ new_value->it_value.tv_usec ≤ 999999 ∧ 0 ≤ new_value->it_interval.tv_usec ≤ 999999; ensures result_ok: \result ≡ 0; ensures initialization: old_value: \initialized(\old(old_value)); assigns \result, *old_value; assigns \result \from \nothing; assigns *old_value \from __fc_itimer_prof; behavior invalid: assumes invalid_itimer_or_new_value: (which ≢ 0 ∧ which ≢ 1 ∧ which ≢ 2) ∨ ¬(0 ≤ new_value->it_value.tv_usec ≤ 999999 ∧ 0 ≤ new_value->it_interval.tv_usec ≤ 999999); ensures result_error: \result ≡ -1; assigns \result; assigns \result \from \nothing; disjoint behaviors invalid, prof, virtual, real; */ extern int setitimer(int which, struct itimerval const * __restrict new_value, struct itimerval * __restrict old_value); /*@ ghost int volatile __fc_fds_state; */ /*@ requires nfds: nfds ≥ 0; requires readfs: readfds ≡ \null ∨ \valid(readfds); requires writefds: writefds ≡ \null ∨ \valid(writefds); requires errorfds: errorfds ≡ \null ∨ \valid(errorfds); requires timeout: timeout ≡ \null ∨ \valid(timeout); assigns __fc_fds_state, *readfds, *writefds, *errorfds, *timeout, \result; assigns __fc_fds_state \from __fc_fds_state; assigns *readfds \from (indirect: nfds), (indirect: readfds), (indirect: *readfds), (indirect: writefds), (indirect: *writefds), (indirect: errorfds), (indirect: *errorfds), (indirect: timeout), (indirect: *timeout), __fc_fds_state; assigns *writefds \from (indirect: nfds), (indirect: readfds), (indirect: *readfds), (indirect: writefds), (indirect: *writefds), (indirect: errorfds), (indirect: *errorfds), (indirect: timeout), (indirect: *timeout), __fc_fds_state; assigns *errorfds \from (indirect: nfds), (indirect: readfds), (indirect: *readfds), (indirect: writefds), (indirect: *writefds), (indirect: errorfds), (indirect: *errorfds), (indirect: timeout), (indirect: *timeout), __fc_fds_state; assigns *timeout \from (indirect: nfds), (indirect: readfds), (indirect: *readfds), (indirect: writefds), (indirect: *writefds), (indirect: errorfds), (indirect: *errorfds), (indirect: timeout), (indirect: *timeout), __fc_fds_state; assigns \result \from (indirect: nfds), (indirect: readfds), (indirect: *readfds), (indirect: writefds), (indirect: *writefds), (indirect: errorfds), (indirect: *errorfds), (indirect: timeout), (indirect: *timeout), __fc_fds_state; behavior read_notnull: assumes readfds_is_not_null: readfds ≢ \null; ensures initialization: readfds: \initialized(\old(readfds)); behavior write_notnull: assumes writefds_is_not_null: writefds ≢ \null; ensures initialization: writefds: \initialized(\old(writefds)); behavior error_notnull: assumes errorfds_is_not_null: errorfds ≢ \null; ensures initialization: errorfds: \initialized(\old(errorfds)); behavior timeout_notnull: assumes timeout_is_not_null: timeout ≢ \null; ensures initialization: timeout: \initialized(\old(timeout)); */ extern int select(int nfds, fd_set *readfds, fd_set *writefds, fd_set *errorfds, struct timeval *timeout); /*@ requires valid_string_path: valid_read_string(path); ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1; assigns \result; assigns \result \from (indirect: path), (indirect: *(path + (0 ..))), (indirect: mode); */ extern int mkdir(char const *path, mode_t mode); /*@ requires valid_pathname: valid_read_string(pathname); requires valid_buf: \valid(buf); ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1; ensures init_on_success: initialization: buf: \result ≡ 0 ⇒ \initialized(\old(buf)); assigns \result, *buf; assigns \result \from *(pathname + (0 ..)); assigns *buf \from *(pathname + (0 ..)); */ extern int stat(char const *pathname, struct stat *buf); /*@ assigns \result; assigns \result \from (indirect: cmask); */ extern mode_t umask(mode_t cmask); /*@ assigns *(*(outbuf + (0 .. *outbytesleft - 1))), __fc_errno; assigns *(*(outbuf + (0 .. *outbytesleft - 1))) \from *(*(inbuf + (0 .. *inbytesleft - 1))); */ extern size_t iconv(iconv_t cd, char ** __restrict inbuf, size_t * __restrict inbytesleft, char ** __restrict outbuf, size_t * __restrict outbytesleft); /*@ ensures result_zero_or_neg: \result ≡ 0 ∨ \result ≡ -1; assigns __fc_errno; */ extern int iconv_close(iconv_t); /*@ assigns \result, __fc_errno; assigns \result \from *(tocode + (..)), *(fromcode + (..)); */ extern iconv_t iconv_open(char const *tocode, char const *fromcode); extern char __fc_basename[256]; char *__fc_p_basename = __fc_basename; /*@ requires null_or_valid_string_path: path ≡ \null ∨ valid_read_string(path); ensures result_points_to_internal_storage_or_path: \subset(\result, {__fc_p_basename, \old(path)}); assigns *(path + (0 ..)), __fc_basename[0 ..], \result; assigns *(path + (0 ..)) \from *(path + (0 ..)), __fc_basename[0 ..]; assigns __fc_basename[0 ..] \from *(path + (0 ..)), __fc_basename[0 ..]; assigns \result \from __fc_p_basename, path; */ extern char *basename(char *path); extern char __fc_dirname[256]; char *__fc_p_dirname = __fc_dirname; /*@ requires null_or_valid_string_path: path ≡ \null ∨ valid_read_string(path); ensures result_points_to_internal_storage_or_path: \subset(\result, {__fc_p_dirname, \old(path)}); assigns *(path + (0 ..)), __fc_dirname[0 ..], \result; assigns *(path + (0 ..)) \from *(path + (0 ..)), __fc_dirname[0 ..]; assigns __fc_dirname[0 ..] \from *(path + (0 ..)), __fc_dirname[0 ..]; assigns \result \from __fc_p_dirname, path; */ extern char *dirname(char *path); /*@ requires valid_file_descriptors: \valid(fds + (0 .. nfds - 1)); ensures error_timeout_or_bounded: \result ≡ -1 ∨ \result ≡ 0 ∨ (1 ≤ \result ≤ \old(nfds)); ensures initialization: revents: \initialized(&(\old(fds) + (0 .. \old(nfds) - 1))->revents); assigns (fds + (0 .. nfds - 1))->revents, \result; assigns (fds + (0 .. nfds - 1))->revents \from (indirect: (fds + (0 .. nfds - 1))->fd), (fds + (0 .. nfds - 1))->events, (indirect: nfds), (indirect: timeout), (indirect: Frama_C_entropy_source); assigns \result \from (indirect: (fds + (0 .. nfds - 1))->fd), (indirect: (fds + (0 .. nfds - 1))->events), (indirect: nfds), (indirect: timeout), (indirect: Frama_C_entropy_source); */ extern int poll(struct pollfd *fds, nfds_t nfds, int timeout); /*@ requires valid_cond: \valid(cond); ensures sucess: \result ≡ 0; assigns \result; assigns \result \from \nothing; */ extern int pthread_cond_broadcast(pthread_cond_t *cond); /*@ requires valid_cond: \valid(cond); ensures success_or_error: \result ≡ 0 ∨ \result ≡ 16; assigns \result; assigns \result \from (indirect: *cond); */ extern int pthread_cond_destroy(pthread_cond_t *cond); /*@ requires valid_cond: \valid(cond); requires valid_null_attr: attr ≡ \null ∨ \valid_read(attr); ensures initialization: cond: \initialized(\old(cond)); ensures success: \result ≡ 0; assigns *cond, \result; assigns *cond \from *attr; assigns \result \from \nothing; */ extern int pthread_cond_init(pthread_cond_t * __restrict cond, pthread_condattr_t const * __restrict attr); /*@ requires valid_cond: \valid(cond); requires valid_mutex: \valid(mutex); ensures success: \result ≡ 0; assigns \result; assigns \result \from \nothing; */ extern int pthread_cond_wait(pthread_cond_t * __restrict cond, pthread_mutex_t * __restrict mutex); /*@ requires valid_thread: \valid(thread); requires valid_null_attr: attr ≡ \null ∨ \valid_read(attr); requires valid_routine: \valid_function(start_routine); requires valid_null_arg: arg ≡ \null ∨ \valid((char *)arg); ensures success_or_error: \result ≡ 0 ∨ \result ≡ 11 ∨ \result ≡ 22 ∨ \result ≡ 1; assigns *thread, \result; assigns *thread \from *attr; assigns \result \from (indirect: *attr); */ extern int pthread_create(pthread_t * __restrict thread, pthread_attr_t const * __restrict attr, void *(*start_routine)(void *), void * __restrict arg); /*@ requires valid_or_null_retval: retval ≡ \null ∨ \valid(retval); ensures success_or_error: \result ≡ 0 ∨ \result ≡ 35 ∨ \result ≡ 22 ∨ \result ≡ 3; assigns *retval, \result; assigns *retval \from thread; assigns \result \from (indirect: thread); behavior ignore_retval: assumes null_retval: retval ≡ \null; assigns \result; assigns \result \from (indirect: thread); behavior use_retval: assumes valid_retval: \valid(retval); assigns *retval, \result; assigns *retval \from thread; assigns \result \from (indirect: thread); */ extern int pthread_join(pthread_t thread, void **retval); /*@ requires mutex_valid: \valid(mutex); ensures init_or_busy: \result ≡ 0 ∨ \result ≡ 16; assigns *mutex, \result; assigns *mutex \from *mutex; assigns \result \from (indirect: *mutex); */ extern int pthread_mutex_destroy(pthread_mutex_t *mutex); /*@ requires mutex_valid: \valid(mutex); requires attrs_valid_or_null: attrs ≡ \null ∨ \valid_read(attrs); ensures initialization: success_or_error: (\result ≡ 0 ∧ \initialized(\old(mutex))) ∨ \result ≡ 11 ∨ \result ≡ 12 ∨ \result ≡ 1 ∨ \result ≡ 22; assigns *mutex, \result; assigns *mutex \from *mutex, *attrs; assigns \result \from (indirect: *mutex), (indirect: *attrs); */ extern int pthread_mutex_init(pthread_mutex_t * __restrict mutex, pthread_mutexattr_t const * __restrict attrs); /*@ requires mutex_valid: \valid(mutex); ensures success_or_error: \result ≡ 0 ∨ \result ≡ 11 ∨ \result ≡ 22 ∨ \result ≡ 35; assigns *mutex, \result; assigns *mutex \from *mutex; assigns \result \from (indirect: *mutex); */ extern int pthread_mutex_lock(pthread_mutex_t *mutex); /*@ requires mutex_valid: \valid(mutex); ensures success_or_error: \result ≡ 0 ∨ \result ≡ 1; assigns *mutex, \result; assigns *mutex \from *mutex; assigns \result \from (indirect: *mutex); */ extern int pthread_mutex_unlock(pthread_mutex_t *mutex); extern char __fc_getpwuid_pw_name[64]; extern char __fc_getpwuid_pw_passwd[64]; extern char __fc_getpwuid_pw_dir[64]; extern char __fc_getpwuid_pw_shell[64]; struct passwd __fc_pwd = {.pw_name = __fc_getpwuid_pw_name, .pw_passwd = __fc_getpwuid_pw_passwd, .pw_uid = 0U, .pw_gid = 0U, .pw_gecos = (char *)0, .pw_dir = __fc_getpwuid_pw_dir, .pw_shell = __fc_getpwuid_pw_shell}; struct passwd *__fc_p_pwd = & __fc_pwd; /*@ requires valid_name: valid_read_string(name); ensures result_null_or_internal_struct: \result ≡ \null ∨ \result ≡ __fc_p_pwd; assigns \result, __fc_pwd; assigns \result \from __fc_p_pwd, (indirect: *(name + (0 ..))); assigns __fc_pwd \from (indirect: *(name + (0 ..))); */ extern struct passwd *getpwnam(char const *name); /*@ ensures result_null_or_internal_struct: \result ≡ \null ∨ \result ≡ __fc_p_pwd; assigns \result, __fc_pwd; assigns \result \from __fc_p_pwd, (indirect: uid); assigns __fc_pwd \from (indirect: uid); */ extern struct passwd *getpwuid(uid_t uid); /*@ assigns *(env + (0 .. 4)); */ extern int setjmp(int * /*[5]*/ env); /*@ ensures never_terminates: \false; assigns \nothing; */ extern void longjmp(int * /*[5]*/ env, int val); /*@ ensures never_terminates: \false; assigns \nothing; */ extern void siglongjmp(sigjmp_buf env, int val); /*@ assigns \result; assigns \result \from (indirect: fd), (indirect: request); */ extern int __va_ioctl_void(int fd, int request); /*@ assigns \result; assigns \result \from (indirect: fd), (indirect: request), (indirect: arg); */ extern int __va_ioctl_int(int fd, int request, int arg); /*@ assigns \result, *((char *)argp + (0 ..)); assigns \result \from (indirect: fd), (indirect: request), (indirect: *((char *)argp + (0 ..))); assigns *((char *)argp + (0 ..)) \from (indirect: fd), (indirect: request), *((char *)argp + (0 ..)); */ extern int __va_ioctl_ptr(int fd, int request, void *argp); /*@ ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1; assigns \result; assigns \result \from (indirect: fd), (indirect: operation); */ extern int flock(int fd, int operation); CODE facilitynames[23] = {{.c_name = "auth", .c_val = 4 << 3}, {.c_name = "authpriv", .c_val = 10 << 3}, {.c_name = "cron", .c_val = 9 << 3}, {.c_name = "daemon", .c_val = 3 << 3}, {.c_name = "ftp", .c_val = 11 << 3}, {.c_name = "kern", .c_val = 0 << 3}, {.c_name = "lpr", .c_val = 6 << 3}, {.c_name = "mail", .c_val = 2 << 3}, {.c_name = "mark", .c_val = 24 | 0}, {.c_name = "news", .c_val = 7 << 3}, {.c_name = "security", .c_val = 4 << 3}, {.c_name = "syslog", .c_val = 5 << 3}, {.c_name = "user", .c_val = 1 << 3}, {.c_name = "uucp", .c_val = 8 << 3}, {.c_name = "local0", .c_val = 16 << 3}, {.c_name = "local1", .c_val = 17 << 3}, {.c_name = "local2", .c_val = 18 << 3}, {.c_name = "local3", .c_val = 19 << 3}, {.c_name = "local4", .c_val = 20 << 3}, {.c_name = "local5", .c_val = 21 << 3}, {.c_name = "local6", .c_val = 22 << 3}, {.c_name = "local7", .c_val = 23 << 3}, {.c_name = (char const *)0, .c_val = -1}}; CODE prioritynames[13] = {{.c_name = "alert", .c_val = 1}, {.c_name = "crit", .c_val = 2}, {.c_name = "debug", .c_val = 7}, {.c_name = "emerg", .c_val = 0}, {.c_name = "err", .c_val = 3}, {.c_name = "error", .c_val = 3}, {.c_name = "info", .c_val = 6}, {.c_name = "none", .c_val = 0x10}, {.c_name = "notice", .c_val = 5}, {.c_name = "panic", .c_val = 0}, {.c_name = "warn", .c_val = 4}, {.c_name = "warning", .c_val = 4}, {.c_name = (char const *)0, .c_val = -1}}; /*@ assigns \nothing; */ extern void closelog(void); /*@ assigns \nothing; */ extern void openlog(char const *, int, int); /*@ assigns \nothing; */ extern int setlogmask(int); /*@ assigns \nothing; */ extern void syslog(int, char const *, void * const *__va_params); /*@ assigns \nothing; */ extern void vsyslog(int, char const *, va_list); /*@ assigns \result; assigns \result \from which, who; */ extern int getpriority(int which, id_t who); /*@ assigns \result; assigns \result \from which, who, prio; */ extern int setpriority(int which, id_t who, int prio); /*@ requires valid_rlp: \valid(rlp); assigns \result, *rlp; assigns \result \from resource; assigns *rlp \from resource; */ extern int getrlimit(int resource, struct rlimit *rlp); /*@ requires valid_r_usage: \valid(r_usage); ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1; assigns *r_usage, \result; assigns *r_usage \from who; assigns \result \from (indirect: who); */ extern int getrusage(int who, struct rusage *r_usage); /*@ requires valid_rlp: \valid_read(rlp); ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1; assigns *rlp, \result; assigns *rlp \from resource; assigns \result \from (indirect: resource), (indirect: *rlp); */ extern int setrlimit(int resource, struct rlimit const *rlp); /*@ requires valid_buffer: \valid(buffer); assigns \result, *buffer; assigns \result \from __fc_time; assigns *buffer \from __fc_time; */ extern clock_t times(struct tms *buffer); /*@ ensures result_ok_or_error: \result ≡ -1 ∨ \result ≥ 0; ensures initialization: stat_loc_init_on_success: \result ≥ 0 ∧ \old(stat_loc) ≢ \null ⇒ \initialized(\old(stat_loc)); assigns \result, *stat_loc; assigns \result \from \nothing; assigns *stat_loc \from \nothing; behavior stat_loc_null: assumes stat_loc_null: stat_loc ≡ \null; assigns \result; assigns \result \from \nothing; behavior stat_loc_non_null: assumes stat_loc_non_null: stat_loc ≢ \null; requires valid_stat_loc: \valid(stat_loc); */ extern pid_t wait(int *stat_loc); /*@ ensures result_ok_or_error: \result ≡ -1 ∨ \result ≥ 0; ensures initialization: stat_loc_init_on_success: \result ≥ 0 ∧ \old(stat_loc) ≢ \null ⇒ \initialized(\old(stat_loc)); assigns \result, *stat_loc; assigns \result \from (indirect: options); assigns *stat_loc \from (indirect: options); behavior stat_loc_null: assumes stat_loc_null: stat_loc ≡ \null; assigns \result; assigns \result \from \nothing; behavior stat_loc_non_null: assumes stat_loc_non_null: stat_loc ≢ \null; requires valid_stat_loc: \valid(stat_loc); */ extern pid_t waitpid(pid_t pid, int *stat_loc, int options); /*@ requires valid_termios_p: \valid(termios_p); assigns \result, *termios_p, Frama_C_entropy_source; assigns \result \from (indirect: fd), (indirect: Frama_C_entropy_source); assigns *termios_p \from (indirect: fd), (indirect: Frama_C_entropy_source); assigns Frama_C_entropy_source \from Frama_C_entropy_source; behavior ok: assumes nondet: Frama_C_entropy_source ≡ 0; ensures initialization: termios_p: \initialized(\old(termios_p)); ensures result_ok: \result ≡ 0; behavior error: assumes nondet: Frama_C_entropy_source ≢ 0; ensures result_error: \result ≡ -1; complete behaviors error, ok; disjoint behaviors error, ok; */ extern int tcgetattr(int fd, struct termios *termios_p); /*@ requires valid_termios_p: \valid(termios_p); ensures result_ok_or_error: \result ≡ 0 ∨ \result ≡ -1; assigns *termios_p, Frama_C_entropy_source, \result; assigns *termios_p \from (indirect: fd), (indirect: optional_actions), (indirect: Frama_C_entropy_source), *termios_p; assigns Frama_C_entropy_source \from Frama_C_entropy_source; assigns \result \from (indirect: fd), (indirect: optional_actions), (indirect: Frama_C_entropy_source), (indirect: *termios_p); */ extern int tcsetattr(int fd, int optional_actions, struct termios *termios_p); void main(void) { /*@ assert __fc_p_fopen ≡ (FILE *)(&__fc_fopen); */ ; /*@ assert __fc_p_opendir ≡ (DIR *)(&__fc_opendir); */ ; /*@ assert __fc_p_time_tm ≡ &__fc_time_tm; */ ; /*@ assert __fc_p_strerror ≡ (char *)__fc_strerror; */ ; return; }