/* 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 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 220 "C:/cygwin/lib/gcc-lib/i686-pc-cygwin/3.3.1/include/stddef.h" typedef unsigned int size_t; #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 5 "hash.h" struct hash_entry { unsigned int key ; void * entry ; struct hash_entry * next ; unsigned int padding ; }; #line 12 "hash.h" struct meta_fseqp_p_s_hash_entry { void *_e ; } ; #line 12 "hash.h" struct fseqp_p_s_hash_entry { struct hash_entry * * __FSEQ _p ; struct meta_fseqp_p_s_hash_entry _ms ; } ; #line 12 "hash.h" typedef struct fseqp_p_s_hash_entry fseqp_p_s_hash_entry; #line 12 "hash.h" struct hash { fseqp_p_s_hash_entry array ; int (* mapfunc)(unsigned int ) ; int size ; unsigned int padding ; }; #line 16 "mst.h" struct meta_fseqp_s_vert_st { void *_e ; } ; #line 16 "mst.h" struct fseqp_s_vert_st { struct vert_st * __FSEQ _p ; struct meta_fseqp_s_vert_st _ms ; } ; #line 16 "mst.h" typedef struct fseqp_s_vert_st fseqp_s_vert_st; #line 16 "mst.h" struct vert_st { int mindist ; fseqp_s_vert_st next ; struct hash * edgehash ; unsigned int padding ; }; #line 23 "mst.h" struct graph_st { struct fseqp_s_vert_st vlist ; }; #line 7 "main.c" struct blue_return { struct vert_st * vert ; int dist ; }; #line 7 "main.c" typedef struct blue_return BlueReturn; #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 739 "D:/home/db/Software/cygwin/usr/include/sys/reent.h" extern struct _reent * ( __attribute__((__cdecl__)) __getreent)(void) ; #line 26 "d:/home/db/postdoc/Blast/ccured/include/gcc_3.3.1/string.h" extern void * ( __attribute__((__cdecl__)) memset)(void * , int , size_t ) ; #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 204 "d:/home/db/postdoc/Blast/ccured/include/gcc_3.3.1/stdio.h" 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 19 "hash.h" struct hash * MakeHash(int size , int (* map)(unsigned int ) ) ; #line 20 void * HashLookup(unsigned int key , struct hash * hash ) ; #line 21 void HashInsert(void * entry , unsigned int key , struct hash * hash ) ; #line 22 void HashDelete(unsigned int key , struct hash * hash ) ; #line 27 "mst.h" struct graph_st * MakeGraph(int numvert ) ; #line 31 void ( __CCUREDFORMAT(1) __CCUREDVARARG(struct printf_arguments ) chatting)(char * s , ...) ; #line 38 "main.c" extern int __ccured_va_count ; #line 38 "main.c" static char __string1[11] = #line 38 { 'N', 'o', 't', ' ', 'f', 'o', 'u', 'n', 'd', '\n', '\000'}; #line 69 "main.c" static char __string2[11] = #line 69 { 'N', 'o', 't', ' ', 'f', 'o', 'u', 'n', 'd', '\n', '\000'}; #line 12 static BlueReturn BlueRule(struct vert_st * inserted , struct vert_st * vlist ) ; #line 12 "main.c" static BlueReturn BlueRule(struct vert_st * inserted , struct vert_st * vlist ) { int volatile ___first_local ; BlueReturn retval ; struct vert_st * tmp ; struct vert_st * prev ; struct hash * hash ; int dist ; int dist2 ; int count ; struct vert_st * __FSEQ next ; BlueReturn __retres ; void * __cil_tmp14 ; void * __cil_tmp15 ; struct vert_st * __FSEQ __cil_tmp16 ; struct vert_st * __FSEQ __cil_tmp17 ; void *next_e22 ; void *__cil_tmp16_e23 ; void *__cil_tmp17_e24 ; { #line 79 __retres.vert = (struct vert_st */* */)0; #line 79 next_e22 = (void *)0; #line 79 next = (struct vert_st */* __FSEQ */)0; #line 79 hash = (struct hash */* */)0; #line 79 prev = (struct vert_st */* */)0; #line 79 tmp = (struct vert_st */* */)0; #line 79 retval.vert = (struct vert_st */* */)0; #line 20 if (! ((int )vlist)) { #line 21 retval.dist = 999999; #line 22 __retres = retval; goto return_label; } #line 24 prev = (struct vert_st */* */)vlist; #line 25 retval.vert = (struct vert_st */* */)vlist; #line 26 CHECK_NULL((void *)vlist); #line 26 retval.dist = vlist->mindist; #line 27 CHECK_NULL((void *)vlist); #line 27 hash = (struct hash */* */)vlist->edgehash; #line 28 __cil_tmp14 = HashLookup((unsigned int )inserted, (struct hash */* */)hash); #line 28 dist = (int )__cil_tmp14; #line 30 if (dist) { #line 32 if (dist < retval.dist) { #line 34 CHECK_NULL((void *)vlist); #line 34 vlist->mindist = dist; #line 35 retval.dist = dist; } } else { #line 38 __ccured_va_count = -1; #line 38 chatting((char */* */)((char */* */)(& __string1[0]))); } #line 40 count = 0; #line 43 CHECK_NULL((void *)vlist); #line 43 CHECK_FSEQ2SAFE(vlist->next._ms._e, (void *)vlist->next._p, sizeof(struct vert_st ), sizeof(struct vert_st ), 0, 0); #line 43 tmp = (struct vert_st */* */)vlist->next._p; #line 43 while ((int )tmp) { #line 45 count = count + 1; #line 48 if ((unsigned int )tmp == (unsigned int )inserted) { #line 51 CHECK_NULL((void *)tmp); #line 51 __cil_tmp16 = tmp->next._p; #line 51 __cil_tmp16_e23 = tmp->next._ms._e; #line 51 next_e22 = __cil_tmp16_e23; #line 51 next = __cil_tmp16; #line 52 CHECK_NULL((void *)prev); #line 52 __cil_tmp17 = next; #line 52 __cil_tmp17_e24 = next_e22; #line 52 CHECK_STOREPTR((void *)(& prev->next), __cil_tmp17_e24, (void *)(& ___first_local)); #line 52 prev->next._ms._e = __cil_tmp17_e24; #line 52 prev->next._p = __cil_tmp17; } else { #line 57 CHECK_NULL((void *)tmp); #line 57 hash = (struct hash */* */)tmp->edgehash; #line 58 CHECK_NULL((void *)tmp); #line 58 dist2 = tmp->mindist; #line 59 __cil_tmp15 = HashLookup((unsigned int )inserted, (struct hash */* */)hash); #line 59 dist = (int )__cil_tmp15; #line 61 if (dist) { #line 63 if (dist < dist2) { #line 65 CHECK_NULL((void *)tmp); #line 65 tmp->mindist = dist; #line 66 dist2 = dist; } } else { #line 69 __ccured_va_count = -1; #line 69 chatting((char */* */)((char */* */)(& __string2[0]))); } #line 70 if (dist2 < retval.dist) { #line 72 retval.vert = (struct vert_st */* */)tmp; #line 73 retval.dist = dist2; } } #line 43 prev = (struct vert_st */* */)tmp; #line 43 CHECK_NULL((void *)tmp); #line 43 CHECK_FSEQ2SAFE(tmp->next._ms._e, (void *)tmp->next._p, sizeof(struct vert_st ), sizeof(struct vert_st ), 0, 0); #line 43 tmp = (struct vert_st */* */)tmp->next._p; } #line 79 __retres = retval; return_label: /* CIL Label */ #line 12 CHECK_RETURNPTR((void *)__retres.vert, (void *)(& ___first_local)); #line 12 return (__retres); } } #line 84 "main.c" static struct vert_st * MyVertexList = (struct vert_st */* */)0; #line 92 "main.c" static char __string3[17] = #line 92 { 'C', 'o', 'm', 'p', 'u', 't', 'e', ' ', 'p', 'h', 'a', 's', 'e', ' ', '1', '\n', '\000'}; #line 102 "main.c" static char __string4[17] = #line 102 { 'C', 'o', 'm', 'p', 'u', 't', 'e', ' ', 'p', 'h', 'a', 's', 'e', ' ', '2', '\n', '\000'}; #line 86 static int ComputeMst(struct graph_st * graph , int numvert ) ; #line 86 "main.c" static int ComputeMst(struct graph_st * graph , int numvert ) { int volatile ___first_local ; struct vert_st * inserted ; struct vert_st * __FSEQ tmp ; int cost ; int dist ; BlueReturn br ; int __retres ; struct vert_st * __FSEQ __cil_tmp9 ; struct vert_st * __FSEQ __cil_tmp10 ; BlueReturn __cil_tmp12 ; void *tmp_e16 ; void *__cil_tmp9_e17 ; void *__cil_tmp10_e18 ; { #line 115 br.vert = (struct vert_st */* */)0; #line 115 tmp_e16 = (void *)0; #line 115 tmp = (struct vert_st */* __FSEQ */)0; #line 115 inserted = (struct vert_st */* */)0; #line 89 cost = 0; #line 92 __ccured_va_count = -1; #line 92 chatting((char */* */)((char */* */)(& __string3[0]))); #line 95 CHECK_NULL((void *)graph); #line 95 CHECK_FSEQ2SAFE(graph->vlist._ms._e, (void *)graph->vlist._p, sizeof(struct vert_st ), sizeof(struct vert_st ), 0, 0); #line 95 inserted = (struct vert_st */* */)graph->vlist._p; #line 96 CHECK_NULL((void *)inserted); #line 96 __cil_tmp9 = inserted->next._p; #line 96 __cil_tmp9_e17 = inserted->next._ms._e; #line 96 tmp_e16 = __cil_tmp9_e17; #line 96 tmp = __cil_tmp9; #line 97 CHECK_NULL((void *)graph); #line 97 __cil_tmp10 = tmp; #line 97 __cil_tmp10_e18 = tmp_e16; #line 97 CHECK_STOREPTR((void *)(& graph->vlist), __cil_tmp10_e18, (void *)(& ___first_local)); #line 97 graph->vlist._ms._e = __cil_tmp10_e18; #line 97 graph->vlist._p = __cil_tmp10; #line 98 CHECK_FSEQ2SAFE(tmp_e16, (void *)tmp, sizeof(struct vert_st ), sizeof(struct vert_st ), 0, 0); #line 98 CHECK_STOREPTR((void *)(& MyVertexList), (void *)((struct vert_st */* */)tmp), (void *)(& ___first_local)); #line 98 MyVertexList = (struct vert_st */* */)tmp; #line 99 numvert = numvert - 1; #line 102 __ccured_va_count = -1; #line 102 chatting((char */* */)((char */* */)(& __string4[0]))); #line 103 while (numvert) { #line 107 if ((unsigned int )inserted == (unsigned int )MyVertexList) { #line 108 CHECK_NULL((void *)MyVertexList); #line 108 CHECK_FSEQ2SAFE(MyVertexList->next._ms._e, (void *)MyVertexList->next._p, sizeof(struct vert_st ), sizeof(struct vert_st ), 0, 0); #line 108 CHECK_STOREPTR((void *)(& MyVertexList), (void *)((struct vert_st */* */)MyVertexList->next._p), (void *)(& ___first_local)); #line 108 MyVertexList = (struct vert_st */* */)MyVertexList->next._p; } #line 109 __cil_tmp12 = BlueRule((struct vert_st */* */)inserted, (struct vert_st */* */)MyVertexList); #line 109 br = __cil_tmp12; #line 110 inserted = (struct vert_st */* */)br.vert; #line 111 dist = br.dist; #line 112 numvert = numvert - 1; #line 113 cost = cost + dist; } #line 115 __retres = cost; #line 86 return (__retres); } } #line 118 "main.c" struct meta_fseqp_char { void *_e ; } ; #line 118 "main.c" struct fseqp_char { char * __FSEQ _p ; struct meta_fseqp_char _ms ; } ; #line 118 "main.c" typedef struct fseqp_char fseqp_char; #line 118 "main.c" struct meta_fseqp_p_char { void *_e ; } ; #line 118 int dealwithargs_ff(int argc , fseqp_char * __FSEQ argv , void *argv_e ) ; extern void * /*11*/__trusted_cast(unsigned int p ) ; extern unsigned int /*12*/wrapperAlloc(unsigned int ) ; extern struct fseqp_char /*13*/__mkptr_string_fs(char * p ) ; extern void * /*15*/__trusted_deepcast(void * p ) ; struct meta_seq_void { void *_b ; void *_e ; } ; #line 120 "main.c" struct meta_seq_p_char { void *_b ; void *_e ; } ; #line 126 "main.c" static char __string5[22] = #line 126 { 'H', 'a', 's', 'h', ' ', 'e', 'n', 't', 'r', 'y', ' ', 's', 'i', 'z', 'e', ' ', '=', ' ', '%', 'd', '\n', '\000'}; #line 127 "main.c" static char __string6[16] = #line 127 { 'H', 'a', 's', 'h', ' ', 's', 'i', 'z', 'e', ' ', '=', ' ', '%', 'd', '\n', '\000'}; #line 128 "main.c" static char __string7[18] = #line 128 { 'V', 'e', 'r', 't', 'e', 'x', ' ', 's', 'i', 'z', 'e', ' ', '=', ' ', '%', 'd', '\n', '\000'}; #line 132 "main.c" static char __string8[25] = #line 132 { 'M', 'a', 'k', 'i', 'n', 'g', ' ', 'g', 'r', 'a', 'p', 'h', ' ', 'o', 'f', ' ', 's', 'i', 'z', 'e', ' ', '%', 'd', '\n', '\000'}; #line 134 "main.c" static char __string9[17] = #line 134 { 'G', 'r', 'a', 'p', 'h', ' ', 'c', 'o', 'm', 'p', 'l', 'e', 't', 'e', 'd', '\n', '\000'}; #line 136 "main.c" static char __string10[23] = #line 136 { 'A', 'b', 'o', 'u', 't', ' ', 't', 'o', ' ', 'c', 'o', 'm', 'p', 'u', 't', 'e', ' ', 'm', 's', 't', ' ', '\n', '\000'}; #line 139 "main.c" static char __string11[17] = #line 139 { 'M', 'S', 'T', ' ', 'h', 'a', 's', ' ', 'c', 'o', 's', 't', ' ', '%', 'd', '\n', '\000'}; #line 120 int main(int argc , char * __ROSTRING * __argv_input ) ; #line 120 "main.c" int main(int argc , char * __ROSTRING * __argv_input ) { int volatile ___first_local ; struct fseqp_char * __SEQ argv ; struct graph_st * graph ; int dist ; int size ; int no_mangling8 ; int num_strings9 ; char * * p_argv10 ; unsigned int argvsize11 ; struct fseqp_char * tmp_argv12 ; int __retres ; 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 ; struct graph_st * __cil_tmp31 ; int __cil_tmp32 ; void *argv_b42 ; void *argv_e43 ; void *__cil_tmp15_b44 ; void *__cil_tmp15_e45 ; void *__cil_tmp18_b46 ; void *__cil_tmp18_e47 ; void *__cil_tmp20_e48 ; void *__cil_tmp24_b49 ; void *__cil_tmp24_e50 ; void *__cil_tmp25_b51 ; void *__cil_tmp25_e52 ; void *__cil_tmp26_b53 ; void *__cil_tmp26_e54 ; void *__cil_tmp27_b55 ; void *__cil_tmp27_e56 ; void *__cil_tmp29_e57 ; { #line 120 tmp_argv12 = (struct fseqp_char */* */)0; #line 120 p_argv10 = (char * */* */)0; #line 120 graph = (struct graph_st */* */)0; #line 120 argv_e43 = (void *)0; #line 120 argv_b42 = (void *)0; #line 120 argv = (struct fseqp_char */* __SEQ */)0; { #line 120 no_mangling8 = 0; #line 120 if ((int )__argv_input) { { #line 120 no_mangling8 = 0; #line 120 if (no_mangling8) { { #line 120 no_mangling8 = 0; } } } } else { { #line 120 no_mangling8 = 1; } } #line 120 if (no_mangling8) { { #line 120 __cil_tmp23 = /*15*/__trusted_deepcast((void */* */)__argv_input); #line 120 tmp_argv12 = (struct fseqp_char */* */)__cil_tmp23; #line 120 if ((void */* */)tmp_argv12) { #line 120 __cil_tmp25 = (void */* */)tmp_argv12; #line 120 __cil_tmp25_b51 = (void */* */)tmp_argv12; #line 120 __cil_tmp25_e52 = (void */* */)tmp_argv12 + sizeof((*argv)); #line 120 __cil_tmp24_e50 = __cil_tmp25_e52; #line 120 __cil_tmp24_b49 = __cil_tmp25_b51; #line 120 __cil_tmp24 = __cil_tmp25; } else { #line 120 __cil_tmp26 = 0; #line 120 __cil_tmp26_b53 = (void *)0; #line 120 __cil_tmp26_e54 = (void *)0; #line 120 __cil_tmp24_e50 = __cil_tmp26_e54; #line 120 __cil_tmp24_b49 = __cil_tmp26_b53; #line 120 __cil_tmp24 = __cil_tmp26; } #line 120 CHECK_SEQALIGN(sizeof(struct fseqp_char ), (void *)((struct fseqp_char */* __SEQ */)__cil_tmp24), __cil_tmp24_b49, __cil_tmp24_e50); #line 120 __cil_tmp27 = (struct fseqp_char */* __SEQ */)__cil_tmp24; #line 120 __cil_tmp27_b55 = __cil_tmp24_b49; #line 120 __cil_tmp27_e56 = __cil_tmp24_e50; #line 120 argv_e43 = __cil_tmp27_e56; #line 120 argv_b42 = __cil_tmp27_b55; #line 120 argv = __cil_tmp27; } } else { { #line 120 num_strings9 = 0; #line 120 p_argv10 = (char * */* */)__argv_input; #line 120 while (1) { #line 120 CHECK_NULL((void *)p_argv10); #line 120 if (! ((int )((unsigned int )(*p_argv10)))) { #line 120 break; } { #line 120 num_strings9 = num_strings9 + 1; #line 120 __cil_tmp14 = /*11*/__trusted_cast((unsigned int )((void */* */)((long )p_argv10 + sizeof((*__argv_input))))); #line 120 p_argv10 = (char * */* */)__cil_tmp14; } } #line 120 argvsize11 = (unsigned int )((1 + num_strings9) * sizeof((*argv))); #line 120 __cil_tmp16 = (struct fseqp_char */* __SEQ */)/*12*/wrapperAlloc(((argvsize11 + 3U) >> 2) << 2); #line 120 if (__cil_tmp16) { #line 120 __cil_tmp15 = __cil_tmp16; #line 120 __cil_tmp15_b44 = (void *)__cil_tmp16; #line 120 __cil_tmp17 = (unsigned int )__cil_tmp16 + (((argvsize11 + 3U) >> 2) << 2); while ((unsigned int )__cil_tmp16 + sizeof(struct fseqp_char ) <= __cil_tmp17) { #line 120 __cil_tmp16->_ms._e = (void *)0; #line 120 __cil_tmp16->_p = (char */* __FSEQ */)0; #line 120 __cil_tmp16 = __cil_tmp16 + 1; } #line 120 __cil_tmp15_e45 = __cil_tmp16; } else { #line 120 __cil_tmp15 = 0; #line 120 __cil_tmp15_b44 = (void *)0; #line 120 __cil_tmp15_e45 = (void *)0; } #line 120 __cil_tmp18 = __cil_tmp15; #line 120 __cil_tmp18_b46 = __cil_tmp15_b44; #line 120 __cil_tmp18_e47 = __cil_tmp15_e45; #line 120 argv_e43 = __cil_tmp18_e47; #line 120 argv_b42 = __cil_tmp18_b46; #line 120 argv = __cil_tmp18; #line 120 while (num_strings9 >= 0) { { #line 120 CHECK_NULL((void *)p_argv10); #line 120 __cil_tmp19 = /*13*/__mkptr_string_fs((char */* */)(*p_argv10)); #line 120 __cil_tmp20 = __cil_tmp19._p; #line 120 __cil_tmp20_e48 = __cil_tmp19._ms._e; #line 120 CHECK_SEQ2SAFE(argv_b42, argv_e43, (void *)(argv + num_strings9), sizeof(struct fseqp_char ), sizeof(struct fseqp_char ), 1, 0); #line 120 CHECK_STOREPTR((void *)(argv + num_strings9), __cil_tmp20_e48, (void *)(& ___first_local)); #line 120 (argv + num_strings9)->_ms._e = __cil_tmp20_e48; #line 120 (argv + num_strings9)->_p = __cil_tmp20; #line 120 __cil_tmp22 = /*11*/__trusted_cast((unsigned int )((void */* */)((long )p_argv10 - sizeof((*__argv_input))))); #line 120 p_argv10 = (char * */* */)__cil_tmp22; #line 120 num_strings9 = num_strings9 - 1; } } } } } #line 120 __ccuredAlwaysStopOnError = 1; #line 120 __ccuredUseStrings = 0; #line 120 __ccuredLogNonPointers = 0; #line 120 __ccuredInit(); #line 120 __cil_tmp28 = ___compute_stack_threshhold(); #line 120 ___stack_threshhold = __cil_tmp28; { #line 126 __ccured_va_count = -1; #line 126 chatting((char */* */)((char */* */)(& __string5[0])), (int )sizeof(struct hash_entry )); #line 127 __ccured_va_count = -1; #line 127 chatting((char */* */)((char */* */)(& __string6[0])), (int )sizeof(struct hash )); #line 128 __ccured_va_count = -1; #line 128 chatting((char */* */)((char */* */)(& __string7[0])), (int )sizeof(struct vert_st )); #line 130 CHECK_SEQ2FSEQ(argv_b42, argv_e43, (void *)argv); #line 130 __cil_tmp29 = (fseqp_char */* __FSEQ */)argv; #line 130 __cil_tmp29_e57 = argv_e43; #line 130 __cil_tmp30 = dealwithargs_ff(argc, __cil_tmp29, __cil_tmp29_e57); #line 130 size = __cil_tmp30; #line 132 __ccured_va_count = -1; #line 132 chatting((char */* */)((char */* */)(& __string8[0])), size); #line 133 __cil_tmp31 = MakeGraph(size); #line 133 graph = (struct graph_st */* */)__cil_tmp31; #line 134 __ccured_va_count = -1; #line 134 chatting((char */* */)((char */* */)(& __string9[0]))); #line 136 __ccured_va_count = -1; #line 136 chatting((char */* */)((char */* */)(& __string10[0]))); #line 137 __cil_tmp32 = ComputeMst((struct graph_st */* */)graph, size); #line 137 dist = __cil_tmp32; #line 139 __ccured_va_count = -1; #line 139 chatting((char */* */)((char */* */)(& __string11[0])), dist); #line 140 exit(0); } #line 120 return (__retres); } } #line 9 "makegraph.c" static int HashRange ; #line 11 static int mult(int p , int q ) ; #line 11 "makegraph.c" static int mult(int p , int q ) { int p1 ; int p0 ; int q1 ; int q0 ; int __retres ; { #line 15 p1 = p / 10000; #line 15 p0 = p % 10000; #line 16 q1 = q / 10000; #line 16 q0 = q % 10000; #line 17 __retres = ((p0 * q1 + p1 * q0) % 10000) * 10000 + p0 * q0; #line 11 return (__retres); } } #line 20 static int mst_random(int seed ) ; #line 20 "makegraph.c" static int mst_random(int seed ) { int tmp ; int tmp___0 ; int __retres ; int __cil_tmp5 ; { #line 23 __cil_tmp5 = mult(seed, 31415821); #line 23 tmp___0 = __cil_tmp5; #line 23 tmp = tmp___0 + 1; #line 24 __retres = tmp; #line 20 return (__retres); } } #line 27 static int compute_dist(int i , int j , int numvert ) ; #line 27 "makegraph.c" static int compute_dist(int i , int j , int numvert ) { int less ; int gt ; int tmp ; int __retres ; int __cil_tmp8 ; { #line 30 if (i < j) { #line 30 less = i; #line 30 gt = j; } else { #line 30 less = j; #line 30 gt = i; } #line 31 __cil_tmp8 = mst_random(less * numvert + gt); #line 31 tmp = __cil_tmp8; #line 31 __retres = tmp % 2048 + 1; #line 27 return (__retres); } } #line 34 static int hashfunc(unsigned int key ) ; #line 34 "makegraph.c" static int hashfunc(unsigned int key ) { int __retres ; { #line 36 __retres = (int )((key >> 4) % (unsigned int )HashRange); #line 34 return (__retres); } } #line 62 "makegraph.c" static char __string12[19] = #line 62 { '%', 'd', ' ', 'e', 'd', 'g', 'e', 's', ' ', 'i', 'n', 's', 'e', 'r', 't', 'e', 'd', '\n', '\000'}; #line 39 static void AddEdges(struct graph_st * retval , int numvert ) ; #line 39 "makegraph.c" static void AddEdges(struct graph_st * retval , int numvert ) { struct vert_st * src ; struct vert_st * dest ; struct hash * hash ; int i ; int j ; int dist ; int num_inserted ; int __cil_tmp10 ; { #line 63 hash = (struct hash */* */)0; #line 63 dest = (struct vert_st */* */)0; #line 63 src = (struct vert_st */* */)0; #line 43 num_inserted = 0; #line 45 j = 0; #line 45 while (j < numvert) { #line 47 CHECK_NULL((void *)retval); #line 47 CHECK_FSEQARITH((void *)retval->vlist._p, sizeof(struct vert_st ), (void *)(retval->vlist._p + j)); #line 47 CHECK_FSEQ2SAFE(retval->vlist._ms._e, (void *)(retval->vlist._p + j), sizeof(struct vert_st ), sizeof(struct vert_st ), 0, 0); #line 47 src = (struct vert_st */* */)(retval->vlist._p + j); #line 48 CHECK_NULL((void *)src); #line 48 hash = (struct hash */* */)src->edgehash; #line 50 i = 0; #line 50 while (i < numvert) { #line 52 if (i != j) { #line 54 __cil_tmp10 = compute_dist(i, j, numvert); #line 54 dist = __cil_tmp10; #line 55 CHECK_NULL((void *)retval); #line 55 CHECK_FSEQARITH((void *)retval->vlist._p, sizeof(struct vert_st ), (void *)(retval->vlist._p + i)); #line 55 CHECK_FSEQ2SAFE(retval->vlist._ms._e, (void *)(retval->vlist._p + i), sizeof(struct vert_st ), sizeof(struct vert_st ), 0, 0); #line 55 dest = (struct vert_st */* */)(retval->vlist._p + i); #line 56 HashInsert((void */* */)((void */* */)dist), (unsigned int )dest, (struct hash */* */)hash); #line 57 num_inserted = num_inserted + 1; } #line 50 i = i + 1; } #line 45 j = j + 1; } #line 62 __ccured_va_count = -1; #line 62 chatting((char */* */)((char */* */)(& __string12[0])), num_inserted); #line 39 return; } } extern unsigned int ( __attribute__((__cdecl__)) /*17*/malloc)(size_t __size ) ; #line 73 "makegraph.c" static char __string13[36] = #line 73 { 'M', 'a', 'k', 'e', ' ', 'p', 'h', 'a', 's', 'e', ' ', '1', ':', ' ', 'C', 'r', 'e', 'a', 't', 'i', 'n', 'g', ' ', 'h', 'a', 's', 'h', ' ', 't', 'a', 'b', 'l', 'e', 's', '\n', '\000'}; #line 87 "makegraph.c" static char __string14[30] = #line 87 { 'M', 'a', 'k', 'e', ' ', 'p', 'h', 'a', 's', 'e', ' ', '3', ':', ' ', 'C', 'r', 'e', 'a', 't', 'i', 'n', 'g', ' ', 'g', 'r', 'a', 'p', 'h', '\n', '\000'}; #line 89 "makegraph.c" static char __string15[16] = #line 89 { 'M', 'a', 'k', 'e', ' ', 'r', 'e', 't', 'u', 'r', 'n', 'i', 'n', 'g', '\n', '\000'}; #line 65 struct graph_st * MakeGraph(int numvert ) ; #line 65 "makegraph.c" struct graph_st * MakeGraph(int numvert ) { int volatile ___first_local ; int i ; struct vert_st * __FSEQ vf ; struct vert_st * __FSEQ vt ; struct graph_st * retval ; struct graph_st * __retres ; struct graph_st * __cil_tmp9 ; struct graph_st * __cil_tmp10 ; struct vert_st * __FSEQ __cil_tmp11 ; struct vert_st * __FSEQ __cil_tmp12 ; unsigned int __cil_tmp13 ; struct vert_st * __FSEQ __cil_tmp14 ; struct vert_st * __FSEQ __cil_tmp16 ; struct vert_st * __FSEQ __cil_tmp17 ; struct hash * __cil_tmp18 ; struct vert_st * __FSEQ __cil_tmp19 ; struct vert_st * __FSEQ __cil_tmp20 ; void *vf_e29 ; void *vt_e30 ; void *__cil_tmp11_e31 ; void *__cil_tmp14_e32 ; void *__cil_tmp16_e33 ; void *__cil_tmp17_e34 ; void *__cil_tmp19_e35 ; void *__cil_tmp20_e36 ; { #line 90 __retres = (struct graph_st */* */)0; #line 90 retval = (struct graph_st */* */)0; #line 90 vt_e30 = (void *)0; #line 90 vt = (struct vert_st */* __FSEQ */)0; #line 90 vf_e29 = (void *)0; #line 90 vf = (struct vert_st */* __FSEQ */)0; #line 71 __cil_tmp10 = (struct graph_st */* */)/*17*/malloc(((sizeof((*retval)) + 3U) >> 2) << 2); #line 71 if (__cil_tmp10) { #line 71 __cil_tmp9 = __cil_tmp10; #line 71 CHECK_POSITIVE((int )(((sizeof((*retval)) + 3U) >> 2) << 2) - (int )sizeof(struct graph_st )); #line 71 __cil_tmp10->vlist._ms._e = (void *)0; #line 71 __cil_tmp10->vlist._p = (struct vert_st */* __FSEQ */)0; } else { #line 71 __cil_tmp9 = 0; } #line 71 retval = __cil_tmp9; #line 73 __ccured_va_count = -1; #line 73 chatting((char */* */)((char */* */)(& __string13[0]))); #line 74 __cil_tmp12 = (struct vert_st */* __FSEQ */)/*17*/malloc((((unsigned int )numvert * sizeof((*vf)) + 3U) >> 2) << 2); #line 74 if (__cil_tmp12) { #line 74 __cil_tmp11 = __cil_tmp12; #line 74 __cil_tmp13 = (unsigned int )__cil_tmp12 + ((((unsigned int )numvert * sizeof((*vf)) + 3U) >> 2) << 2); while ((unsigned int )__cil_tmp12 + sizeof(struct vert_st ) <= __cil_tmp13) { #line 74 __cil_tmp12->edgehash = (struct hash */* */)0; #line 74 __cil_tmp12->next._ms._e = (void *)0; #line 74 __cil_tmp12->next._p = (struct vert_st */* __FSEQ */)0; #line 74 __cil_tmp12 = __cil_tmp12 + 1; } #line 74 __cil_tmp11_e31 = __cil_tmp12; } else { #line 74 __cil_tmp11 = 0; #line 74 __cil_tmp11_e31 = (void *)0; } #line 74 CHECK_NULL((void *)retval); #line 74 __cil_tmp14 = __cil_tmp11; #line 74 __cil_tmp14_e32 = __cil_tmp11_e31; #line 74 CHECK_STOREPTR((void *)(& retval->vlist), __cil_tmp14_e32, (void *)(& ___first_local)); #line 74 retval->vlist._ms._e = __cil_tmp14_e32; #line 74 retval->vlist._p = __cil_tmp14; #line 75 __cil_tmp16 = (struct vert_st */* __FSEQ */)0; #line 75 __cil_tmp16_e33 = (void *)0; #line 75 vt_e30 = __cil_tmp16_e33; #line 75 vt = __cil_tmp16; #line 77 i = numvert - 1; #line 77 while (i >= 0) { #line 79 CHECK_NULL((void *)retval); #line 79 CHECK_FSEQARITH((void *)retval->vlist._p, sizeof(struct vert_st ), (void *)(retval->vlist._p + i)); #line 79 __cil_tmp17 = retval->vlist._p + i; #line 79 __cil_tmp17_e34 = retval->vlist._ms._e; #line 79 vf_e29 = __cil_tmp17_e34; #line 79 vf = __cil_tmp17; #line 80 HashRange = numvert / 4; #line 81 CHECK_FSEQ2SAFE(vf_e29, (void *)vf, sizeof(struct vert_st ), sizeof(struct vert_st ), 1, 0); #line 81 vf->mindist = 9999999; #line 82 __cil_tmp18 = MakeHash(HashRange, (int (*/* */)(unsigned int ))(& hashfunc)); #line 82 CHECK_FSEQ2SAFE(vf_e29, (void *)vf, sizeof(struct vert_st ), sizeof(struct vert_st ), 1, 0); #line 82 CHECK_STOREPTR((void *)(& vf->edgehash), (void *)((struct hash */* */)__cil_tmp18), (void *)(& ___first_local)); #line 82 vf->edgehash = (struct hash */* */)__cil_tmp18; #line 83 CHECK_FSEQ2SAFE(vf_e29, (void *)vf, sizeof(struct vert_st ), sizeof(struct vert_st ), 1, 0); #line 83 __cil_tmp19 = vt; #line 83 __cil_tmp19_e35 = vt_e30; #line 83 CHECK_STOREPTR((void *)(& vf->next), __cil_tmp19_e35, (void *)(& ___first_local)); #line 83 vf->next._ms._e = __cil_tmp19_e35; #line 83 vf->next._p = __cil_tmp19; #line 84 __cil_tmp20 = vf; #line 84 __cil_tmp20_e36 = vf_e29; #line 84 vt_e30 = __cil_tmp20_e36; #line 84 vt = __cil_tmp20; #line 77 i = i - 1; } #line 87 __ccured_va_count = -1; #line 87 chatting((char */* */)((char */* */)(& __string14[0]))); #line 88 AddEdges((struct graph_st */* */)retval, numvert); #line 89 __ccured_va_count = -1; #line 89 chatting((char */* */)((char */* */)(& __string15[0]))); #line 90 __retres = (struct graph_st */* */)retval; #line 65 CHECK_RETURNPTR((void *)__retres, (void *)(& ___first_local)); #line 65 return (__retres); } } #line 24 "hash.c" static int remaining = 0; #line 25 "hash.c" struct meta_seq_char { void *_b ; void *_e ; } ; #line 25 "hash.c" struct seq_char { char * __SEQ _p ; struct meta_seq_char _ms ; } ; #line 25 "hash.c" typedef struct seq_char seq_char; #line 25 "hash.c" static seq_char temp_q ; static unsigned int /*19*/localmalloc(int size ) ; #line 43 struct hash * MakeHash(int size , int (* map)(unsigned int ) ) ; #line 43 "hash.c" struct hash * MakeHash(int size , int (* map)(unsigned int ) ) { int volatile ___first_local ; struct hash * retval ; struct hash * __retres ; struct hash * __cil_tmp7 ; struct hash * __cil_tmp8 ; struct hash_entry * * __FSEQ __cil_tmp9 ; struct hash_entry * * __FSEQ __cil_tmp10 ; unsigned int __cil_tmp11 ; struct hash_entry * * __FSEQ __cil_tmp12 ; void *__cil_tmp9_e16 ; void *__cil_tmp12_e17 ; { #line 55 __retres = (struct hash */* */)0; #line 55 retval = (struct hash */* */)0; #line 47 __cil_tmp8 = (struct hash */* */)/*19*/localmalloc((((unsigned int )((int )sizeof((*retval))) + 3U) >> 2) << 2); #line 47 if (__cil_tmp8) { #line 47 __cil_tmp7 = __cil_tmp8; #line 47 CHECK_POSITIVE((int )((((unsigned int )((int )sizeof((*retval))) + 3U) >> 2) << 2) - (int )sizeof(struct hash )); #line 47 __cil_tmp8->mapfunc = (int (*/* */)(unsigned int ))0; #line 47 __cil_tmp8->array._ms._e = (void *)0; #line 47 __cil_tmp8->array._p = (struct hash_entry * */* __FSEQ */)0; } else { #line 47 __cil_tmp7 = 0; } #line 47 retval = __cil_tmp7; #line 48 __cil_tmp10 = (struct hash_entry * */* __FSEQ */)/*19*/localmalloc((((unsigned int )((int )((unsigned int )size * sizeof((*(retval->array._p))))) + 3U) >> 2) << 2); #line 48 if (__cil_tmp10) { #line 48 __cil_tmp9 = __cil_tmp10; #line 48 __cil_tmp11 = (unsigned int )__cil_tmp10 + ((((unsigned int )((int )((unsigned int )size * sizeof((*(retval->array._p))))) + 3U) >> 2) << 2); while ((unsigned int )__cil_tmp10 + sizeof(struct hash_entry */* */) <= __cil_tmp11) { #line 48 (*__cil_tmp10) = (struct hash_entry */* */)0; #line 48 __cil_tmp10 = __cil_tmp10 + 1; } #line 48 __cil_tmp9_e16 = __cil_tmp10; } else { #line 48 __cil_tmp9 = 0; #line 48 __cil_tmp9_e16 = (void *)0; } #line 48 CHECK_NULL((void *)retval); #line 48 __cil_tmp12 = __cil_tmp9; #line 48 __cil_tmp12_e17 = __cil_tmp9_e16; #line 48 CHECK_STOREPTR((void *)(& retval->array), __cil_tmp12_e17, (void *)(& ___first_local)); #line 48 retval->array._ms._e = __cil_tmp12_e17; #line 48 retval->array._p = __cil_tmp12; { __NOCURE #line 50 memset((void *)((char *)retval->array._p), 0, (unsigned int )size * sizeof((*(retval->array._p + 0)))); } #line 52 CHECK_NULL((void *)retval); #line 52 CHECK_STOREPTR((void *)(& retval->mapfunc), (void *)((int (*/* */)(unsigned int ))map), (void *)(& ___first_local)); #line 52 retval->mapfunc = (int (*/* */)(unsigned int ))map; #line 53 CHECK_NULL((void *)retval); #line 53 retval->size = size; #line 54 CHECK_NULL((void *)retval); #line 54 retval->padding = 0U; #line 55 __retres = (struct hash */* */)retval; #line 43 CHECK_RETURNPTR((void *)__retres, (void *)(& ___first_local)); #line 43 return (__retres); } } #line 58 void * HashLookup(unsigned int key , struct hash * hash ) ; #line 58 "hash.c" void * HashLookup(unsigned int key , struct hash * hash ) { int volatile ___first_local ; int j ; struct hash_entry * ent ; void * __retres ; int __cil_tmp6 ; { #line 70 __retres = (void */* */)0; #line 70 ent = (struct hash_entry */* */)0; #line 63 CHECK_NULL((void *)hash); #line 63 CHECK_NULL((void *)hash->mapfunc); #line 63 CHECK_NULL((void *)hash->mapfunc); #line 63 __cil_tmp6 = ((*(hash->mapfunc)))(key); #line 63 j = __cil_tmp6; #line 67 CHECK_NULL((void *)hash); #line 67 CHECK_FSEQARITH2SAFE((void *)hash->array._p, hash->array._ms._e, (void *)(hash->array._p + j), sizeof(struct hash_entry */* */), sizeof(struct hash_entry */* */), 1, 0); #line 67 ent = (struct hash_entry */* */)(*(hash->array._p + j)); #line 67 while (1) { #line 67 if ((int )ent) { #line 67 CHECK_NULL((void *)ent); #line 67 if (! (ent->key != key)) { #line 67 break; } } else { #line 67 break; } #line 67 CHECK_NULL((void *)ent); #line 67 ent = (struct hash_entry */* */)ent->next; } #line 69 if ((int )ent) { #line 69 CHECK_NULL((void *)ent); #line 69 __retres = (void */* */)ent->entry; goto return_label; } #line 70 __retres = (void */* */)0; return_label: /* CIL Label */ #line 58 CHECK_RETURNPTR((void *)__retres, (void *)(& ___first_local)); #line 58 return (__retres); } } #line 73 void HashInsert(void * entry , unsigned int key , struct hash * hash ) ; #line 73 "hash.c" void HashInsert(void * entry , unsigned int key , struct hash * hash ) { int volatile ___first_local ; struct hash_entry * ent ; int j ; int __cil_tmp7 ; struct hash_entry * __cil_tmp8 ; struct hash_entry * __cil_tmp9 ; { #line 87 ent = (struct hash_entry */* */)0; #line 80 CHECK_NULL((void *)hash); #line 80 CHECK_NULL((void *)hash->mapfunc); #line 80 CHECK_NULL((void *)hash->mapfunc); #line 80 __cil_tmp7 = ((*(hash->mapfunc)))(key); #line 80 j = __cil_tmp7; #line 82 __cil_tmp9 = (struct hash_entry */* */)/*19*/localmalloc((((unsigned int )((int )sizeof((*ent))) + 3U) >> 2) << 2); #line 82 if (__cil_tmp9) { #line 82 __cil_tmp8 = __cil_tmp9; #line 82 CHECK_POSITIVE((int )((((unsigned int )((int )sizeof((*ent))) + 3U) >> 2) << 2) - (int )sizeof(struct hash_entry )); #line 82 __cil_tmp9->next = (struct hash_entry */* */)0; #line 82 __cil_tmp9->entry = (void */* */)0; } else { #line 82 __cil_tmp8 = 0; } #line 82 ent = __cil_tmp8; #line 83 CHECK_NULL((void *)ent); #line 83 CHECK_NULL((void *)hash); #line 83 CHECK_FSEQARITH2SAFE((void *)hash->array._p, hash->array._ms._e, (void *)(hash->array._p + j), sizeof(struct hash_entry */* */), sizeof(struct hash_entry */* */), 1, 0); #line 83 CHECK_STOREPTR((void *)(& ent->next), (void *)((struct hash_entry */* */)(*(hash->array._p + j))), (void *)(& ___first_local)); #line 83 ent->next = (struct hash_entry */* */)(*(hash->array._p + j)); #line 84 CHECK_NULL((void *)hash); #line 84 CHECK_FSEQARITH((void *)hash->array._p, sizeof(struct hash_entry */* */), (void *)(hash->array._p + j)); #line 84 CHECK_FSEQ2SAFE(hash->array._ms._e, (void *)(hash->array._p + j), sizeof(struct hash_entry */* */), sizeof(struct hash_entry */* */), 1, 0); #line 84 CHECK_STOREPTR((void *)(hash->array._p + j), (void *)((struct hash_entry */* */)ent), (void *)(& ___first_local)); #line 84 (*(hash->array._p + j)) = (struct hash_entry */* */)ent; #line 85 CHECK_NULL((void *)ent); #line 85 ent->key = key; #line 86 CHECK_NULL((void *)ent); #line 86 CHECK_STOREPTR((void *)(& ent->entry), (void *)((void */* */)entry), (void *)(& ___first_local)); #line 86 ent->entry = (void */* */)entry; #line 73 return; } } #line 89 void HashDelete(unsigned int key , struct hash * hash ) ; #line 89 "hash.c" void HashDelete(unsigned int key , struct hash * hash ) { int volatile ___first_local ; struct hash_entry * * ent ; struct hash_entry * tmp ; int j ; int __cil_tmp6 ; { #line 101 tmp = (struct hash_entry */* */)0; #line 101 ent = (struct hash_entry * */* */)0; #line 95 CHECK_NULL((void *)hash); #line 95 CHECK_NULL((void *)hash->mapfunc); #line 95 CHECK_NULL((void *)hash->mapfunc); #line 95 __cil_tmp6 = ((*(hash->mapfunc)))(key); #line 95 j = __cil_tmp6; #line 96 CHECK_NULL((void *)hash); #line 96 CHECK_FSEQARITH((void *)hash->array._p, sizeof(struct hash_entry */* */), (void *)(hash->array._p + j)); #line 96 CHECK_FSEQ2SAFE(hash->array._ms._e, (void *)(hash->array._p + j), sizeof(struct hash_entry */* */), sizeof(struct hash_entry */* */), 0, 0); #line 96 ent = (struct hash_entry * */* */)(hash->array._p + j); #line 96 while (1) { #line 96 CHECK_NULL((void *)ent); #line 96 if ((int )(*ent)) { #line 96 CHECK_NULL((void *)ent); #line 96 CHECK_NULL((void *)(*ent)); #line 96 if (! (((*ent))->key != key)) { #line 96 break; } } else { #line 96 break; } #line 96 CHECK_NULL((void *)ent); #line 96 CHECK_NULL((void *)(*ent)); #line 96 ent = (struct hash_entry * */* */)(& ((*ent))->next); } #line 98 CHECK_NULL((void *)ent); #line 98 tmp = (struct hash_entry */* */)(*ent); #line 99 CHECK_NULL((void *)ent); #line 99 CHECK_NULL((void *)ent); #line 99 CHECK_NULL((void *)(*ent)); #line 99 CHECK_STOREPTR((void *)ent, (void *)((struct hash_entry */* */)((*ent))->next), (void *)(& ___first_local)); #line 99 (*ent) = (struct hash_entry */* */)((*ent))->next; #line 89 return; } } __inline static int /*22*/atoi_wrapper_f(char * __FSEQ str , void *str_e ) ; #line 9 "args.c" int dealwithargs_ff(int argc , fseqp_char * __FSEQ argv , void *argv_e ) ; #line 9 "args.c" int dealwithargs_ff(int argc , fseqp_char * __FSEQ argv , void *argv_e ) { int level ; int __retres ; char * __FSEQ __cil_tmp5 ; int __cil_tmp6 ; void *__cil_tmp5_e10 ; { #line 13 if (argc > 1) { #line 14 CHECK_FSEQARITH2SAFE((void *)argv, argv_e, (void *)(argv + 1), sizeof(fseqp_char ), sizeof(fseqp_char ), 1, 0); #line 14 __cil_tmp5 = (argv + 1)->_p; #line 14 __cil_tmp5_e10 = (argv + 1)->_ms._e; #line 14 __cil_tmp6 = /*22*/atoi_wrapper_f(__cil_tmp5, __cil_tmp5_e10); #line 14 level = __cil_tmp6; } else { #line 16 level = 1024; } #line 18 __retres = level; #line 9 return (__retres); } } #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 32 "hash.c" static char __string16[28] = #line 32 { 'E', 'r', 'r', 'o', 'r', '!', ' ', 'm', 'a', 'l', 'l', 'o', 'c', ' ', 'r', 'e', 't', 'u', 'r', 'n', 's', ' ', 'n', 'u', 'l', 'l', '\n', '\000'}; static unsigned int /*19*/localmalloc(int size ) ; static unsigned int /*19*/localmalloc(int size ) { int volatile ___first_local ; char * blah ; unsigned int __retres ; char * __SEQ __cil_tmp5 ; char * __SEQ __cil_tmp6 ; unsigned int __cil_tmp7 ; char * __SEQ __cil_tmp8 ; char * __SEQ __cil_tmp10 ; void *__cil_tmp5_b14 ; void *__cil_tmp5_e15 ; void *__cil_tmp8_b16 ; void *__cil_tmp8_e17 ; void *__cil_tmp10_b18 ; void *__cil_tmp10_e19 ; { #line 38 blah = (char */* */)0; #line 29 if (size > remaining) { #line 31 __cil_tmp6 = (char */* __SEQ */)/*17*/malloc(((32768U + 3U) >> 2) << 2); #line 31 if (__cil_tmp6) { #line 31 __cil_tmp5 = __cil_tmp6; #line 31 __cil_tmp5_b14 = (void *)__cil_tmp6; #line 31 __cil_tmp7 = (unsigned int )__cil_tmp6 + (((32768U + 3U) >> 2) << 2); #line 31 __cil_tmp6 = (char */* __SEQ */)__cil_tmp7; #line 31 __cil_tmp5_e15 = __cil_tmp6; } else { #line 31 __cil_tmp5 = 0; #line 31 __cil_tmp5_b14 = (void *)0; #line 31 __cil_tmp5_e15 = (void *)0; } #line 31 __cil_tmp8 = __cil_tmp5; #line 31 __cil_tmp8_b16 = __cil_tmp5_b14; #line 31 __cil_tmp8_e17 = __cil_tmp5_e15; #line 31 CHECK_STOREPTR((void *)(& temp_q), __cil_tmp8_b16, (void *)(& ___first_local)); #line 31 temp_q._ms._e = __cil_tmp8_e17; #line 31 temp_q._ms._b = __cil_tmp8_b16; #line 31 temp_q._p = __cil_tmp8; #line 32 if (! ((int )temp_q._p)) { #line 32 __ccured_va_count = -1; #line 32 chatting((char */* */)((char */* */)(& __string16[0]))); } #line 33 remaining = 32768; } #line 35 CHECK_SEQ2SAFE(temp_q._ms._b, temp_q._ms._e, (void *)temp_q._p, sizeof(char ), sizeof(char ), 0, 0); #line 35 blah = (char */* */)temp_q._p; #line 36 __cil_tmp10 = temp_q._p + size; #line 36 __cil_tmp10_b18 = temp_q._ms._b; #line 36 __cil_tmp10_e19 = temp_q._ms._e; #line 36 CHECK_STOREPTR((void *)(& temp_q), __cil_tmp10_b18, (void *)(& ___first_local)); #line 36 temp_q._ms._e = __cil_tmp10_e19; #line 36 temp_q._ms._b = __cil_tmp10_b18; #line 36 temp_q._p = __cil_tmp10; #line 37 remaining = remaining - size; #line 38 __retres = (unsigned int )blah; return (__retres); } } extern void /*26*/__verify_nul_f(char * __FSEQ ptr_p , void *ptr_ms_e ) ; __inline static int /*22*/atoi_wrapper_f(char * __FSEQ str , void *str_e ) ; __inline static int /*22*/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 /*26*/__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); } }