/* 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 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 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 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 21 "em3d.h" struct meta_fseqp_p_s_node_t { void *_e ; } ; #line 21 "em3d.h" struct fseqp_p_s_node_t { struct node_t * * __FSEQ _p ; struct meta_fseqp_p_s_node_t _ms ; } ; #line 21 "em3d.h" typedef struct fseqp_p_s_node_t fseqp_p_s_node_t; #line 21 "em3d.h" struct meta_fseqp_double { void *_e ; } ; #line 21 "em3d.h" struct fseqp_double { double * __FSEQ _p ; struct meta_fseqp_double _ms ; } ; #line 21 "em3d.h" typedef struct fseqp_double fseqp_double; #line 21 "em3d.h" struct node_t { double value ; struct node_t * next ; fseqp_p_s_node_t to_nodes ; struct fseqp_p_s_node_t from_nodes ; fseqp_double coeffs ; int from_count ; }; #line 21 "em3d.h" typedef struct node_t node_t; #line 30 "em3d.h" struct graph_t { node_t * e_nodes ; node_t * h_nodes ; }; #line 30 "em3d.h" typedef struct graph_t graph_t; #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 199 "d:/home/db/postdoc/Blast/ccured/include/gcc_3.3.1/stdio.h" extern int ( __CCUREDFORMAT(2) __CCUREDVARARG(struct printf_arguments ) __attribute__((__cdecl__)) fprintf)(FILE * , char * , ...) ; #line 201 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 11 "em3d.h" int n_nodes ; #line 12 int d_nodes ; #line 13 "em3d.h" int iters ; #line 36 void compute_nodes(node_t * nodelist ) ; #line 13 "make_graph.h" graph_t initialize_graph(void) ; #line 8 "main.c" void print_graph(graph_t graph ) ; #line 8 "main.c" void print_graph(graph_t graph ) { { #line 8 return; } } #line 33 "main.c" struct meta_fseqp_char { void *_e ; } ; #line 33 "main.c" struct fseqp_char { char * __FSEQ _p ; struct meta_fseqp_char _ms ; } ; #line 33 "main.c" typedef struct fseqp_char fseqp_char; #line 33 "main.c" struct meta_fseqp_p_char { void *_e ; } ; #line 33 void dealwithargs_ff(int argc , fseqp_char * __FSEQ argv , void *argv_e ) ; extern void * /*3*/__trusted_cast(unsigned int p ) ; extern unsigned int /*4*/wrapperAlloc(unsigned int ) ; extern struct fseqp_char /*5*/__mkptr_string_fs(char * p ) ; extern void * /*7*/__trusted_deepcast(void * p ) ; struct meta_seq_void { void *_b ; void *_e ; } ; #line 41 extern int __ccured_va_count ; #line 28 "main.c" struct meta_seq_p_char { void *_b ; void *_e ; } ; #line 41 "main.c" static char __string1[35] = #line 41 { 'C', 'o', 'm', 'p', 'l', 'e', 't', 'e', 'd', ' ', 'a', ' ', 'c', 'o', 'm', 'p', 'u', 't', 'a', 't', 'i', 'o', 'n', ' ', 'p', 'h', 'a', 's', 'e', ':', ' ', '%', 'd', '\n', '\000'}; #line 28 int main(int argc , char * __ROSTRING * __argv_input ) ; #line 28 "main.c" int main(int argc , char * __ROSTRING * __argv_input ) { int volatile ___first_local ; struct fseqp_char * __SEQ argv ; int i ; graph_t graph ; struct _reent * tmp ; 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 ; graph_t __cil_tmp30 ; struct _reent * __cil_tmp31 ; void *argv_b41 ; void *argv_e42 ; void *__cil_tmp15_b43 ; void *__cil_tmp15_e44 ; void *__cil_tmp18_b45 ; void *__cil_tmp18_e46 ; void *__cil_tmp20_e47 ; void *__cil_tmp24_b48 ; void *__cil_tmp24_e49 ; void *__cil_tmp25_b50 ; void *__cil_tmp25_e51 ; void *__cil_tmp26_b52 ; void *__cil_tmp26_e53 ; void *__cil_tmp27_b54 ; void *__cil_tmp27_e55 ; void *__cil_tmp29_e56 ; { #line 28 tmp_argv12 = (struct fseqp_char */* */)0; #line 28 p_argv10 = (char * */* */)0; #line 28 tmp = (struct _reent */* */)0; #line 28 graph.h_nodes = (node_t */* */)0; #line 28 graph.e_nodes = (node_t */* */)0; #line 28 argv_e42 = (void *)0; #line 28 argv_b41 = (void *)0; #line 28 argv = (struct fseqp_char */* __SEQ */)0; { #line 28 no_mangling8 = 0; #line 28 if ((int )__argv_input) { { #line 28 no_mangling8 = 0; #line 28 if (no_mangling8) { { #line 28 no_mangling8 = 0; } } } } else { { #line 28 no_mangling8 = 1; } } #line 28 if (no_mangling8) { { #line 28 __cil_tmp23 = /*7*/__trusted_deepcast((void */* */)__argv_input); #line 28 tmp_argv12 = (struct fseqp_char */* */)__cil_tmp23; #line 28 if ((void */* */)tmp_argv12) { #line 28 __cil_tmp25 = (void */* */)tmp_argv12; #line 28 __cil_tmp25_b50 = (void */* */)tmp_argv12; #line 28 __cil_tmp25_e51 = (void */* */)tmp_argv12 + sizeof((*argv)); #line 28 __cil_tmp24_e49 = __cil_tmp25_e51; #line 28 __cil_tmp24_b48 = __cil_tmp25_b50; #line 28 __cil_tmp24 = __cil_tmp25; } else { #line 28 __cil_tmp26 = 0; #line 28 __cil_tmp26_b52 = (void *)0; #line 28 __cil_tmp26_e53 = (void *)0; #line 28 __cil_tmp24_e49 = __cil_tmp26_e53; #line 28 __cil_tmp24_b48 = __cil_tmp26_b52; #line 28 __cil_tmp24 = __cil_tmp26; } #line 28 CHECK_SEQALIGN(sizeof(struct fseqp_char ), (void *)((struct fseqp_char */* __SEQ */)__cil_tmp24), __cil_tmp24_b48, __cil_tmp24_e49); #line 28 __cil_tmp27 = (struct fseqp_char */* __SEQ */)__cil_tmp24; #line 28 __cil_tmp27_b54 = __cil_tmp24_b48; #line 28 __cil_tmp27_e55 = __cil_tmp24_e49; #line 28 argv_e42 = __cil_tmp27_e55; #line 28 argv_b41 = __cil_tmp27_b54; #line 28 argv = __cil_tmp27; } } else { { #line 28 num_strings9 = 0; #line 28 p_argv10 = (char * */* */)__argv_input; #line 28 while (1) { #line 28 CHECK_NULL((void *)p_argv10); #line 28 if (! ((int )((unsigned int )(*p_argv10)))) { #line 28 break; } { #line 28 num_strings9 = num_strings9 + 1; #line 28 __cil_tmp14 = /*3*/__trusted_cast((unsigned int )((void */* */)((long )p_argv10 + sizeof((*__argv_input))))); #line 28 p_argv10 = (char * */* */)__cil_tmp14; } } #line 28 argvsize11 = (unsigned int )((1 + num_strings9) * sizeof((*argv))); #line 28 __cil_tmp16 = (struct fseqp_char */* __SEQ */)/*4*/wrapperAlloc(((argvsize11 + 3U) >> 2) << 2); #line 28 if (__cil_tmp16) { #line 28 __cil_tmp15 = __cil_tmp16; #line 28 __cil_tmp15_b43 = (void *)__cil_tmp16; #line 28 __cil_tmp17 = (unsigned int )__cil_tmp16 + (((argvsize11 + 3U) >> 2) << 2); while ((unsigned int )__cil_tmp16 + sizeof(struct fseqp_char ) <= __cil_tmp17) { #line 28 __cil_tmp16->_ms._e = (void *)0; #line 28 __cil_tmp16->_p = (char */* __FSEQ */)0; #line 28 __cil_tmp16 = __cil_tmp16 + 1; } #line 28 __cil_tmp15_e44 = __cil_tmp16; } else { #line 28 __cil_tmp15 = 0; #line 28 __cil_tmp15_b43 = (void *)0; #line 28 __cil_tmp15_e44 = (void *)0; } #line 28 __cil_tmp18 = __cil_tmp15; #line 28 __cil_tmp18_b45 = __cil_tmp15_b43; #line 28 __cil_tmp18_e46 = __cil_tmp15_e44; #line 28 argv_e42 = __cil_tmp18_e46; #line 28 argv_b41 = __cil_tmp18_b45; #line 28 argv = __cil_tmp18; #line 28 while (num_strings9 >= 0) { { #line 28 CHECK_NULL((void *)p_argv10); #line 28 __cil_tmp19 = /*5*/__mkptr_string_fs((char */* */)(*p_argv10)); #line 28 __cil_tmp20 = __cil_tmp19._p; #line 28 __cil_tmp20_e47 = __cil_tmp19._ms._e; #line 28 CHECK_SEQ2SAFE(argv_b41, argv_e42, (void *)(argv + num_strings9), sizeof(struct fseqp_char ), sizeof(struct fseqp_char ), 1, 0); #line 28 CHECK_STOREPTR((void *)(argv + num_strings9), __cil_tmp20_e47, (void *)(& ___first_local)); #line 28 (argv + num_strings9)->_ms._e = __cil_tmp20_e47; #line 28 (argv + num_strings9)->_p = __cil_tmp20; #line 28 __cil_tmp22 = /*3*/__trusted_cast((unsigned int )((void */* */)((long )p_argv10 - sizeof((*__argv_input))))); #line 28 p_argv10 = (char * */* */)__cil_tmp22; #line 28 num_strings9 = num_strings9 - 1; } } } } } #line 28 __ccuredAlwaysStopOnError = 1; #line 28 __ccuredUseStrings = 0; #line 28 __ccuredLogNonPointers = 0; #line 28 __ccuredInit(); #line 28 __cil_tmp28 = ___compute_stack_threshhold(); #line 28 ___stack_threshhold = __cil_tmp28; { #line 33 CHECK_SEQ2FSEQ(argv_b41, argv_e42, (void *)argv); #line 33 __cil_tmp29 = (fseqp_char */* __FSEQ */)argv; #line 33 __cil_tmp29_e56 = argv_e42; #line 33 dealwithargs_ff(argc, __cil_tmp29, __cil_tmp29_e56); #line 34 __cil_tmp30 = initialize_graph(); #line 34 graph = __cil_tmp30; #line 35 print_graph(graph); #line 37 i = 0; #line 37 while (i < iters) { #line 39 compute_nodes((node_t */* */)graph.e_nodes); #line 40 compute_nodes((node_t */* */)graph.h_nodes); #line 41 __cil_tmp31 = __getreent(); #line 41 tmp = (struct _reent */* */)__cil_tmp31; #line 41 __ccured_va_count = -1; #line 41 CHECK_NULL((void *)tmp); #line 41 fprintf((FILE */* */)tmp->_stderr, (char */* */)(& __string1[0]), i); #line 42 print_graph(graph); #line 37 i = i + 1; } #line 44 return (0); } #line 28 return (__retres); } } #line 3 "em3d.c" void compute_nodes(node_t * nodelist ) ; #line 3 "em3d.c" void compute_nodes(node_t * nodelist ) { int i ; node_t * other_node ; double coeff ; double value ; { #line 16 other_node = (node_t */* */)0; #line 7 while ((int )nodelist) { #line 8 i = 0; #line 8 while (1) { #line 8 CHECK_NULL((void *)nodelist); #line 8 if (! (i < nodelist->from_count)) { #line 8 break; } #line 10 CHECK_FSEQARITH2SAFE((void *)nodelist->from_nodes._p, nodelist->from_nodes._ms._e, (void *)(nodelist->from_nodes._p + i), sizeof(struct node_t */* */), sizeof(struct node_t */* */), 1, 0); #line 10 other_node = (node_t */* */)(*(nodelist->from_nodes._p + i)); #line 11 CHECK_FSEQARITH2SAFE((void *)nodelist->coeffs._p, nodelist->coeffs._ms._e, (void *)(nodelist->coeffs._p + i), sizeof(double ), sizeof(double ), 1, 0); #line 11 coeff = (*(nodelist->coeffs._p + i)); #line 12 CHECK_NULL((void *)other_node); #line 12 value = other_node->value; #line 14 nodelist->value = nodelist->value - coeff * value; #line 8 i = i + 1; } #line 7 nodelist = (node_t */* */)nodelist->next; } #line 3 return; } } #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 66 extern void ( __attribute__((__cdecl__)) free)(void * ) ; #line 93 extern void ( __attribute__((__cdecl__)) srand)(unsigned int __seed ) ; #line 132 double ( __attribute__((__cdecl__)) drand48)(void) ; #line 140 long ( __attribute__((__cdecl__)) lrand48)(void) ; #line 150 void ( __attribute__((__cdecl__)) srand48)(long seed ) ; #line 163 extern int ( __attribute__((__cdecl__)) random)(void) ; #line 11 "em3d.h" int n_nodes ; #line 12 "em3d.h" int d_nodes ; #line 11 "util.h" void init_random(int myid ) ; #line 14 int gen_number(int range ) ; #line 17 int gen_signed_number(int range ) ; #line 20 double gen_uniform_double(void) ; #line 23 int check_percent(int percent ) ; extern unsigned int ( __attribute__((__cdecl__)) /*17*/malloc)(size_t __size ) ; #line 28 "make_graph.c" static char __string2[19] = #line 28 { 'A', 's', 's', 'e', 'r', 't', 'i', 'o', 'n', ' ', 'f', 'a', 'i', 'l', 'u', 'r', 'e', '\n', '\000'}; #line 23 struct fseqp_p_s_node_t make_table_fs(int size ) ; #line 23 "make_graph.c" struct fseqp_p_s_node_t make_table_fs(int size ) { int volatile ___first_local ; struct node_t * * __FSEQ retval ; struct node_t * * __FSEQ __retres ; struct node_t * * __FSEQ __cil_tmp5 ; struct node_t * * __FSEQ __cil_tmp6 ; unsigned int __cil_tmp7 ; struct node_t * * __FSEQ __cil_tmp8 ; struct node_t * * __FSEQ __cil_tmp9 ; struct fseqp_p_s_node_t __cil_tmp10 ; void *retval_e17 ; void *__retres_e18 ; void *__cil_tmp5_e19 ; void *__cil_tmp8_e20 ; void *__cil_tmp9_e21 ; { #line 29 __retres_e18 = (void *)0; #line 29 __retres = (struct node_t * */* __FSEQ */)0; #line 29 retval_e17 = (void *)0; #line 29 retval = (struct node_t * */* __FSEQ */)0; #line 27 __cil_tmp6 = (struct node_t * */* __FSEQ */)/*17*/malloc((((unsigned int )size * sizeof(node_t */* */) + 3U) >> 2) << 2); #line 27 if (__cil_tmp6) { #line 27 __cil_tmp5 = __cil_tmp6; #line 27 __cil_tmp7 = (unsigned int )__cil_tmp6 + ((((unsigned int )size * sizeof(node_t */* */) + 3U) >> 2) << 2); while ((unsigned int )__cil_tmp6 + sizeof(struct node_t */* */) <= __cil_tmp7) { #line 27 (*__cil_tmp6) = (struct node_t */* */)0; #line 27 __cil_tmp6 = __cil_tmp6 + 1; } #line 27 __cil_tmp5_e19 = __cil_tmp6; } else { #line 27 __cil_tmp5 = 0; #line 27 __cil_tmp5_e19 = (void *)0; } #line 27 __cil_tmp8 = __cil_tmp5; #line 27 __cil_tmp8_e20 = __cil_tmp5_e19; #line 27 retval_e17 = __cil_tmp8_e20; #line 27 retval = __cil_tmp8; #line 28 if (! ((int )retval)) { #line 28 __ccured_va_count = -1; #line 28 printf((char */* */)(& __string2[0])); #line 28 exit(-1); } #line 29 __cil_tmp9 = retval; #line 29 __cil_tmp9_e21 = retval_e17; #line 29 __retres_e18 = __cil_tmp9_e21; #line 29 __retres = __cil_tmp9; #line 23 __cil_tmp10._p = __retres; #line 23 __cil_tmp10._ms._e = __retres_e18; #line 23 CHECK_RETURNPTR(__cil_tmp10._ms._e, (void *)(& ___first_local)); #line 23 return (__cil_tmp10); } } #line 35 void fill_table_fs(struct node_t * * __FSEQ table , void *table_e , int size ) ; #line 35 "make_graph.c" void fill_table_fs(struct node_t * * __FSEQ table , void *table_e , int size ) { int volatile ___first_local ; int i ; struct node_t * __cil_tmp5 ; struct node_t * __cil_tmp6 ; double __cil_tmp8 ; { #line 40 i = 0; #line 40 while (i < size) { #line 42 __cil_tmp6 = (struct node_t */* */)/*17*/malloc(((sizeof(node_t ) + 3U) >> 2) << 2); #line 42 if (__cil_tmp6) { #line 42 __cil_tmp5 = __cil_tmp6; #line 42 __cil_tmp6->coeffs._ms._e = (void *)0; #line 42 __cil_tmp6->coeffs._p = (double */* __FSEQ */)0; #line 42 __cil_tmp6->from_nodes._ms._e = (void *)0; #line 42 __cil_tmp6->from_nodes._p = (struct node_t * */* __FSEQ */)0; #line 42 __cil_tmp6->to_nodes._ms._e = (void *)0; #line 42 __cil_tmp6->to_nodes._p = (struct node_t * */* __FSEQ */)0; #line 42 __cil_tmp6->next = (struct node_t */* */)0; } else { #line 42 __cil_tmp5 = 0; } #line 42 CHECK_FSEQARITH((void *)table, sizeof(struct node_t */* */), (void *)(table + i)); #line 42 CHECK_FSEQ2SAFE(table_e, (void *)(table + i), sizeof(struct node_t */* */), sizeof(struct node_t */* */), 1, 0); #line 42 CHECK_STOREPTR((void *)(table + i), (void *)__cil_tmp5, (void *)(& ___first_local)); #line 42 (*(table + i)) = __cil_tmp5; #line 43 __cil_tmp8 = gen_uniform_double(); #line 43 CHECK_FSEQARITH2SAFE((void *)table, table_e, (void *)(table + i), sizeof(struct node_t */* */), sizeof(struct node_t */* */), 1, 0); #line 43 CHECK_NULL((void *)(*(table + i))); #line 43 ((*(table + i)))->value = __cil_tmp8; #line 44 ((*(table + i)))->from_count = 0; #line 46 if (i > 0) { #line 47 CHECK_FSEQARITH2SAFE((void *)table, table_e, (void *)(table + (i - 1)), sizeof(struct node_t */* */), sizeof(struct node_t */* */), 1, 0); #line 47 CHECK_NULL((void *)(*(table + (i - 1)))); #line 47 CHECK_STOREPTR((void *)(& ((*(table + (i - 1))))->next), (void *)((struct node_t */* */)(*(table + i))), (void *)(& ___first_local)); #line 47 ((*(table + (i - 1))))->next = (struct node_t */* */)(*(table + i)); } #line 40 i = i + 1; } #line 49 CHECK_FSEQARITH2SAFE((void *)table, table_e, (void *)(table + (size - 1)), sizeof(struct node_t */* */), sizeof(struct node_t */* */), 1, 0); #line 49 CHECK_NULL((void *)(*(table + (size - 1)))); #line 49 CHECK_STOREPTR((void *)(& ((*(table + (size - 1))))->next), (void *)((struct node_t */* */)0), (void *)(& ___first_local)); #line 49 ((*(table + (size - 1))))->next = (struct node_t */* */)0; #line 35 return; } } #line 57 void make_neighbors_sfs(node_t * nodelist , struct node_t * * __FSEQ table , void *table_e , int tablesz , int degree ) ; #line 57 "make_graph.c" void make_neighbors_sfs(node_t * nodelist , struct node_t * * __FSEQ table , void *table_e , int tablesz , int degree ) { int volatile ___first_local ; node_t * cur_node ; node_t * other_node ; int j ; int k ; int tmp___0 ; struct node_t * * __FSEQ __cil_tmp11 ; struct node_t * * __FSEQ __cil_tmp12 ; unsigned int __cil_tmp13 ; struct node_t * * __FSEQ __cil_tmp14 ; int __cil_tmp16 ; void *__cil_tmp11_e21 ; void *__cil_tmp14_e22 ; { #line 82 other_node = (node_t */* */)0; #line 82 cur_node = (node_t */* */)0; #line 62 cur_node = (node_t */* */)nodelist; #line 62 while ((int )cur_node) { #line 67 __cil_tmp12 = (struct node_t * */* __FSEQ */)/*17*/malloc((((unsigned int )degree * sizeof(node_t */* */) + 3U) >> 2) << 2); #line 67 if (__cil_tmp12) { #line 67 __cil_tmp11 = __cil_tmp12; #line 67 __cil_tmp13 = (unsigned int )__cil_tmp12 + ((((unsigned int )degree * sizeof(node_t */* */) + 3U) >> 2) << 2); while ((unsigned int )__cil_tmp12 + sizeof(struct node_t */* */) <= __cil_tmp13) { #line 67 (*__cil_tmp12) = (struct node_t */* */)0; #line 67 __cil_tmp12 = __cil_tmp12 + 1; } #line 67 __cil_tmp11_e21 = __cil_tmp12; } else { #line 67 __cil_tmp11 = 0; #line 67 __cil_tmp11_e21 = (void *)0; } #line 67 CHECK_NULL((void *)cur_node); #line 67 __cil_tmp14 = __cil_tmp11; #line 67 __cil_tmp14_e22 = __cil_tmp11_e21; #line 67 CHECK_STOREPTR((void *)(& cur_node->to_nodes), __cil_tmp14_e22, (void *)(& ___first_local)); #line 67 cur_node->to_nodes._ms._e = __cil_tmp14_e22; #line 67 cur_node->to_nodes._p = __cil_tmp14; #line 68 j = 0; #line 68 while (j < degree) { #line 71 while (1) { #line 73 __cil_tmp16 = gen_number(tablesz); #line 73 tmp___0 = __cil_tmp16; #line 73 CHECK_FSEQARITH2SAFE((void *)table, table_e, (void *)(table + tmp___0), sizeof(struct node_t */* */), sizeof(struct node_t */* */), 1, 0); #line 73 other_node = (node_t */* */)(*(table + tmp___0)); #line 74 k = 0; #line 74 while (k < j) { #line 75 CHECK_NULL((void *)cur_node); #line 75 CHECK_FSEQARITH2SAFE((void *)cur_node->to_nodes._p, cur_node->to_nodes._ms._e, (void *)(cur_node->to_nodes._p + k), sizeof(struct node_t */* */), sizeof(struct node_t */* */), 1, 0); #line 75 if ((unsigned int )other_node == (unsigned int )(*(cur_node->to_nodes._p + k))) { #line 75 break; } #line 74 k = k + 1; } #line 71 if (! (k < j)) { #line 71 break; } } #line 78 CHECK_NULL((void *)cur_node); #line 78 CHECK_FSEQARITH((void *)cur_node->to_nodes._p, sizeof(struct node_t */* */), (void *)(cur_node->to_nodes._p + j)); #line 78 CHECK_FSEQ2SAFE(cur_node->to_nodes._ms._e, (void *)(cur_node->to_nodes._p + j), sizeof(struct node_t */* */), sizeof(struct node_t */* */), 1, 0); #line 78 CHECK_STOREPTR((void *)(cur_node->to_nodes._p + j), (void *)((struct node_t */* */)other_node), (void *)(& ___first_local)); #line 78 (*(cur_node->to_nodes._p + j)) = (struct node_t */* */)other_node; #line 79 CHECK_NULL((void *)other_node); #line 79 other_node->from_count = other_node->from_count + 1; #line 68 j = j + 1; } #line 62 cur_node = (node_t */* */)cur_node->next; } #line 57 return; } } #line 88 void update_from_coeffs(node_t * nodelist ) ; #line 88 "make_graph.c" void update_from_coeffs(node_t * nodelist ) { int volatile ___first_local ; node_t * cur_node ; int from_count ; int k ; struct node_t * * __FSEQ __cil_tmp7 ; struct node_t * * __FSEQ __cil_tmp8 ; unsigned int __cil_tmp9 ; struct node_t * * __FSEQ __cil_tmp10 ; double * __FSEQ __cil_tmp12 ; double * __FSEQ __cil_tmp13 ; unsigned int __cil_tmp14 ; double * __FSEQ __cil_tmp15 ; double __cil_tmp16 ; void *__cil_tmp7_e21 ; void *__cil_tmp10_e22 ; void *__cil_tmp12_e23 ; void *__cil_tmp15_e24 ; { #line 105 cur_node = (node_t */* */)0; #line 93 cur_node = (node_t */* */)nodelist; #line 93 while ((int )cur_node) { #line 95 CHECK_NULL((void *)cur_node); #line 95 from_count = cur_node->from_count; #line 98 __cil_tmp8 = (struct node_t * */* __FSEQ */)/*17*/malloc((((unsigned int )from_count * sizeof(node_t */* */) + 3U) >> 2) << 2); #line 98 if (__cil_tmp8) { #line 98 __cil_tmp7 = __cil_tmp8; #line 98 __cil_tmp9 = (unsigned int )__cil_tmp8 + ((((unsigned int )from_count * sizeof(node_t */* */) + 3U) >> 2) << 2); while ((unsigned int )__cil_tmp8 + sizeof(struct node_t */* */) <= __cil_tmp9) { #line 98 (*__cil_tmp8) = (struct node_t */* */)0; #line 98 __cil_tmp8 = __cil_tmp8 + 1; } #line 98 __cil_tmp7_e21 = __cil_tmp8; } else { #line 98 __cil_tmp7 = 0; #line 98 __cil_tmp7_e21 = (void *)0; } #line 98 CHECK_NULL((void *)cur_node); #line 98 __cil_tmp10 = __cil_tmp7; #line 98 __cil_tmp10_e22 = __cil_tmp7_e21; #line 98 CHECK_STOREPTR((void *)(& cur_node->from_nodes), __cil_tmp10_e22, (void *)(& ___first_local)); #line 98 cur_node->from_nodes._ms._e = __cil_tmp10_e22; #line 98 cur_node->from_nodes._p = __cil_tmp10; #line 99 __cil_tmp13 = (double */* __FSEQ */)/*17*/malloc((((unsigned int )from_count * sizeof(double ) + 3U) >> 2) << 2); #line 99 if (__cil_tmp13) { #line 99 __cil_tmp12 = __cil_tmp13; #line 99 __cil_tmp14 = (unsigned int )__cil_tmp13 + ((((unsigned int )from_count * sizeof(double ) + 3U) >> 2) << 2); #line 99 __cil_tmp13 = (double */* __FSEQ */)__cil_tmp14; #line 99 __cil_tmp12_e23 = __cil_tmp13; } else { #line 99 __cil_tmp12 = 0; #line 99 __cil_tmp12_e23 = (void *)0; } #line 99 CHECK_NULL((void *)cur_node); #line 99 __cil_tmp15 = __cil_tmp12; #line 99 __cil_tmp15_e24 = __cil_tmp12_e23; #line 99 CHECK_STOREPTR((void *)(& cur_node->coeffs), __cil_tmp15_e24, (void *)(& ___first_local)); #line 99 cur_node->coeffs._ms._e = __cil_tmp15_e24; #line 99 cur_node->coeffs._p = __cil_tmp15; #line 100 k = 0; #line 100 while (k < from_count) { #line 101 __cil_tmp16 = gen_uniform_double(); #line 101 CHECK_NULL((void *)cur_node); #line 101 CHECK_FSEQARITH((void *)cur_node->coeffs._p, sizeof(double ), (void *)(cur_node->coeffs._p + k)); #line 101 CHECK_FSEQ2SAFE(cur_node->coeffs._ms._e, (void *)(cur_node->coeffs._p + k), sizeof(double ), sizeof(double ), 1, 0); #line 101 (*(cur_node->coeffs._p + k)) = __cil_tmp16; #line 100 k = k + 1; } #line 103 cur_node->from_count = 0; #line 93 cur_node = (node_t */* */)cur_node->next; } #line 88 return; } } #line 114 void fill_from_fields(node_t * nodelist , int degree ) ; #line 114 "make_graph.c" void fill_from_fields(node_t * nodelist , int degree ) { int volatile ___first_local ; node_t * cur_node ; int j ; node_t * other_node ; { #line 128 other_node = (node_t */* */)0; #line 128 cur_node = (node_t */* */)0; #line 117 cur_node = (node_t */* */)nodelist; #line 117 while ((int )cur_node) { #line 121 j = 0; #line 121 while (j < degree) { #line 123 CHECK_NULL((void *)cur_node); #line 123 CHECK_FSEQARITH2SAFE((void *)cur_node->to_nodes._p, cur_node->to_nodes._ms._e, (void *)(cur_node->to_nodes._p + j), sizeof(struct node_t */* */), sizeof(struct node_t */* */), 1, 0); #line 123 other_node = (node_t */* */)(*(cur_node->to_nodes._p + j)); #line 124 CHECK_NULL((void *)other_node); #line 124 CHECK_FSEQARITH((void *)other_node->from_nodes._p, sizeof(struct node_t */* */), (void *)(other_node->from_nodes._p + other_node->from_count)); #line 124 CHECK_FSEQ2SAFE(other_node->from_nodes._ms._e, (void *)(other_node->from_nodes._p + other_node->from_count), sizeof(struct node_t */* */), sizeof(struct node_t */* */), 1, 0); #line 124 CHECK_STOREPTR((void *)(other_node->from_nodes._p + other_node->from_count), (void *)((struct node_t */* */)cur_node), (void *)(& ___first_local)); #line 124 (*(other_node->from_nodes._p + other_node->from_count)) = (struct node_t */* */)cur_node; #line 125 other_node->from_count = other_node->from_count + 1; #line 121 j = j + 1; } #line 117 CHECK_NULL((void *)cur_node); #line 117 cur_node = (node_t */* */)cur_node->next; } #line 114 return; } } struct meta_fseqp_void { void *_e ; } ; void /*22*/free_wrapper_f(void * __FSEQ x , void *x_e ) ; #line 136 graph_t initialize_graph(void) ; #line 136 "make_graph.c" graph_t initialize_graph(void) { int volatile ___first_local ; struct node_t * * __FSEQ h_table ; struct node_t * * __FSEQ e_table ; graph_t retval ; graph_t __retres ; struct fseqp_p_s_node_t __cil_tmp5 ; struct node_t * * __FSEQ __cil_tmp6 ; struct node_t * * __FSEQ __cil_tmp7 ; struct fseqp_p_s_node_t __cil_tmp8 ; struct node_t * * __FSEQ __cil_tmp9 ; struct node_t * * __FSEQ __cil_tmp10 ; struct node_t * * __FSEQ __cil_tmp11 ; struct node_t * * __FSEQ __cil_tmp12 ; void * __FSEQ __cil_tmp13 ; void * __FSEQ __cil_tmp14 ; void *h_table_e26 ; void *e_table_e27 ; void *__cil_tmp6_e28 ; void *__cil_tmp7_e29 ; void *__cil_tmp9_e30 ; void *__cil_tmp10_e31 ; void *__cil_tmp11_e32 ; void *__cil_tmp12_e33 ; void *__cil_tmp13_e34 ; void *__cil_tmp14_e35 ; { #line 169 __retres.h_nodes = (node_t */* */)0; #line 169 __retres.e_nodes = (node_t */* */)0; #line 169 retval.h_nodes = (node_t */* */)0; #line 169 retval.e_nodes = (node_t */* */)0; #line 169 e_table_e27 = (void *)0; #line 169 e_table = (struct node_t * */* __FSEQ */)0; #line 169 h_table_e26 = (void *)0; #line 169 h_table = (struct node_t * */* __FSEQ */)0; #line 143 __cil_tmp5 = make_table_fs(n_nodes); #line 143 __cil_tmp6 = __cil_tmp5._p; #line 143 __cil_tmp6_e28 = __cil_tmp5._ms._e; #line 143 h_table_e26 = __cil_tmp6_e28; #line 143 h_table = __cil_tmp6; #line 144 __cil_tmp7 = h_table; #line 144 __cil_tmp7_e29 = h_table_e26; #line 144 fill_table_fs(__cil_tmp7, __cil_tmp7_e29, n_nodes); #line 147 __cil_tmp8 = make_table_fs(n_nodes); #line 147 __cil_tmp9 = __cil_tmp8._p; #line 147 __cil_tmp9_e30 = __cil_tmp8._ms._e; #line 147 e_table_e27 = __cil_tmp9_e30; #line 147 e_table = __cil_tmp9; #line 148 __cil_tmp10 = e_table; #line 148 __cil_tmp10_e31 = e_table_e27; #line 148 fill_table_fs(__cil_tmp10, __cil_tmp10_e31, n_nodes); #line 152 CHECK_FSEQ2SAFE(h_table_e26, (void *)h_table, sizeof(struct node_t */* */), sizeof(struct node_t */* */), 1, 0); #line 152 __cil_tmp11 = e_table; #line 152 __cil_tmp11_e32 = e_table_e27; #line 152 make_neighbors_sfs((node_t */* */)(*h_table), __cil_tmp11, __cil_tmp11_e32, n_nodes, d_nodes); #line 153 CHECK_FSEQ2SAFE(e_table_e27, (void *)e_table, sizeof(struct node_t */* */), sizeof(struct node_t */* */), 1, 0); #line 153 __cil_tmp12 = h_table; #line 153 __cil_tmp12_e33 = h_table_e26; #line 153 make_neighbors_sfs((node_t */* */)(*e_table), __cil_tmp12, __cil_tmp12_e33, n_nodes, d_nodes); #line 156 update_from_coeffs((node_t */* */)(*h_table)); #line 157 update_from_coeffs((node_t */* */)(*e_table)); #line 160 fill_from_fields((node_t */* */)(*h_table), d_nodes); #line 161 fill_from_fields((node_t */* */)(*e_table), d_nodes); #line 163 retval.e_nodes = (node_t */* */)(*e_table); #line 164 retval.h_nodes = (node_t */* */)(*h_table); #line 166 __cil_tmp13 = (void */* __FSEQ */)h_table; #line 166 __cil_tmp13_e34 = h_table_e26; #line 166 /*22*/free_wrapper_f(__cil_tmp13, __cil_tmp13_e34); #line 167 __cil_tmp14 = (void */* __FSEQ */)e_table; #line 167 __cil_tmp14_e35 = e_table_e27; #line 167 /*22*/free_wrapper_f(__cil_tmp14, __cil_tmp14_e35); #line 169 __retres = retval; #line 136 CHECK_RETURNPTR((void *)__retres.e_nodes, (void *)(& ___first_local)); #line 136 CHECK_RETURNPTR((void *)__retres.h_nodes, (void *)(& ___first_local)); #line 136 return (__retres); } } #line 5 "util.c" void init_random(int myid ) ; #line 5 "util.c" void init_random(int myid ) { { #line 7 srand48((long )(myid * 45)); #line 5 return; } } #line 11 int gen_number(int range ) ; #line 11 "util.c" int gen_number(int range ) { long tmp ; int __retres ; long __cil_tmp4 ; { #line 13 __cil_tmp4 = lrand48(); #line 13 tmp = __cil_tmp4; #line 13 __retres = (int )(tmp % (long )range); #line 11 return (__retres); } } #line 17 int gen_signed_number(int range ) ; #line 17 "util.c" int gen_signed_number(int range ) { int temp ; long tmp ; int __retres ; long __cil_tmp5 ; { #line 21 __cil_tmp5 = lrand48(); #line 21 tmp = __cil_tmp5; #line 21 temp = (int )(tmp % (long )(2 * range - 1)); #line 22 __retres = temp - (range - 1); #line 17 return (__retres); } } #line 26 double gen_uniform_double(void) ; #line 26 "util.c" double gen_uniform_double(void) { double tmp ; double __retres ; double __cil_tmp3 ; { #line 28 __cil_tmp3 = drand48(); #line 28 tmp = __cil_tmp3; #line 28 __retres = tmp; #line 26 return (__retres); } } #line 31 int check_percent(int percent ) ; #line 31 "util.c" int check_percent(int percent ) { double tmp ; int __retres ; double __cil_tmp4 ; { #line 33 __cil_tmp4 = drand48(); #line 33 tmp = __cil_tmp4; #line 33 __retres = tmp < (double )percent / 100.0; #line 31 return (__retres); } } __inline static int /*24*/atoi_wrapper_f(char * __FSEQ str , void *str_e ) ; #line 5 "args.c" void dealwithargs_ff(int argc , fseqp_char * __FSEQ argv , void *argv_e ) ; #line 5 "args.c" void dealwithargs_ff(int argc , fseqp_char * __FSEQ argv , void *argv_e ) { char * __FSEQ __cil_tmp3 ; int __cil_tmp4 ; char * __FSEQ __cil_tmp5 ; int __cil_tmp6 ; char * __FSEQ __cil_tmp7 ; int __cil_tmp8 ; void *__cil_tmp3_e14 ; void *__cil_tmp5_e15 ; void *__cil_tmp7_e16 ; { #line 7 if (argc > 1) { #line 8 CHECK_FSEQARITH2SAFE((void *)argv, argv_e, (void *)(argv + 1), sizeof(fseqp_char ), sizeof(fseqp_char ), 1, 0); #line 8 __cil_tmp3 = (argv + 1)->_p; #line 8 __cil_tmp3_e14 = (argv + 1)->_ms._e; #line 8 __cil_tmp4 = /*24*/atoi_wrapper_f(__cil_tmp3, __cil_tmp3_e14); #line 8 n_nodes = __cil_tmp4; } else { #line 10 n_nodes = 10; } #line 12 if (argc > 2) { #line 13 CHECK_FSEQARITH2SAFE((void *)argv, argv_e, (void *)(argv + 2), sizeof(fseqp_char ), sizeof(fseqp_char ), 1, 0); #line 13 __cil_tmp5 = (argv + 2)->_p; #line 13 __cil_tmp5_e15 = (argv + 2)->_ms._e; #line 13 __cil_tmp6 = /*24*/atoi_wrapper_f(__cil_tmp5, __cil_tmp5_e15); #line 13 d_nodes = __cil_tmp6; } else { #line 15 d_nodes = 3; } #line 17 if (argc > 3) { #line 18 CHECK_FSEQARITH2SAFE((void *)argv, argv_e, (void *)(argv + 3), sizeof(fseqp_char ), sizeof(fseqp_char ), 1, 0); #line 18 __cil_tmp7 = (argv + 3)->_p; #line 18 __cil_tmp7_e16 = (argv + 3)->_ms._e; #line 18 __cil_tmp8 = /*24*/atoi_wrapper_f(__cil_tmp7, __cil_tmp7_e16); #line 18 iters = __cil_tmp8; } else { #line 20 iters = 100; } #line 5 return; } } #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 86 void ( __CCUREDFORMAT(1) __CCUREDVARARG(struct printf_arguments ) chatting)(char * s , ...) ; #line 10 "ssplain.c" struct __ccured_va_localinfo { int next ; int count ; int tags[32] ; void * nextp ; }; #line 10 void ( __CCUREDFORMAT(1) __CCUREDVARARG(struct printf_arguments ) chatting)(char * s , ...) ; #line 10 "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 16 ap__vainfo5.nextp = (void */* */)0; #line 16 tmp___0 = (struct _reent */* */)0; #line 16 ap = (struct __ccured_va_list */* */)0; #line 10 ap = (struct __ccured_va_list */* */)(& ap__vainfo5); #line 13 __cil_tmp7 = GCC_STDARG_START(s); #line 13 tmp = __cil_tmp7; #line 13 __ccured_va_start_vs((struct __ccured_va_list */* */)ap, tmp); #line 14 __cil_tmp8 = __getreent(); #line 14 tmp___0 = (struct _reent */* */)__cil_tmp8; #line 14 CHECK_NULL((void *)tmp___0); #line 14 vfprintf_ssvs((FILE */* */)tmp___0->_stderr, (char */* */)((char */* */)s), (struct __ccured_va_list */* */)ap); #line 15 __ccured_va_end_vs((struct __ccured_va_list */* */)ap); #line 10 return; } } #line 20 double ( __attribute__((__cdecl__)) drand48)(void) ; #line 20 "ssplain.c" double ( __attribute__((__cdecl__)) drand48)(void) { double d ; int tmp ; double __retres ; int __cil_tmp4 ; { #line 23 __cil_tmp4 = random(); #line 23 tmp = __cil_tmp4; #line 23 d = (double )tmp / (double )2147483647L; #line 24 __retres = d; #line 20 return (__retres); } } #line 28 long ( __attribute__((__cdecl__)) lrand48)(void) ; #line 28 "ssplain.c" long ( __attribute__((__cdecl__)) lrand48)(void) { long l ; long tmp ; long __retres ; int __cil_tmp4 ; { #line 30 __cil_tmp4 = random(); #line 30 tmp = (long )__cil_tmp4; #line 30 l = tmp; #line 31 __retres = l; #line 28 return (__retres); } } #line 34 void ( __attribute__((__cdecl__)) srand48)(long seed ) ; #line 34 "ssplain.c" void ( __attribute__((__cdecl__)) srand48)(long seed ) { { #line 36 srand((unsigned int )seed); #line 34 return; } } #line 42 "ssplain.c" static unsigned long bytes_allocated = 0UL; #line 43 "ssplain.c" static unsigned long allocations = 0UL; #line 45 void * ssplain_malloc(int size ) ; #line 45 "ssplain.c" void * ssplain_malloc(int size ) { int volatile ___first_local ; void * tmp ; void * __retres ; void * __cil_tmp4 ; void * __cil_tmp5 ; { #line 50 __retres = (void */* */)0; #line 50 tmp = (void */* */)0; #line 48 allocations = allocations + 1UL; #line 49 bytes_allocated = bytes_allocated + (unsigned long )size; #line 50 __cil_tmp5 = (void */* */)/*17*/malloc((((unsigned int )size + 3U) >> 2) << 2); #line 50 if (__cil_tmp5) { #line 50 __cil_tmp4 = __cil_tmp5; #line 50 CHECK_POSITIVE((int )((((unsigned int )size + 3U) >> 2) << 2) - (int )sizeof(void )); } else { #line 50 __cil_tmp4 = 0; } #line 50 tmp = __cil_tmp4; #line 50 __retres = (void */* */)tmp; #line 45 CHECK_RETURNPTR((void *)__retres, (void *)(& ___first_local)); #line 45 return (__retres); } } extern unsigned int ( __attribute__((__cdecl__)) /*28*/calloc)(size_t __nmemb , size_t __size ) ; #line 60 "ssplain.c" static char __string3[17] = #line 60 { 'C', 'a', 'n', 'n', 'o', 't', ' ', 'a', 'l', 'l', 'o', 'c', 'a', 't', 'e', '\n', '\000'}; #line 53 void * ssplain_calloc(int nelems , int size ) ; #line 53 "ssplain.c" void * ssplain_calloc(int nelems , int size ) { int volatile ___first_local ; void * p ; void * __retres ; void * __cil_tmp5 ; void * __cil_tmp6 ; { #line 61 __retres = (void */* */)0; #line 61 p = (void */* */)0; #line 57 allocations = allocations + 1UL; #line 58 bytes_allocated = bytes_allocated + (unsigned long )(nelems * size); #line 59 __cil_tmp6 = (void */* */)/*28*/calloc(1, (((unsigned int )((unsigned int )nelems * (unsigned int )size) + 3U) >> 2) << 2); #line 59 if (__cil_tmp6) { #line 59 __cil_tmp5 = __cil_tmp6; #line 59 CHECK_POSITIVE((int )((((unsigned int )((unsigned int )nelems * (unsigned int )size) + 3U) >> 2) << 2) - (int )sizeof(void )); } else { #line 59 __cil_tmp5 = 0; } #line 59 p = __cil_tmp5; #line 60 if (! ((int )p)) { #line 60 __ccured_va_count = -1; #line 60 printf((char */* */)(& __string3[0])); #line 60 exit(3); } #line 61 __retres = (void */* */)p; #line 53 CHECK_RETURNPTR((void *)__retres, (void *)(& ___first_local)); #line 53 return (__retres); } } #line 67 "ssplain.c" static char __string4[56] = #line 67 { '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 64 void ssplain_alloc_stats(void) ; #line 64 "ssplain.c" void ssplain_alloc_stats(void) { { #line 67 __ccured_va_count = -1; #line 67 chatting((char */* */)((char */* */)(& __string4[0])), (int )bytes_allocated, (int )allocations); #line 64 return; } } void /*22*/free_wrapper_f(void * __FSEQ x , void *x_e ) ; void /*22*/free_wrapper_f(void * __FSEQ x , void *x_e ) { void * tmp ; void * __cil_tmp3 ; { #line 25 "d:/home/db/postdoc/Blast/ccured/include/malloc_wrappers.h" tmp = (void */* */)0; #line 24 if (x) { #line 24 CHECK_FSEQ2SAFE(x_e, (void *)x, sizeof(void ), sizeof(void ), 1, 0); } #line 24 __cil_tmp3 = x; #line 24 tmp = (void */* */)__cil_tmp3; #line 24 free((void */* */)tmp); return; } } extern void /*31*/__verify_nul_f(char * __FSEQ ptr_p , void *ptr_ms_e ) ; __inline static int /*24*/atoi_wrapper_f(char * __FSEQ str , void *str_e ) ; __inline static int /*24*/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 /*31*/__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); } }