/* Generated by CIL v. 1.2.4 */ /* print_CIL_Input is false */ #define CCURED_SPLIT_ARGUMENTS // #define CCURED_ALLOW_PARTIAL_ELEMENTS_IN_SEQUENCE // #define CCURED_LOG_NON_POINTERS // #define CCURED_USE_STRINGS #define CCURED_FAIL_IS_TERSE #define CCURED_ALWAYS_STOP_ON_ERROR // Include the definition of the checkers #define CCURED #define CCURED_POST #include "ccuredcheck.h" extern unsigned int ___stack_threshhold ; extern unsigned int ___compute_stack_threshhold(void) ; extern void ___stack_overflow(void) ; #line 452 "d:/home/db/postdoc/Blast/ccured/include/ccured.h" struct printf_arguments { int i ; double d ; char * __ROSTRING s ; long long ll ; }; #line 5 "node.h" struct node { int value ; struct node * left ; struct node * right ; }; #line 11 "node.h" typedef struct node HANDLE; #line 220 "C:/cygwin/lib/gcc-lib/i686-pc-cygwin/3.3.1/include/stddef.h" typedef unsigned int size_t; #line 13 "/usr/include/sys/_types.h" typedef long long _off64_t; #line 16 "/usr/include/sys/_types.h" typedef int _ssize_t; #line 361 "C:/cygwin/lib/gcc-lib/i686-pc-cygwin/3.3.1/include/stddef.h" typedef unsigned int wint_t; #line 25 "/usr/include/sys/_types.h" union __anonunion___value_2 { wint_t __wch ; unsigned char ( __wchb)[4] ; }; #line 25 "/usr/include/sys/_types.h" struct __anonstruct__mbstate_t_1 { int __count ; union __anonunion___value_2 __value ; }; #line 25 "/usr/include/sys/_types.h" typedef struct __anonstruct__mbstate_t_1 _mbstate_t; #line 35 "/usr/include/sys/_types.h" typedef int _flock_t; #line 19 "d:/home/db/postdoc/Blast/ccured/include/gcc_3.3.1/sys/reent.h" typedef unsigned long __ULong; #line 40 "d:/home/db/postdoc/Blast/ccured/include/gcc_3.3.1/sys/reent.h" struct _Bigint { struct _Bigint * _next ; int _k ; int _maxwds ; int _sign ; int _wds ; __ULong ( _x)[1] ; }; #line 48 "d:/home/db/postdoc/Blast/ccured/include/gcc_3.3.1/sys/reent.h" 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 ; }; #line 67 "d:/home/db/postdoc/Blast/ccured/include/gcc_3.3.1/sys/reent.h" struct _on_exit_args { void * ( _fnargs)[32] ; __ULong _fntypes ; }; #line 80 "d:/home/db/postdoc/Blast/ccured/include/gcc_3.3.1/sys/reent.h" struct _atexit { struct _atexit * _next ; int _ind ; void (* ( _fns)[32])(void) ; struct _on_exit_args _on_exit_args ; }; #line 95 "d:/home/db/postdoc/Blast/ccured/include/gcc_3.3.1/sys/reent.h" struct __sbuf { unsigned char * _base ; int _size ; }; #line 105 "d:/home/db/postdoc/Blast/ccured/include/gcc_3.3.1/sys/reent.h" typedef long _fpos_t; #line 109 "d:/home/db/postdoc/Blast/ccured/include/gcc_3.3.1/sys/reent.h" typedef _off64_t _fpos64_t; #line 160 struct _reent; #line 208 "d:/home/db/postdoc/Blast/ccured/include/gcc_3.3.1/sys/reent.h" struct __sFILE64 { unsigned char * _p ; int _r ; int _w ; short _flags ; short _file ; struct __sbuf _bf ; int _lbfsize ; struct _reent * _data ; void * _cookie ; _ssize_t ( __attribute__((__cdecl__)) (* _read))(void * _cookie , char * _buf , int _n ) ; _ssize_t ( __attribute__((__cdecl__)) (* _write))(void * _cookie , char * _buf , int _n ) ; _fpos_t ( __attribute__((__cdecl__)) (* _seek))(void * _cookie , _fpos_t _offset , int _whence ) ; int ( __attribute__((__cdecl__)) (* _close))(void * _cookie ) ; struct __sbuf _ub ; unsigned char * _up ; int _ur ; unsigned char ( _ubuf)[3] ; unsigned char ( _nbuf)[1] ; struct __sbuf _lb ; int _blksize ; int _flags2 ; _off64_t _offset ; _fpos64_t ( __attribute__((__cdecl__)) (* _seek64))(void * _cookie , _fpos64_t _offset , int _whence ) ; _flock_t _lock ; }; #line 251 "d:/home/db/postdoc/Blast/ccured/include/gcc_3.3.1/sys/reent.h" typedef struct __sFILE64 __FILE; #line 256 "d:/home/db/postdoc/Blast/ccured/include/gcc_3.3.1/sys/reent.h" struct _glue { struct _glue * _next ; int _niobs ; __FILE * _iobs ; }; #line 284 "d:/home/db/postdoc/Blast/ccured/include/gcc_3.3.1/sys/reent.h" struct _rand48 { unsigned short ( _seed)[3] ; unsigned short ( _mult)[3] ; unsigned short _add ; }; #line 533 "d:/home/db/postdoc/Blast/ccured/include/gcc_3.3.1/sys/reent.h" struct _new_reent { unsigned int _unused_rand ; char * _strtok_last ; char ( _asctime_buf)[26] ; struct __tm _localtime_buf ; int _gamma_signgam ; unsigned long long _rand_next ; struct _rand48 _r48 ; _mbstate_t _mblen_state ; _mbstate_t _mbtowc_state ; _mbstate_t _wctomb_state ; char ( _l64a_buf)[8] ; char ( _signal_buf)[24] ; int _getdate_err ; _mbstate_t _mbrlen_state ; _mbstate_t _mbrtowc_state ; _mbstate_t _mbsrtowcs_state ; _mbstate_t _wcrtomb_state ; _mbstate_t _wcsrtombs_state ; }; #line 533 "d:/home/db/postdoc/Blast/ccured/include/gcc_3.3.1/sys/reent.h" struct __anonstruct__new_3 { struct _new_reent _reent ; char ( _unused)[(int )((2U * sizeof(int )) * 30U - sizeof(struct _new_reent ))] ; }; #line 533 "d:/home/db/postdoc/Blast/ccured/include/gcc_3.3.1/sys/reent.h" struct _reent { int _errno ; __FILE * _stdin ; __FILE * _stdout ; __FILE * _stderr ; int _inc ; char ( _emergency)[25] ; int _current_category ; char * _current_locale ; int __sdidinit ; void ( __attribute__((__cdecl__)) (* __cleanup))(struct _reent * ) ; struct _Bigint * _result ; int _result_k ; struct _Bigint * _p5s ; struct _Bigint * * _freelist ; int _cvtlen ; char * _cvtbuf ; struct __anonstruct__new_3 _new ; struct _atexit * _atexit ; struct _atexit _atexit0 ; void (* * _sig_func)(int ) ; struct _glue __sglue ; __FILE ( __sf)[3] ; }; #line 243 "d:/home/db/postdoc/Blast/ccured/include/ccured_GNUCC.patch" struct __ccured_va_list; #line 50 "d:/home/db/postdoc/Blast/ccured/include/gcc_3.3.1/stdio.h" typedef __FILE FILE; #line 105 "d:/home/db/postdoc/Blast/ccured/include/stdio_wrappers.h" struct scanf_format { int * p_int ; double * p_double ; long * p_long ; unsigned int * p_uint ; unsigned long * p_ulong ; char * p_char ; short * p_short ; }; #line 263 "d:/home/db/postdoc/Blast/ccured/include/ccured_GNUCC.patch" struct __ccured_va_list { int next ; }; #line 129 "d:/home/db/postdoc/Blast/ccured/include/ccuredannot.h" extern void __ccuredInit(void) ; #line 328 "d:/home/db/postdoc/Blast/ccured/include/ccured.h" extern __attribute__((__noreturn__)) void abort_deepcopy(char * errmsg ) ; #line 6 "proc.h" HANDLE * RandTree(int n , int seed , int level ) ; #line 11 int Bimerge(HANDLE * root , int spr_val , int dir ) ; #line 12 int Bisort(HANDLE * root , int spr_val , int dir ) ; #line 4 "ssplain.h" void * ssplain_malloc(int size ) ; #line 5 void * ssplain_calloc(int nelems , int size ) ; #line 6 void ssplain_alloc_stats(void) ; #line 739 "D:/home/db/Software/cygwin/usr/include/sys/reent.h" extern struct _reent * ( __attribute__((__cdecl__)) __getreent)(void) ; #line 56 "d:/home/db/postdoc/Blast/ccured/include/gcc_3.3.1/stdlib.h" extern int ( __attribute__((__cdecl__)) atoi)(char * __nptr ) ; #line 65 extern __attribute__((__noreturn__)) void ( __attribute__((__cdecl__)) exit)(int __status ) ; #line 86 "ssplain.h" void ( __CCUREDFORMAT(1) __CCUREDVARARG(struct printf_arguments ) chatting)(char * s , ...) ; #line 21 "bitonic.c" int flag = 0; #line 21 "bitonic.c" int foo = 0; #line 42 extern int __ccured_va_count ; #line 42 "bitonic.c" static char __string1[11] = #line 42 { '%', 'd', ' ', '@', ' ', '0', 'x', '%', 'x', '\n', '\000'}; #line 33 void InOrder(HANDLE * h ) ; #line 33 "bitonic.c" void InOrder(HANDLE * h ) { HANDLE * l ; HANDLE * r ; int __a_local ; { #line 33 r = (HANDLE */* */)0; #line 33 l = (HANDLE */* */)0; #line 33 if ((unsigned int )(& __a_local) <= ___stack_threshhold) { #line 33 ___stack_overflow(); } { #line 37 if ((unsigned int )h != 0) { #line 39 CHECK_NULL((void *)h); #line 39 l = (HANDLE */* */)h->left; #line 40 r = (HANDLE */* */)h->right; #line 41 InOrder((HANDLE */* */)l); #line 42 __ccured_va_count = -1; #line 42 chatting((char */* */)((char */* */)(& __string1[0])), h->value, (int )((long )h)); #line 43 InOrder((HANDLE */* */)r); } #line 45 return; } #line 33 return; } } #line 47 int mult(int p , int q ) ; #line 47 "bitonic.c" int mult(int p , int q ) { int p1 ; int p0 ; int q1 ; int q0 ; int __retres ; { #line 51 p1 = p / 10000; #line 51 p0 = p % 10000; #line 52 q1 = q / 10000; #line 52 q0 = q % 10000; #line 53 __retres = ((p0 * q1 + p1 * q0) % 10000) * 10000 + p0 * q0; #line 47 return (__retres); } } #line 56 int skiprand(int seed , int n ) ; #line 56 "bitonic.c" int skiprand(int seed , int n ) { int tmp ; int __retres ; int __cil_tmp5 ; { #line 59 while (n) { #line 59 __cil_tmp5 = mult(seed, 31415821); #line 59 tmp = __cil_tmp5; #line 59 seed = tmp + 1; #line 59 n = n - 1; } #line 63 __retres = seed; #line 56 return (__retres); } } extern unsigned int ( __attribute__((__cdecl__)) /*9*/malloc)(size_t __size ) ; #line 75 HANDLE * RandTree(int n , int seed , int level ) ; #line 75 "bitonic.c" HANDLE * RandTree(int n , int seed , int level ) { int volatile ___first_local ; int next_val ; int my_name ; HANDLE * h ; int tmp ; int tmp___0 ; int tmp___2 ; int __a_local ; HANDLE * __retres ; int __cil_tmp13 ; HANDLE * __cil_tmp14 ; HANDLE * __cil_tmp15 ; HANDLE * __cil_tmp17 ; int __cil_tmp18 ; HANDLE * __cil_tmp19 ; { #line 75 __retres = (HANDLE */* */)0; #line 75 h = (HANDLE */* */)0; #line 75 if ((unsigned int )(& __a_local) <= ___stack_threshhold) { #line 75 ___stack_overflow(); } { #line 81 tmp = foo; #line 81 foo = foo + 1; #line 81 my_name = tmp; #line 83 if (n > 1) { #line 86 __cil_tmp13 = mult(seed, 31415821); #line 86 tmp___0 = __cil_tmp13; #line 86 seed = tmp___0 + 1; #line 90 next_val = seed % 100; #line 91 __cil_tmp15 = (HANDLE */* */)/*9*/malloc(((sizeof(struct node ) + 3U) >> 2) << 2); #line 91 if (__cil_tmp15) { #line 91 __cil_tmp14 = __cil_tmp15; #line 91 __cil_tmp15->right = (struct node */* */)0; #line 91 __cil_tmp15->left = (struct node */* */)0; } else { #line 91 __cil_tmp14 = 0; } #line 91 h = __cil_tmp14; #line 91 CHECK_NULL((void *)h); #line 91 h->value = next_val; #line 91 CHECK_STOREPTR((void *)(& h->left), (void *)((struct node */* */)0), (void *)(& ___first_local)); #line 91 h->left = (struct node */* */)0; #line 91 CHECK_STOREPTR((void *)(& h->right), (void *)((struct node */* */)0), (void *)(& ___first_local)); #line 91 h->right = (struct node */* */)0; #line 93 __cil_tmp17 = RandTree(n / 2, seed, level + 1); #line 93 CHECK_NULL((void *)h); #line 93 CHECK_STOREPTR((void *)(& h->left), (void *)((struct node */* */)__cil_tmp17), (void *)(& ___first_local)); #line 93 h->left = (struct node */* */)__cil_tmp17; #line 94 __cil_tmp18 = skiprand(seed, n + 1); #line 94 tmp___2 = __cil_tmp18; #line 94 __cil_tmp19 = RandTree(n / 2, tmp___2, level + 1); #line 94 CHECK_STOREPTR((void *)(& h->right), (void *)((struct node */* */)__cil_tmp19), (void *)(& ___first_local)); #line 94 h->right = (struct node */* */)__cil_tmp19; } else { #line 97 h = (HANDLE */* */)0; } #line 98 CHECK_RETURNPTR((void *)((HANDLE */* */)h), (void *)(& ___first_local)); #line 98 return ((HANDLE */* */)h); } #line 75 CHECK_RETURNPTR((void *)__retres, (void *)(& ___first_local)); #line 75 return (__retres); } } #line 101 void SwapVal(HANDLE * l , HANDLE * r ) ; #line 101 "bitonic.c" void SwapVal(HANDLE * l , HANDLE * r ) { int temp ; { #line 106 CHECK_NULL((void *)l); #line 106 temp = l->value; #line 107 CHECK_NULL((void *)r); #line 107 l->value = r->value; #line 108 r->value = temp; #line 101 return; } } #line 111 void SwapLeft(HANDLE * l , HANDLE * r ) ; #line 111 "bitonic.c" void SwapLeft(HANDLE * l , HANDLE * r ) { int volatile ___first_local ; HANDLE * h ; { #line 119 h = (HANDLE */* */)0; #line 116 CHECK_NULL((void *)r); #line 116 h = (HANDLE */* */)r->left; #line 117 CHECK_NULL((void *)l); #line 117 CHECK_STOREPTR((void *)(& r->left), (void *)l->left, (void *)(& ___first_local)); #line 117 r->left = l->left; #line 118 CHECK_STOREPTR((void *)(& l->left), (void *)((struct node */* */)h), (void *)(& ___first_local)); #line 118 l->left = (struct node */* */)h; #line 111 return; } } #line 121 void SwapRight(HANDLE * l , HANDLE * r ) ; #line 121 "bitonic.c" void SwapRight(HANDLE * l , HANDLE * r ) { int volatile ___first_local ; HANDLE * h ; { #line 129 h = (HANDLE */* */)0; #line 126 CHECK_NULL((void *)r); #line 126 h = (HANDLE */* */)r->right; #line 127 CHECK_NULL((void *)l); #line 127 CHECK_STOREPTR((void *)(& r->right), (void *)l->right, (void *)(& ___first_local)); #line 127 r->right = l->right; #line 128 CHECK_STOREPTR((void *)(& l->right), (void *)((struct node */* */)h), (void *)(& ___first_local)); #line 128 l->right = (struct node */* */)h; #line 121 return; } } #line 131 int Bimerge(HANDLE * root , int spr_val , int dir ) ; #line 131 "bitonic.c" int Bimerge(HANDLE * root , int spr_val , int dir ) { int rightexchange ; int elementexchange ; HANDLE * pl ; HANDLE * pr ; int temp ; int __a_local ; int __retres ; int __cil_tmp11 ; int __cil_tmp12 ; { #line 131 pr = (HANDLE */* */)0; #line 131 pl = (HANDLE */* */)0; #line 131 if ((unsigned int )(& __a_local) <= ___stack_threshhold) { #line 131 ___stack_overflow(); } { #line 139 CHECK_NULL((void *)root); #line 139 rightexchange = (root->value > spr_val) ^ dir; #line 140 if (rightexchange) { #line 143 temp = root->value; #line 144 root->value = spr_val; #line 145 spr_val = temp; } #line 148 pl = (HANDLE */* */)root->left; #line 149 pr = (HANDLE */* */)root->right; #line 151 while ((unsigned int )pl != 0) { #line 153 CHECK_NULL((void *)pl); #line 153 CHECK_NULL((void *)pr); #line 153 elementexchange = (pl->value > pr->value) ^ dir; #line 154 if (rightexchange) { #line 156 if (elementexchange) { #line 158 SwapVal((HANDLE */* */)pl, (HANDLE */* */)pr); #line 159 SwapRight((HANDLE */* */)pl, (HANDLE */* */)pr); #line 160 CHECK_NULL((void *)pl); #line 160 pl = (HANDLE */* */)pl->left; #line 161 CHECK_NULL((void *)pr); #line 161 pr = (HANDLE */* */)pr->left; } else { #line 165 pl = (HANDLE */* */)pl->right; #line 166 pr = (HANDLE */* */)pr->right; } } else { #line 171 if (elementexchange) { #line 173 SwapVal((HANDLE */* */)pl, (HANDLE */* */)pr); #line 174 SwapLeft((HANDLE */* */)pl, (HANDLE */* */)pr); #line 175 CHECK_NULL((void *)pl); #line 175 pl = (HANDLE */* */)pl->right; #line 176 CHECK_NULL((void *)pr); #line 176 pr = (HANDLE */* */)pr->right; } else { #line 180 pl = (HANDLE */* */)pl->left; #line 181 pr = (HANDLE */* */)pr->left; } } } #line 186 CHECK_NULL((void *)root); #line 186 if ((unsigned int )root->left != 0) { #line 188 __cil_tmp11 = Bimerge((HANDLE */* */)root->left, root->value, dir); #line 188 root->value = __cil_tmp11; #line 189 __cil_tmp12 = Bimerge((HANDLE */* */)root->right, spr_val, dir); #line 189 spr_val = __cil_tmp12; } #line 192 return (spr_val); } #line 131 return (__retres); } } #line 195 int Bisort(HANDLE * root , int spr_val , int dir ) ; #line 195 "bitonic.c" int Bisort(HANDLE * root , int spr_val , int dir ) { int val ; int __a_local ; int __retres ; int __cil_tmp7 ; int __cil_tmp8 ; int __cil_tmp9 ; { #line 195 if ((unsigned int )(& __a_local) <= ___stack_threshhold) { #line 195 ___stack_overflow(); } { #line 200 CHECK_NULL((void *)root); #line 200 if ((unsigned int )root->left == 0) { #line 202 if ((root->value > spr_val) ^ dir) { #line 205 val = spr_val; #line 206 spr_val = root->value; #line 207 root->value = val; } } else { #line 213 __cil_tmp7 = Bisort((HANDLE */* */)root->left, root->value, dir); #line 213 root->value = __cil_tmp7; #line 214 __cil_tmp8 = Bisort((HANDLE */* */)root->right, spr_val, ! dir != 0); #line 214 spr_val = __cil_tmp8; #line 215 __cil_tmp9 = Bimerge((HANDLE */* */)root, spr_val, dir); #line 215 spr_val = __cil_tmp9; } #line 218 return (spr_val); } #line 195 return (__retres); } } #line 231 "bitonic.c" struct meta_fseqp_char { void *_e ; } ; #line 231 "bitonic.c" struct fseqp_char { char * __FSEQ _p ; struct meta_fseqp_char _ms ; } ; #line 231 "bitonic.c" typedef struct fseqp_char fseqp_char; #line 231 "bitonic.c" struct meta_fseqp_p_char { void *_e ; } ; #line 231 int dealwithargs_ff(int argc , fseqp_char * __FSEQ argv , void *argv_e ) ; extern void * /*12*/__trusted_cast(unsigned int p ) ; extern unsigned int /*13*/wrapperAlloc(unsigned int ) ; extern struct fseqp_char /*14*/__mkptr_string_fs(char * p ) ; extern void * /*16*/__trusted_deepcast(void * p ) ; struct meta_seq_void { void *_b ; void *_e ; } ; #line 221 "bitonic.c" struct meta_seq_p_char { void *_b ; void *_e ; } ; #line 233 "bitonic.c" static char __string2[21] = #line 233 { 'B', 'i', 's', 'o', 'r', 't', ' ', 'w', 'i', 't', 'h', ' ', '%', 'd', ' ', 's', 'i', 'z', 'e', '\n', '\000'}; #line 242 "bitonic.c" static char __string3[4] = { '%', 'd', '\n', '\000'}; #line 244 "bitonic.c" static char __string4[40] = #line 244 { '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '\n', '\000'}; #line 245 "bitonic.c" static char __string5[39] = #line 245 { 'B', 'E', 'G', 'I', 'N', 'N', 'I', 'N', 'G', ' ', 'B', 'I', 'T', 'O', 'N', 'I', 'C', ' ', 'S', 'O', 'R', 'T', ' ', 'A', 'L', 'G', 'O', 'R', 'I', 'T', 'H', 'M', ' ', 'H', 'E', 'R', 'E', '\n', '\000'}; #line 246 "bitonic.c" static char __string6[40] = #line 246 { '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '*', '\n', '\000'}; #line 248 "bitonic.c" static char __string7[19] = #line 248 { 'S', 'o', 'r', 't', 'i', 'n', 'g', ' ', 'f', 'o', 'r', 'w', 'a', 'r', 'd', '.', '.', '.', '\000'}; #line 251 "bitonic.c" static char __string8[14] = #line 251 { 'S', 'o', 'r', 't', 'e', 'd', ' ', 'T', 'r', 'e', 'e', ':', '\n', '\000'}; #line 253 "bitonic.c" static char __string9[4] = { '%', 'd', '\n', '\000'}; #line 255 "bitonic.c" static char __string10[6] = { 'd', 'o', 'n', 'e', '\n', '\000'}; #line 257 "bitonic.c" static char __string11[20] = #line 257 { 's', 'o', 'r', 't', 'i', 'n', 'g', ' ', 'b', 'a', 'c', 'k', 'w', 'a', 'r', 'd', '.', '.', '.', '\000'}; #line 260 "bitonic.c" static char __string12[14] = #line 260 { 'S', 'o', 'r', 't', 'e', 'd', ' ', 'T', 'r', 'e', 'e', ':', '\n', '\000'}; #line 262 "bitonic.c" static char __string13[4] = { '%', 'd', '\n', '\000'}; #line 264 "bitonic.c" static char __string14[6] = { 'd', 'o', 'n', 'e', '\n', '\000'}; #line 221 void main(int argc , char * __ROSTRING * __argv_input ) ; #line 221 "bitonic.c" void main(int argc , char * __ROSTRING * __argv_input ) { int volatile ___first_local ; struct fseqp_char * __SEQ argv ; HANDLE * h ; int sval ; int n ; int tmp ; int no_mangling9 ; int num_strings10 ; char * * p_argv11 ; unsigned int argvsize12 ; struct fseqp_char * tmp_argv13 ; void * __cil_tmp14 ; struct fseqp_char * __SEQ __cil_tmp15 ; struct fseqp_char * __SEQ __cil_tmp16 ; unsigned int __cil_tmp17 ; struct fseqp_char * __SEQ __cil_tmp18 ; struct fseqp_char __cil_tmp19 ; char * __FSEQ __cil_tmp20 ; void * __cil_tmp22 ; void * __cil_tmp23 ; void * __SEQ __cil_tmp24 ; void * __SEQ __cil_tmp25 ; void * __SEQ __cil_tmp26 ; struct fseqp_char * __SEQ __cil_tmp27 ; unsigned int __cil_tmp28 ; fseqp_char * __FSEQ __cil_tmp29 ; int __cil_tmp30 ; HANDLE * __cil_tmp31 ; int __cil_tmp32 ; int __cil_tmp33 ; int __cil_tmp34 ; void *argv_b44 ; void *argv_e45 ; void *__cil_tmp15_b46 ; void *__cil_tmp15_e47 ; void *__cil_tmp18_b48 ; void *__cil_tmp18_e49 ; void *__cil_tmp20_e50 ; void *__cil_tmp24_b51 ; void *__cil_tmp24_e52 ; void *__cil_tmp25_b53 ; void *__cil_tmp25_e54 ; void *__cil_tmp26_b55 ; void *__cil_tmp26_e56 ; void *__cil_tmp27_b57 ; void *__cil_tmp27_e58 ; void *__cil_tmp29_e59 ; { #line 221 tmp_argv13 = (struct fseqp_char */* */)0; #line 221 p_argv11 = (char * */* */)0; #line 221 h = (HANDLE */* */)0; #line 221 argv_e45 = (void *)0; #line 221 argv_b44 = (void *)0; #line 221 argv = (struct fseqp_char */* __SEQ */)0; { #line 221 no_mangling9 = 0; #line 221 if ((int )__argv_input) { { #line 221 no_mangling9 = 0; #line 221 if (no_mangling9) { { #line 221 no_mangling9 = 0; } } } } else { { #line 221 no_mangling9 = 1; } } #line 221 if (no_mangling9) { { #line 221 __cil_tmp23 = /*16*/__trusted_deepcast((void */* */)__argv_input); #line 221 tmp_argv13 = (struct fseqp_char */* */)__cil_tmp23; #line 221 if ((void */* */)tmp_argv13) { #line 221 __cil_tmp25 = (void */* */)tmp_argv13; #line 221 __cil_tmp25_b53 = (void */* */)tmp_argv13; #line 221 __cil_tmp25_e54 = (void */* */)tmp_argv13 + sizeof((*argv)); #line 221 __cil_tmp24_e52 = __cil_tmp25_e54; #line 221 __cil_tmp24_b51 = __cil_tmp25_b53; #line 221 __cil_tmp24 = __cil_tmp25; } else { #line 221 __cil_tmp26 = 0; #line 221 __cil_tmp26_b55 = (void *)0; #line 221 __cil_tmp26_e56 = (void *)0; #line 221 __cil_tmp24_e52 = __cil_tmp26_e56; #line 221 __cil_tmp24_b51 = __cil_tmp26_b55; #line 221 __cil_tmp24 = __cil_tmp26; } #line 221 CHECK_SEQALIGN(sizeof(struct fseqp_char ), (void *)((struct fseqp_char */* __SEQ */)__cil_tmp24), __cil_tmp24_b51, __cil_tmp24_e52); #line 221 __cil_tmp27 = (struct fseqp_char */* __SEQ */)__cil_tmp24; #line 221 __cil_tmp27_b57 = __cil_tmp24_b51; #line 221 __cil_tmp27_e58 = __cil_tmp24_e52; #line 221 argv_e45 = __cil_tmp27_e58; #line 221 argv_b44 = __cil_tmp27_b57; #line 221 argv = __cil_tmp27; } } else { { #line 221 num_strings10 = 0; #line 221 p_argv11 = (char * */* */)__argv_input; #line 221 while (1) { #line 221 CHECK_NULL((void *)p_argv11); #line 221 if (! ((int )((unsigned int )(*p_argv11)))) { #line 221 break; } { #line 221 num_strings10 = num_strings10 + 1; #line 221 __cil_tmp14 = /*12*/__trusted_cast((unsigned int )((void */* */)((long )p_argv11 + sizeof((*__argv_input))))); #line 221 p_argv11 = (char * */* */)__cil_tmp14; } } #line 221 argvsize12 = (unsigned int )((1 + num_strings10) * sizeof((*argv))); #line 221 __cil_tmp16 = (struct fseqp_char */* __SEQ */)/*13*/wrapperAlloc(((argvsize12 + 3U) >> 2) << 2); #line 221 if (__cil_tmp16) { #line 221 __cil_tmp15 = __cil_tmp16; #line 221 __cil_tmp15_b46 = (void *)__cil_tmp16; #line 221 __cil_tmp17 = (unsigned int )__cil_tmp16 + (((argvsize12 + 3U) >> 2) << 2); while ((unsigned int )__cil_tmp16 + sizeof(struct fseqp_char ) <= __cil_tmp17) { #line 221 __cil_tmp16->_ms._e = (void *)0; #line 221 __cil_tmp16->_p = (char */* __FSEQ */)0; #line 221 __cil_tmp16 = __cil_tmp16 + 1; } #line 221 __cil_tmp15_e47 = __cil_tmp16; } else { #line 221 __cil_tmp15 = 0; #line 221 __cil_tmp15_b46 = (void *)0; #line 221 __cil_tmp15_e47 = (void *)0; } #line 221 __cil_tmp18 = __cil_tmp15; #line 221 __cil_tmp18_b48 = __cil_tmp15_b46; #line 221 __cil_tmp18_e49 = __cil_tmp15_e47; #line 221 argv_e45 = __cil_tmp18_e49; #line 221 argv_b44 = __cil_tmp18_b48; #line 221 argv = __cil_tmp18; #line 221 while (num_strings10 >= 0) { { #line 221 CHECK_NULL((void *)p_argv11); #line 221 __cil_tmp19 = /*14*/__mkptr_string_fs((char */* */)(*p_argv11)); #line 221 __cil_tmp20 = __cil_tmp19._p; #line 221 __cil_tmp20_e50 = __cil_tmp19._ms._e; #line 221 CHECK_SEQ2SAFE(argv_b44, argv_e45, (void *)(argv + num_strings10), sizeof(struct fseqp_char ), sizeof(struct fseqp_char ), 1, 0); #line 221 CHECK_STOREPTR((void *)(argv + num_strings10), __cil_tmp20_e50, (void *)(& ___first_local)); #line 221 (argv + num_strings10)->_ms._e = __cil_tmp20_e50; #line 221 (argv + num_strings10)->_p = __cil_tmp20; #line 221 __cil_tmp22 = /*12*/__trusted_cast((unsigned int )((void */* */)((long )p_argv11 - sizeof((*__argv_input))))); #line 221 p_argv11 = (char * */* */)__cil_tmp22; #line 221 num_strings10 = num_strings10 - 1; } } } } } #line 221 __ccuredAlwaysStopOnError = 1; #line 221 __ccuredUseStrings = 0; #line 221 __ccuredLogNonPointers = 0; #line 221 __ccuredInit(); #line 221 __cil_tmp28 = ___compute_stack_threshhold(); #line 221 ___stack_threshhold = __cil_tmp28; { #line 231 CHECK_SEQ2FSEQ(argv_b44, argv_e45, (void *)argv); #line 231 __cil_tmp29 = (fseqp_char */* __FSEQ */)argv; #line 231 __cil_tmp29_e59 = argv_e45; #line 231 __cil_tmp30 = dealwithargs_ff(argc, __cil_tmp29, __cil_tmp29_e59); #line 231 n = __cil_tmp30; #line 233 __ccured_va_count = -1; #line 233 chatting((char */* */)((char */* */)(& __string2[0])), n); #line 234 __cil_tmp31 = RandTree(n, 12345768, 0); #line 234 h = (HANDLE */* */)__cil_tmp31; #line 236 __cil_tmp32 = mult(245867, 31415821); #line 236 tmp = __cil_tmp32; #line 236 sval = (tmp + 1) % 100; #line 240 if (flag) { #line 241 InOrder((HANDLE */* */)h); #line 242 __ccured_va_count = -1; #line 242 chatting((char */* */)((char */* */)(& __string3[0])), sval); } #line 244 __ccured_va_count = -1; #line 244 chatting((char */* */)((char */* */)(& __string4[0]))); #line 245 __ccured_va_count = -1; #line 245 chatting((char */* */)((char */* */)(& __string5[0]))); #line 246 __ccured_va_count = -1; #line 246 chatting((char */* */)((char */* */)(& __string6[0]))); #line 248 __ccured_va_count = -1; #line 248 chatting((char */* */)((char */* */)(& __string7[0]))); #line 249 __cil_tmp33 = Bisort((HANDLE */* */)h, sval, 0); #line 249 sval = __cil_tmp33; #line 250 if (flag) { #line 251 __ccured_va_count = -1; #line 251 chatting((char */* */)((char */* */)(& __string8[0]))); #line 252 InOrder((HANDLE */* */)h); #line 253 __ccured_va_count = -1; #line 253 chatting((char */* */)((char */* */)(& __string9[0])), sval); } #line 255 __ccured_va_count = -1; #line 255 chatting((char */* */)((char */* */)(& __string10[0]))); #line 257 __ccured_va_count = -1; #line 257 chatting((char */* */)((char */* */)(& __string11[0]))); #line 258 __cil_tmp34 = Bisort((HANDLE */* */)h, sval, 1); #line 258 sval = __cil_tmp34; #line 259 if (flag) { #line 260 __ccured_va_count = -1; #line 260 chatting((char */* */)((char */* */)(& __string12[0]))); #line 261 InOrder((HANDLE */* */)h); #line 262 __ccured_va_count = -1; #line 262 chatting((char */* */)((char */* */)(& __string13[0])), sval); } #line 264 __ccured_va_count = -1; #line 264 chatting((char */* */)((char */* */)(& __string14[0]))); #line 265 exit(0); } #line 221 return; } } #line 7 "args.c" int mylog(int num ) ; #line 7 "args.c" int mylog(int num ) { int j ; int k ; int __retres ; { #line 9 j = 0; #line 9 k = 1; #line 11 while (k < num) { #line 11 k = k * 2; #line 11 j = j + 1; } #line 12 __retres = j; #line 7 return (__retres); } } __inline static int /*18*/atoi_wrapper_f(char * __FSEQ str , void *str_e ) ; #line 16 int dealwithargs_ff(int argc , fseqp_char * __FSEQ argv , void *argv_e ) ; #line 16 "args.c" int dealwithargs_ff(int argc , fseqp_char * __FSEQ argv , void *argv_e ) { int size ; int __retres ; char * __FSEQ __cil_tmp5 ; int __cil_tmp6 ; char * __FSEQ __cil_tmp7 ; int __cil_tmp8 ; void *__cil_tmp5_e13 ; void *__cil_tmp7_e14 ; { #line 20 if (argc > 2) { #line 21 CHECK_FSEQARITH2SAFE((void *)argv, argv_e, (void *)(argv + 2), sizeof(fseqp_char ), sizeof(fseqp_char ), 1, 0); #line 21 __cil_tmp5 = (argv + 2)->_p; #line 21 __cil_tmp5_e13 = (argv + 2)->_ms._e; #line 21 __cil_tmp6 = /*18*/atoi_wrapper_f(__cil_tmp5, __cil_tmp5_e13); #line 21 flag = __cil_tmp6; } else { #line 23 flag = 0; } #line 25 if (argc > 1) { #line 26 CHECK_FSEQARITH2SAFE((void *)argv, argv_e, (void *)(argv + 1), sizeof(fseqp_char ), sizeof(fseqp_char ), 1, 0); #line 26 __cil_tmp7 = (argv + 1)->_p; #line 26 __cil_tmp7_e14 = (argv + 1)->_ms._e; #line 26 __cil_tmp8 = /*18*/atoi_wrapper_f(__cil_tmp7, __cil_tmp7_e14); #line 26 size = __cil_tmp8; } else { #line 28 size = 16; } #line 30 __retres = size; #line 16 return (__retres); } } #line 201 "d:/home/db/postdoc/Blast/ccured/include/gcc_3.3.1/stdio.h" extern int ( __CCUREDFORMAT(1) __CCUREDVARARG(struct printf_arguments ) __attribute__((__cdecl__)) printf)(char * , ...) ; #line 204 extern int ( __CCUREDFORMAT(2) __CCUREDVARARG(struct printf_arguments ) __attribute__((__cdecl__)) vfprintf_ssvs)(FILE * , char * , struct __ccured_va_list * ) ; #line 264 "d:/home/db/postdoc/Blast/ccured/include/ccured_GNUCC.patch" extern void __ccured_va_start_vs(struct __ccured_va_list * , unsigned long ) ; #line 267 extern void __ccured_va_end_vs(struct __ccured_va_list * ) ; #line 9 "ssplain.c" struct __ccured_va_localinfo { int next ; int count ; int tags[32] ; void * nextp ; }; #line 9 void ( __CCUREDFORMAT(1) __CCUREDVARARG(struct printf_arguments ) chatting)(char * s , ...) ; #line 9 "ssplain.c" void ( __CCUREDFORMAT(1) __CCUREDVARARG(struct printf_arguments ) chatting)(char * s , ...) { struct __ccured_va_list * ap ; unsigned long tmp ; struct _reent * tmp___0 ; struct __ccured_va_localinfo ap__vainfo5 ; unsigned long __cil_tmp7 ; struct _reent * __cil_tmp8 ; { #line 15 ap__vainfo5.nextp = (void */* */)0; #line 15 tmp___0 = (struct _reent */* */)0; #line 15 ap = (struct __ccured_va_list */* */)0; #line 9 ap = (struct __ccured_va_list */* */)(& ap__vainfo5); #line 12 __cil_tmp7 = GCC_STDARG_START(s); #line 12 tmp = __cil_tmp7; #line 12 __ccured_va_start_vs((struct __ccured_va_list */* */)ap, tmp); #line 13 __cil_tmp8 = __getreent(); #line 13 tmp___0 = (struct _reent */* */)__cil_tmp8; #line 13 CHECK_NULL((void *)tmp___0); #line 13 vfprintf_ssvs((FILE */* */)tmp___0->_stderr, (char */* */)((char */* */)s), (struct __ccured_va_list */* */)ap); #line 14 __ccured_va_end_vs((struct __ccured_va_list */* */)ap); #line 9 return; } } #line 41 "ssplain.c" static unsigned long bytes_allocated = 0UL; #line 42 "ssplain.c" static unsigned long allocations = 0UL; #line 44 void * ssplain_malloc(int size ) ; #line 44 "ssplain.c" void * ssplain_malloc(int size ) { int volatile ___first_local ; void * tmp ; void * __retres ; void * __cil_tmp4 ; void * __cil_tmp5 ; { #line 49 __retres = (void */* */)0; #line 49 tmp = (void */* */)0; #line 47 allocations = allocations + 1UL; #line 48 bytes_allocated = bytes_allocated + (unsigned long )size; #line 49 __cil_tmp5 = (void */* */)/*9*/malloc((((unsigned int )size + 3U) >> 2) << 2); #line 49 if (__cil_tmp5) { #line 49 __cil_tmp4 = __cil_tmp5; #line 49 CHECK_POSITIVE((int )((((unsigned int )size + 3U) >> 2) << 2) - (int )sizeof(void )); } else { #line 49 __cil_tmp4 = 0; } #line 49 tmp = __cil_tmp4; #line 49 __retres = (void */* */)tmp; #line 44 CHECK_RETURNPTR((void *)__retres, (void *)(& ___first_local)); #line 44 return (__retres); } } extern unsigned int ( __attribute__((__cdecl__)) /*21*/calloc)(size_t __nmemb , size_t __size ) ; #line 59 "ssplain.c" static char __string15[19] = #line 59 { 'A', 'l', 'l', 'o', 'c', 'a', 't', 'i', 'o', 'n', ' ', 'f', 'a', 'i', 'l', 'e', 'd', '\n', '\000'}; #line 52 void * ssplain_calloc(int nelems , int size ) ; #line 52 "ssplain.c" void * ssplain_calloc(int nelems , int size ) { int volatile ___first_local ; void * p ; void * __retres ; void * __cil_tmp5 ; void * __cil_tmp6 ; { #line 60 __retres = (void */* */)0; #line 60 p = (void */* */)0; #line 56 allocations = allocations + 1UL; #line 57 bytes_allocated = bytes_allocated + (unsigned long )(nelems * size); #line 58 __cil_tmp6 = (void */* */)/*21*/calloc(1, (((unsigned int )((unsigned int )nelems * (unsigned int )size) + 3U) >> 2) << 2); #line 58 if (__cil_tmp6) { #line 58 __cil_tmp5 = __cil_tmp6; #line 58 CHECK_POSITIVE((int )((((unsigned int )((unsigned int )nelems * (unsigned int )size) + 3U) >> 2) << 2) - (int )sizeof(void )); } else { #line 58 __cil_tmp5 = 0; } #line 58 p = __cil_tmp5; #line 59 if (! ((int )p)) { #line 59 __ccured_va_count = -1; #line 59 printf((char */* */)(& __string15[0])); #line 59 exit(3); } #line 60 __retres = (void */* */)p; #line 52 CHECK_RETURNPTR((void *)__retres, (void *)(& ___first_local)); #line 52 return (__retres); } } #line 66 "ssplain.c" static char __string16[56] = #line 66 { 'A', 'l', 'l', 'o', 'c', 'a', 't', 'i', 'o', 'n', ' ', 's', 't', 'a', 't', 's', ':', ' ', '%', 'd', ' ', 'b', 'y', 't', 'e', 's', ' ', 'a', 'l', 'l', 'o', 'c', 'a', 't', 'e', 'd', ' ', 'i', 'n', ' ', '%', 'd', ' ', 'a', 'l', 'l', 'o', 'c', 'a', 't', 'i', 'o', 'n', 's', '\n', '\000'}; #line 63 void ssplain_alloc_stats(void) ; #line 63 "ssplain.c" void ssplain_alloc_stats(void) { { #line 66 __ccured_va_count = -1; #line 66 chatting((char */* */)((char */* */)(& __string16[0])), (int )bytes_allocated, (int )allocations); #line 63 return; } } extern void /*22*/__verify_nul_f(char * __FSEQ ptr_p , void *ptr_ms_e ) ; __inline static int /*18*/atoi_wrapper_f(char * __FSEQ str , void *str_e ) ; __inline static int /*18*/atoi_wrapper_f(char * __FSEQ str , void *str_e ) { char * tmp ; int tmp___0 ; int __retres ; char * __FSEQ __cil_tmp5 ; void * __cil_tmp6 ; int __cil_tmp7 ; void *__cil_tmp5_e11 ; { #line 60 "d:/home/db/postdoc/Blast/ccured/include/stdlib_wrappers.h" tmp = (char */* */)0; #line 59 __cil_tmp5 = str; #line 59 __cil_tmp5_e11 = str_e; #line 59 /*22*/__verify_nul_f(__cil_tmp5, __cil_tmp5_e11); #line 60 if ((void */* __FSEQ */)str) { #line 60 CHECK_FSEQ2SAFE(str_e, (void *)((void */* __FSEQ */)str), sizeof(void ), sizeof(void ), 1, 0); } #line 60 __cil_tmp6 = (void */* __FSEQ */)str; #line 60 tmp = (char */* */)__cil_tmp6; #line 60 __cil_tmp7 = atoi((char */* */)((char */* */)tmp)); #line 60 tmp___0 = __cil_tmp7; #line 60 __retres = tmp___0; return (__retres); } }