/* 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 1 "tsp.h" struct tree { int sz ; double x ; double y ; struct tree * left ; struct tree * right ; struct tree * next ; struct tree * prev ; }; #line 220 "C:/cygwin/lib/gcc-lib/i686-pc-cygwin/3.3.1/include/stddef.h" typedef unsigned int size_t; #line 90 "d:/home/db/postdoc/Blast/ccured/include/gcc_3.3.1/sys/types.h" typedef unsigned long clock_t; #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 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 11 "tsp.h" struct tree * build_tree(int n , int dir , int lo , int num_proc , double min_x , double max_x , double min_y , double max_y ) ; #line 14 struct tree * tsp(struct tree * t , int sz , int nproc ) ; #line 46 "d:/home/db/postdoc/Blast/ccured/include/gcc_3.3.1/time.h" extern clock_t ( __attribute__((__cdecl__)) clock)(void) ; #line 23 "tsp.h" double wallclock ; #line 19 "tsp.c" static struct tree * conquer(struct tree * t ) ; #line 20 static struct tree * merge(struct tree * a , struct tree * b , struct tree * t , int nproc ) ; #line 21 static struct tree * makelist(struct tree * t ) ; #line 22 static void reverse(struct tree * t ) ; #line 23 static double distance(struct tree * a , struct tree * b ) ; #line 24 extern double sqrt(double a ) ; #line 27 static double distance(struct tree * a , struct tree * b ) ; #line 27 "tsp.c" static double distance(struct tree * a , struct tree * b ) { double ax ; double ay ; double bx ; double by ; double tmp ; double __retres ; double __cil_tmp9 ; { #line 30 CHECK_NULL((void *)a); #line 30 ax = a->x; #line 30 CHECK_NULL((void *)a); #line 30 ay = a->y; #line 31 CHECK_NULL((void *)b); #line 31 bx = b->x; #line 31 CHECK_NULL((void *)b); #line 31 by = b->y; #line 32 __cil_tmp9 = sqrt((ax - bx) * (ax - bx) + (ay - by) * (ay - by)); #line 32 tmp = __cil_tmp9; #line 32 __retres = tmp; #line 27 return (__retres); } } #line 37 static struct tree * makelist(struct tree * t ) ; #line 37 "tsp.c" static struct tree * makelist(struct tree * t ) { int volatile ___first_local ; struct tree * left ; struct tree * right ; struct tree * tleft ; struct tree * tright ; struct tree * retval ; int __a_local ; struct tree * __retres ; struct tree * __cil_tmp10 ; struct tree * __cil_tmp11 ; { #line 37 __retres = (struct tree */* */)0; #line 37 retval = (struct tree */* */)0; #line 37 tright = (struct tree */* */)0; #line 37 tleft = (struct tree */* */)0; #line 37 right = (struct tree */* */)0; #line 37 left = (struct tree */* */)0; #line 37 if ((unsigned int )(& __a_local) <= ___stack_threshhold) { #line 37 ___stack_overflow(); } { #line 40 retval = (struct tree */* */)t; #line 42 if (! ((int )t)) { #line 42 CHECK_RETURNPTR((void *)((struct tree */* */)0), (void *)(& ___first_local)); #line 42 return ((struct tree */* */)0); } #line 45 CHECK_NULL((void *)t); #line 45 __cil_tmp10 = makelist((struct tree */* */)t->left); #line 45 left = (struct tree */* */)__cil_tmp10; #line 46 CHECK_NULL((void *)t); #line 46 __cil_tmp11 = makelist((struct tree */* */)t->right); #line 46 right = (struct tree */* */)__cil_tmp11; #line 48 if ((int )right) { #line 48 retval = (struct tree */* */)right; #line 48 CHECK_NULL((void *)t); #line 48 tright = (struct tree */* */)t->right; #line 48 CHECK_NULL((void *)tright); #line 48 CHECK_STOREPTR((void *)(& tright->next), (void *)((struct tree */* */)t), (void *)(& ___first_local)); #line 48 tright->next = (struct tree */* */)t; } #line 49 if ((int )left) { #line 49 retval = (struct tree */* */)left; #line 49 CHECK_NULL((void *)t); #line 49 tleft = (struct tree */* */)t->left; #line 49 if ((int )right) { #line 49 CHECK_NULL((void *)tleft); #line 49 CHECK_STOREPTR((void *)(& tleft->next), (void *)((struct tree */* */)right), (void *)(& ___first_local)); #line 49 tleft->next = (struct tree */* */)right; } else { #line 49 CHECK_NULL((void *)tleft); #line 49 CHECK_STOREPTR((void *)(& tleft->next), (void *)((struct tree */* */)t), (void *)(& ___first_local)); #line 49 tleft->next = (struct tree */* */)t; } } #line 50 CHECK_NULL((void *)t); #line 50 CHECK_STOREPTR((void *)(& t->next), (void *)((struct tree */* */)0), (void *)(& ___first_local)); #line 50 t->next = (struct tree */* */)0; #line 53 CHECK_RETURNPTR((void *)((struct tree */* */)retval), (void *)(& ___first_local)); #line 53 return ((struct tree */* */)retval); } #line 37 CHECK_RETURNPTR((void *)__retres, (void *)(& ___first_local)); #line 37 return (__retres); } } #line 57 static void reverse(struct tree * t ) ; #line 57 "tsp.c" static void reverse(struct tree * t ) { int volatile ___first_local ; struct tree * prev ; struct tree * back ; struct tree * next ; struct tree * tmp ; { #line 78 tmp = (struct tree */* */)0; #line 78 next = (struct tree */* */)0; #line 78 back = (struct tree */* */)0; #line 78 prev = (struct tree */* */)0; #line 60 if (! ((int )t)) { goto return_label; } #line 63 CHECK_NULL((void *)t); #line 63 prev = (struct tree */* */)t->prev; #line 64 CHECK_NULL((void *)prev); #line 64 CHECK_STOREPTR((void *)(& prev->next), (void *)((struct tree */* */)0), (void *)(& ___first_local)); #line 64 prev->next = (struct tree */* */)0; #line 65 CHECK_NULL((void *)t); #line 65 CHECK_STOREPTR((void *)(& t->prev), (void *)((struct tree */* */)0), (void *)(& ___first_local)); #line 65 t->prev = (struct tree */* */)0; #line 66 back = (struct tree */* */)t; #line 67 tmp = (struct tree */* */)t; #line 68 CHECK_NULL((void *)t); #line 68 t = (struct tree */* */)t->next; #line 68 while ((int )t) { #line 69 CHECK_NULL((void *)t); #line 69 next = (struct tree */* */)t->next; #line 70 CHECK_NULL((void *)t); #line 70 CHECK_STOREPTR((void *)(& t->next), (void *)((struct tree */* */)back), (void *)(& ___first_local)); #line 70 t->next = (struct tree */* */)back; #line 71 CHECK_NULL((void *)back); #line 71 CHECK_STOREPTR((void *)(& back->prev), (void *)((struct tree */* */)t), (void *)(& ___first_local)); #line 71 back->prev = (struct tree */* */)t; #line 68 back = (struct tree */* */)t; #line 68 t = (struct tree */* */)next; } #line 73 CHECK_NULL((void *)tmp); #line 73 CHECK_STOREPTR((void *)(& tmp->next), (void *)((struct tree */* */)prev), (void *)(& ___first_local)); #line 73 tmp->next = (struct tree */* */)prev; #line 74 CHECK_NULL((void *)prev); #line 74 CHECK_STOREPTR((void *)(& prev->prev), (void *)((struct tree */* */)tmp), (void *)(& ___first_local)); #line 74 prev->prev = (struct tree */* */)tmp; return_label: /* CIL Label */ #line 57 return; } } #line 81 static struct tree * conquer(struct tree * t ) ; #line 81 "tsp.c" static struct tree * conquer(struct tree * t ) { int volatile ___first_local ; struct tree * cycle ; struct tree * tmp ; struct tree * min ; struct tree * prev ; struct tree * next ; struct tree * donext ; double mindist ; double test ; double mintonext ; double mintoprev ; double ttonext ; double ttoprev ; struct tree * __retres ; struct tree * __cil_tmp15 ; double __cil_tmp17 ; double __cil_tmp18 ; double __cil_tmp19 ; double __cil_tmp20 ; double __cil_tmp21 ; double __cil_tmp22 ; { #line 129 __retres = (struct tree */* */)0; #line 129 donext = (struct tree */* */)0; #line 129 next = (struct tree */* */)0; #line 129 prev = (struct tree */* */)0; #line 129 min = (struct tree */* */)0; #line 129 tmp = (struct tree */* */)0; #line 129 cycle = (struct tree */* */)0; #line 86 if (! ((int )t)) { #line 86 __retres = (struct tree */* */)0; goto return_label; } #line 87 __cil_tmp15 = makelist((struct tree */* */)t); #line 87 t = (struct tree */* */)__cil_tmp15; #line 91 cycle = (struct tree */* */)t; #line 92 CHECK_NULL((void *)t); #line 92 t = (struct tree */* */)t->next; #line 93 CHECK_NULL((void *)cycle); #line 93 CHECK_STOREPTR((void *)(& cycle->next), (void *)((struct tree */* */)cycle), (void *)(& ___first_local)); #line 93 cycle->next = (struct tree */* */)cycle; #line 94 CHECK_NULL((void *)cycle); #line 94 CHECK_STOREPTR((void *)(& cycle->prev), (void *)((struct tree */* */)cycle), (void *)(& ___first_local)); #line 94 cycle->prev = (struct tree */* */)cycle; #line 96 while ((int )t) { #line 97 CHECK_NULL((void *)t); #line 97 donext = (struct tree */* */)t->next; #line 98 min = (struct tree */* */)cycle; #line 99 __cil_tmp17 = distance((struct tree */* */)t, (struct tree */* */)cycle); #line 99 mindist = __cil_tmp17; #line 100 CHECK_NULL((void *)cycle); #line 100 tmp = (struct tree */* */)cycle->next; #line 100 while ((unsigned int )tmp != (unsigned int )cycle) { #line 101 __cil_tmp18 = distance((struct tree */* */)tmp, (struct tree */* */)t); #line 101 test = __cil_tmp18; #line 102 if (test < mindist) { #line 103 mindist = test; #line 104 min = (struct tree */* */)tmp; } #line 100 CHECK_NULL((void *)tmp); #line 100 tmp = (struct tree */* */)tmp->next; } #line 107 CHECK_NULL((void *)min); #line 107 next = (struct tree */* */)min->next; #line 108 CHECK_NULL((void *)min); #line 108 prev = (struct tree */* */)min->prev; #line 109 __cil_tmp19 = distance((struct tree */* */)min, (struct tree */* */)next); #line 109 mintonext = __cil_tmp19; #line 110 __cil_tmp20 = distance((struct tree */* */)min, (struct tree */* */)prev); #line 110 mintoprev = __cil_tmp20; #line 111 __cil_tmp21 = distance((struct tree */* */)t, (struct tree */* */)next); #line 111 ttonext = __cil_tmp21; #line 112 __cil_tmp22 = distance((struct tree */* */)t, (struct tree */* */)prev); #line 112 ttoprev = __cil_tmp22; #line 113 if (ttoprev - mintoprev < ttonext - mintonext) { #line 115 CHECK_NULL((void *)prev); #line 115 CHECK_STOREPTR((void *)(& prev->next), (void *)((struct tree */* */)t), (void *)(& ___first_local)); #line 115 prev->next = (struct tree */* */)t; #line 116 CHECK_NULL((void *)t); #line 116 CHECK_STOREPTR((void *)(& t->next), (void *)((struct tree */* */)min), (void *)(& ___first_local)); #line 116 t->next = (struct tree */* */)min; #line 117 CHECK_NULL((void *)t); #line 117 CHECK_STOREPTR((void *)(& t->prev), (void *)((struct tree */* */)prev), (void *)(& ___first_local)); #line 117 t->prev = (struct tree */* */)prev; #line 118 CHECK_NULL((void *)min); #line 118 CHECK_STOREPTR((void *)(& min->prev), (void *)((struct tree */* */)t), (void *)(& ___first_local)); #line 118 min->prev = (struct tree */* */)t; } else { #line 121 CHECK_NULL((void *)next); #line 121 CHECK_STOREPTR((void *)(& next->prev), (void *)((struct tree */* */)t), (void *)(& ___first_local)); #line 121 next->prev = (struct tree */* */)t; #line 122 CHECK_NULL((void *)t); #line 122 CHECK_STOREPTR((void *)(& t->next), (void *)((struct tree */* */)next), (void *)(& ___first_local)); #line 122 t->next = (struct tree */* */)next; #line 123 CHECK_NULL((void *)min); #line 123 CHECK_STOREPTR((void *)(& min->next), (void *)((struct tree */* */)t), (void *)(& ___first_local)); #line 123 min->next = (struct tree */* */)t; #line 124 CHECK_NULL((void *)t); #line 124 CHECK_STOREPTR((void *)(& t->prev), (void *)((struct tree */* */)min), (void *)(& ___first_local)); #line 124 t->prev = (struct tree */* */)min; } #line 96 t = (struct tree */* */)donext; } #line 129 __retres = (struct tree */* */)cycle; return_label: /* CIL Label */ #line 81 CHECK_RETURNPTR((void *)__retres, (void *)(& ___first_local)); #line 81 return (__retres); } } #line 133 static struct tree * merge(struct tree * a , struct tree * b , struct tree * t , int nproc ) ; #line 133 "tsp.c" static struct tree * merge(struct tree * a , struct tree * b , struct tree * t , int nproc ) { int volatile ___first_local ; struct tree * min ; struct tree * next ; struct tree * prev ; struct tree * tmp ; double mindist ; double test ; double mintonext ; double mintoprev ; double ttonext ; double ttoprev ; struct tree * n1 ; struct tree * p1 ; struct tree * n2 ; struct tree * p2 ; double tton1 ; double ttop1 ; double tton2 ; double ttop2 ; double n1ton2 ; double n1top2 ; double p1ton2 ; double p1top2 ; int choice ; struct tree * __retres ; double __cil_tmp30 ; double __cil_tmp31 ; double __cil_tmp32 ; double __cil_tmp33 ; double __cil_tmp34 ; double __cil_tmp35 ; double __cil_tmp36 ; double __cil_tmp37 ; double __cil_tmp38 ; double __cil_tmp39 ; double __cil_tmp40 ; double __cil_tmp41 ; double __cil_tmp42 ; double __cil_tmp43 ; double __cil_tmp44 ; double __cil_tmp45 ; { #line 279 __retres = (struct tree */* */)0; #line 279 p2 = (struct tree */* */)0; #line 279 n2 = (struct tree */* */)0; #line 279 p1 = (struct tree */* */)0; #line 279 n1 = (struct tree */* */)0; #line 279 tmp = (struct tree */* */)0; #line 279 prev = (struct tree */* */)0; #line 279 next = (struct tree */* */)0; #line 279 min = (struct tree */* */)0; #line 143 min = (struct tree */* */)a; #line 144 __cil_tmp30 = distance((struct tree */* */)t, (struct tree */* */)a); #line 144 mindist = __cil_tmp30; #line 145 tmp = (struct tree */* */)a; #line 150 CHECK_NULL((void *)a); #line 150 a = (struct tree */* */)a->next; #line 150 while ((unsigned int )a != (unsigned int )tmp) { #line 151 __cil_tmp31 = distance((struct tree */* */)a, (struct tree */* */)t); #line 151 test = __cil_tmp31; #line 152 if (test < mindist) { #line 153 mindist = test; #line 154 min = (struct tree */* */)a; } #line 150 CHECK_NULL((void *)a); #line 150 a = (struct tree */* */)a->next; } #line 157 CHECK_NULL((void *)min); #line 157 next = (struct tree */* */)min->next; #line 158 CHECK_NULL((void *)min); #line 158 prev = (struct tree */* */)min->prev; #line 159 __cil_tmp32 = distance((struct tree */* */)min, (struct tree */* */)next); #line 159 mintonext = __cil_tmp32; #line 160 __cil_tmp33 = distance((struct tree */* */)min, (struct tree */* */)prev); #line 160 mintoprev = __cil_tmp33; #line 161 __cil_tmp34 = distance((struct tree */* */)t, (struct tree */* */)next); #line 161 ttonext = __cil_tmp34; #line 162 __cil_tmp35 = distance((struct tree */* */)t, (struct tree */* */)prev); #line 162 ttoprev = __cil_tmp35; #line 163 if (ttoprev - mintoprev < ttonext - mintonext) { #line 165 p1 = (struct tree */* */)prev; #line 166 n1 = (struct tree */* */)min; #line 167 tton1 = mindist; #line 168 ttop1 = ttoprev; } else { #line 171 p1 = (struct tree */* */)min; #line 172 n1 = (struct tree */* */)next; #line 173 ttop1 = mindist; #line 174 tton1 = ttonext; } #line 178 min = (struct tree */* */)b; #line 179 __cil_tmp36 = distance((struct tree */* */)t, (struct tree */* */)b); #line 179 mindist = __cil_tmp36; #line 180 tmp = (struct tree */* */)b; #line 181 CHECK_NULL((void *)b); #line 181 b = (struct tree */* */)b->next; #line 181 while ((unsigned int )b != (unsigned int )tmp) { #line 182 __cil_tmp37 = distance((struct tree */* */)b, (struct tree */* */)t); #line 182 test = __cil_tmp37; #line 183 if (test < mindist) { #line 184 mindist = test; #line 185 min = (struct tree */* */)b; } #line 181 CHECK_NULL((void *)b); #line 181 b = (struct tree */* */)b->next; } #line 188 CHECK_NULL((void *)min); #line 188 next = (struct tree */* */)min->next; #line 189 CHECK_NULL((void *)min); #line 189 prev = (struct tree */* */)min->prev; #line 190 __cil_tmp38 = distance((struct tree */* */)min, (struct tree */* */)next); #line 190 mintonext = __cil_tmp38; #line 191 __cil_tmp39 = distance((struct tree */* */)min, (struct tree */* */)prev); #line 191 mintoprev = __cil_tmp39; #line 192 __cil_tmp40 = distance((struct tree */* */)t, (struct tree */* */)next); #line 192 ttonext = __cil_tmp40; #line 193 __cil_tmp41 = distance((struct tree */* */)t, (struct tree */* */)prev); #line 193 ttoprev = __cil_tmp41; #line 194 if (ttoprev - mintoprev < ttonext - mintonext) { #line 196 p2 = (struct tree */* */)prev; #line 197 n2 = (struct tree */* */)min; #line 198 tton2 = mindist; #line 199 ttop2 = ttoprev; } else { #line 202 p2 = (struct tree */* */)min; #line 203 n2 = (struct tree */* */)next; #line 204 ttop2 = mindist; #line 205 tton2 = ttonext; } #line 213 __cil_tmp42 = distance((struct tree */* */)n1, (struct tree */* */)n2); #line 213 n1ton2 = __cil_tmp42; #line 214 __cil_tmp43 = distance((struct tree */* */)n1, (struct tree */* */)p2); #line 214 n1top2 = __cil_tmp43; #line 215 __cil_tmp44 = distance((struct tree */* */)p1, (struct tree */* */)n2); #line 215 p1ton2 = __cil_tmp44; #line 216 __cil_tmp45 = distance((struct tree */* */)p1, (struct tree */* */)p2); #line 216 p1top2 = __cil_tmp45; #line 218 mindist = (ttop1 + ttop2) + n1ton2; #line 219 choice = 1; #line 221 test = (ttop1 + tton2) + n1top2; #line 222 if (test < mindist) { #line 223 choice = 2; #line 224 mindist = test; } #line 227 test = (tton1 + ttop2) + p1ton2; #line 228 if (test < mindist) { #line 229 choice = 3; #line 230 mindist = test; } #line 233 test = (tton1 + tton2) + p1top2; #line 234 if (test < mindist) { #line 234 choice = 4; } #line 237 switch (choice) { case 1: #line 241 reverse((struct tree */* */)n2); #line 242 CHECK_NULL((void *)p1); #line 242 CHECK_STOREPTR((void *)(& p1->next), (void *)((struct tree */* */)t), (void *)(& ___first_local)); #line 242 p1->next = (struct tree */* */)t; #line 243 CHECK_NULL((void *)t); #line 243 CHECK_STOREPTR((void *)(& t->prev), (void *)((struct tree */* */)p1), (void *)(& ___first_local)); #line 243 t->prev = (struct tree */* */)p1; #line 244 CHECK_NULL((void *)t); #line 244 CHECK_STOREPTR((void *)(& t->next), (void *)((struct tree */* */)p2), (void *)(& ___first_local)); #line 244 t->next = (struct tree */* */)p2; #line 245 CHECK_NULL((void *)p2); #line 245 CHECK_STOREPTR((void *)(& p2->prev), (void *)((struct tree */* */)t), (void *)(& ___first_local)); #line 245 p2->prev = (struct tree */* */)t; #line 246 CHECK_NULL((void *)n2); #line 246 CHECK_STOREPTR((void *)(& n2->next), (void *)((struct tree */* */)n1), (void *)(& ___first_local)); #line 246 n2->next = (struct tree */* */)n1; #line 247 CHECK_NULL((void *)n1); #line 247 CHECK_STOREPTR((void *)(& n1->prev), (void *)((struct tree */* */)n2), (void *)(& ___first_local)); #line 247 n1->prev = (struct tree */* */)n2; #line 248 break; case 2: #line 251 CHECK_NULL((void *)p1); #line 251 CHECK_STOREPTR((void *)(& p1->next), (void *)((struct tree */* */)t), (void *)(& ___first_local)); #line 251 p1->next = (struct tree */* */)t; #line 252 CHECK_NULL((void *)t); #line 252 CHECK_STOREPTR((void *)(& t->prev), (void *)((struct tree */* */)p1), (void *)(& ___first_local)); #line 252 t->prev = (struct tree */* */)p1; #line 253 CHECK_NULL((void *)t); #line 253 CHECK_STOREPTR((void *)(& t->next), (void *)((struct tree */* */)n2), (void *)(& ___first_local)); #line 253 t->next = (struct tree */* */)n2; #line 254 CHECK_NULL((void *)n2); #line 254 CHECK_STOREPTR((void *)(& n2->prev), (void *)((struct tree */* */)t), (void *)(& ___first_local)); #line 254 n2->prev = (struct tree */* */)t; #line 255 CHECK_NULL((void *)p2); #line 255 CHECK_STOREPTR((void *)(& p2->next), (void *)((struct tree */* */)n1), (void *)(& ___first_local)); #line 255 p2->next = (struct tree */* */)n1; #line 256 CHECK_NULL((void *)n1); #line 256 CHECK_STOREPTR((void *)(& n1->prev), (void *)((struct tree */* */)p2), (void *)(& ___first_local)); #line 256 n1->prev = (struct tree */* */)p2; #line 257 break; case 3: #line 260 CHECK_NULL((void *)p2); #line 260 CHECK_STOREPTR((void *)(& p2->next), (void *)((struct tree */* */)t), (void *)(& ___first_local)); #line 260 p2->next = (struct tree */* */)t; #line 261 CHECK_NULL((void *)t); #line 261 CHECK_STOREPTR((void *)(& t->prev), (void *)((struct tree */* */)p2), (void *)(& ___first_local)); #line 261 t->prev = (struct tree */* */)p2; #line 262 CHECK_NULL((void *)t); #line 262 CHECK_STOREPTR((void *)(& t->next), (void *)((struct tree */* */)n1), (void *)(& ___first_local)); #line 262 t->next = (struct tree */* */)n1; #line 263 CHECK_NULL((void *)n1); #line 263 CHECK_STOREPTR((void *)(& n1->prev), (void *)((struct tree */* */)t), (void *)(& ___first_local)); #line 263 n1->prev = (struct tree */* */)t; #line 264 CHECK_NULL((void *)p1); #line 264 CHECK_STOREPTR((void *)(& p1->next), (void *)((struct tree */* */)n2), (void *)(& ___first_local)); #line 264 p1->next = (struct tree */* */)n2; #line 265 CHECK_NULL((void *)n2); #line 265 CHECK_STOREPTR((void *)(& n2->prev), (void *)((struct tree */* */)p1), (void *)(& ___first_local)); #line 265 n2->prev = (struct tree */* */)p1; #line 266 break; case 4: #line 270 reverse((struct tree */* */)n1); #line 271 CHECK_NULL((void *)n1); #line 271 CHECK_STOREPTR((void *)(& n1->next), (void *)((struct tree */* */)t), (void *)(& ___first_local)); #line 271 n1->next = (struct tree */* */)t; #line 272 CHECK_NULL((void *)t); #line 272 CHECK_STOREPTR((void *)(& t->prev), (void *)((struct tree */* */)n1), (void *)(& ___first_local)); #line 272 t->prev = (struct tree */* */)n1; #line 273 CHECK_NULL((void *)t); #line 273 CHECK_STOREPTR((void *)(& t->next), (void *)((struct tree */* */)n2), (void *)(& ___first_local)); #line 273 t->next = (struct tree */* */)n2; #line 274 CHECK_NULL((void *)n2); #line 274 CHECK_STOREPTR((void *)(& n2->prev), (void *)((struct tree */* */)t), (void *)(& ___first_local)); #line 274 n2->prev = (struct tree */* */)t; #line 275 CHECK_NULL((void *)p2); #line 275 CHECK_STOREPTR((void *)(& p2->next), (void *)((struct tree */* */)p1), (void *)(& ___first_local)); #line 275 p2->next = (struct tree */* */)p1; #line 276 CHECK_NULL((void *)p1); #line 276 CHECK_STOREPTR((void *)(& p1->prev), (void *)((struct tree */* */)p2), (void *)(& ___first_local)); #line 276 p1->prev = (struct tree */* */)p2; #line 277 break; } #line 279 __retres = (struct tree */* */)t; #line 133 CHECK_RETURNPTR((void *)__retres, (void *)(& ___first_local)); #line 133 return (__retres); } } #line 283 struct tree * tsp(struct tree * t , int sz , int nproc ) ; #line 283 "tsp.c" struct tree * tsp(struct tree * t , int sz , int nproc ) { int volatile ___first_local ; struct tree * left ; struct tree * right ; struct tree * leftval ; struct tree * rightval ; int nproc_2 ; struct tree * tmp ; struct tree * tmp___0 ; int __a_local ; struct tree * __retres ; struct tree * __cil_tmp13 ; struct tree * __cil_tmp15 ; struct tree * __cil_tmp16 ; struct tree * __cil_tmp17 ; { #line 283 __retres = (struct tree */* */)0; #line 283 tmp___0 = (struct tree */* */)0; #line 283 tmp = (struct tree */* */)0; #line 283 rightval = (struct tree */* */)0; #line 283 leftval = (struct tree */* */)0; #line 283 right = (struct tree */* */)0; #line 283 left = (struct tree */* */)0; #line 283 if ((unsigned int )(& __a_local) <= ___stack_threshhold) { #line 283 ___stack_overflow(); } { #line 290 nproc_2 = nproc / 2; #line 292 CHECK_NULL((void *)t); #line 292 if (t->sz <= sz) { #line 292 __cil_tmp13 = conquer((struct tree */* */)t); #line 292 tmp = (struct tree */* */)__cil_tmp13; #line 292 CHECK_RETURNPTR((void *)((struct tree */* */)tmp), (void *)(& ___first_local)); #line 292 return ((struct tree */* */)tmp); } #line 294 CHECK_NULL((void *)t); #line 294 left = (struct tree */* */)t->left; #line 294 CHECK_NULL((void *)t); #line 294 right = (struct tree */* */)t->right; #line 296 __cil_tmp15 = tsp((struct tree */* */)left, sz, nproc_2); #line 296 leftval = (struct tree */* */)__cil_tmp15; #line 300 __cil_tmp16 = tsp((struct tree */* */)right, sz, nproc_2); #line 300 rightval = (struct tree */* */)__cil_tmp16; #line 306 __cil_tmp17 = merge((struct tree */* */)leftval, (struct tree */* */)rightval, (struct tree */* */)t, nproc); #line 306 tmp___0 = (struct tree */* */)__cil_tmp17; #line 306 CHECK_RETURNPTR((void *)((struct tree */* */)tmp___0), (void *)(& ___first_local)); #line 306 return ((struct tree */* */)tmp___0); } #line 283 CHECK_RETURNPTR((void *)__retres, (void *)(& ___first_local)); #line 283 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 15 "build.c" double ( __attribute__((__cdecl__)) drand48)(void) ; #line 18 extern double log(double x ) ; #line 65 "d:/home/db/postdoc/Blast/ccured/include/gcc_3.3.1/stdlib.h" extern __attribute__((__noreturn__)) void ( __attribute__((__cdecl__)) exit)(int __status ) ; #line 91 extern int ( __attribute__((__cdecl__)) rand)(void) ; #line 38 "build.c" static double median(double min , double max , int n ) ; #line 39 static double uniform(double min , double max ) ; #line 41 double ( __attribute__((__cdecl__)) drand48)(void) ; #line 41 "build.c" double ( __attribute__((__cdecl__)) drand48)(void) { int tmp ; double __retres ; int __cil_tmp3 ; { #line 42 __cil_tmp3 = rand(); #line 42 tmp = __cil_tmp3; #line 42 __retres = (double )tmp / (double )2147483647; #line 41 return (__retres); } } #line 46 static double median(double min , double max , int n ) ; #line 46 "build.c" static double median(double min , double max , int n ) { double t ; double retval ; double tmp ; double tmp___0 ; double __retres ; double __cil_tmp9 ; double __cil_tmp10 ; double __cil_tmp11 ; { #line 50 __cil_tmp9 = drand48(); #line 50 t = __cil_tmp9; #line 51 if (t > 0.5) { #line 52 __cil_tmp11 = log(1.0 - ((2.0 * (162754.79141900392083592475 - (double )1)) * (t - 0.5)) / 162754.79141900392083592475); #line 52 tmp = __cil_tmp11; #line 52 retval = tmp / 12.0; } else { #line 55 __cil_tmp10 = log(1.0 - ((2.0 * (162754.79141900392083592475 - (double )1)) * t) / 162754.79141900392083592475); #line 55 tmp___0 = __cil_tmp10; #line 55 retval = - (tmp___0 / 12.0); } #line 58 retval = ((retval + 1.0) * (max - min)) / 2.0; #line 59 retval = retval + min; #line 60 __retres = retval; #line 46 return (__retres); } } #line 64 static double uniform(double min , double max ) ; #line 64 "build.c" static double uniform(double min , double max ) { double retval ; double __retres ; double __cil_tmp5 ; { #line 67 __cil_tmp5 = drand48(); #line 67 retval = __cil_tmp5; #line 68 retval = retval * (max - min); #line 69 __retres = retval + min; #line 64 return (__retres); } } extern unsigned int ( __attribute__((__cdecl__)) /*9*/malloc)(size_t __size ) ; #line 77 struct tree * build_tree(int n , int dir , int lo , int num_proc , double min_x , double max_x , double min_y , double max_y ) ; #line 77 "build.c" struct tree * build_tree(int n , int dir , int lo , int num_proc , double min_x , double max_x , double min_y , double max_y ) { int volatile ___first_local ; double med ; struct tree * t ; int __a_local ; struct tree * __retres ; struct tree * __cil_tmp15 ; struct tree * __cil_tmp16 ; double __cil_tmp17 ; struct tree * __cil_tmp18 ; struct tree * __cil_tmp19 ; double __cil_tmp20 ; double __cil_tmp21 ; struct tree * __cil_tmp22 ; struct tree * __cil_tmp23 ; double __cil_tmp24 ; { #line 77 __retres = (struct tree */* */)0; #line 77 t = (struct tree */* */)0; #line 77 if ((unsigned int )(& __a_local) <= ___stack_threshhold) { #line 77 ___stack_overflow(); } { #line 85 if (n == 0) { #line 85 CHECK_RETURNPTR((void *)((struct tree */* */)0), (void *)(& ___first_local)); #line 85 return ((struct tree */* */)0); } #line 87 __cil_tmp16 = (struct tree */* */)/*9*/malloc(((sizeof((*t)) + 3U) >> 2) << 2); #line 87 if (__cil_tmp16) { #line 87 __cil_tmp15 = __cil_tmp16; #line 87 CHECK_POSITIVE((int )(((sizeof((*t)) + 3U) >> 2) << 2) - (int )sizeof(struct tree )); #line 87 __cil_tmp16->prev = (struct tree */* */)0; #line 87 __cil_tmp16->next = (struct tree */* */)0; #line 87 __cil_tmp16->right = (struct tree */* */)0; #line 87 __cil_tmp16->left = (struct tree */* */)0; } else { #line 87 __cil_tmp15 = 0; } #line 87 t = __cil_tmp15; #line 88 if (dir) { #line 89 dir = ! dir != 0; #line 90 __cil_tmp21 = median(min_x, max_x, n); #line 90 med = __cil_tmp21; #line 92 __cil_tmp22 = build_tree(n / 2, dir, lo + num_proc / 2, num_proc / 2, min_x, med, min_y, max_y); #line 92 CHECK_NULL((void *)t); #line 92 CHECK_STOREPTR((void *)(& t->left), (void *)((struct tree */* */)__cil_tmp22), (void *)(& ___first_local)); #line 92 t->left = (struct tree */* */)__cil_tmp22; #line 93 __cil_tmp23 = build_tree(n / 2, dir, lo, num_proc / 2, med, max_x, min_y, max_y); #line 93 CHECK_NULL((void *)t); #line 93 CHECK_STOREPTR((void *)(& t->right), (void *)((struct tree */* */)__cil_tmp23), (void *)(& ___first_local)); #line 93 t->right = (struct tree */* */)__cil_tmp23; #line 99 CHECK_NULL((void *)t); #line 99 t->x = med; #line 100 __cil_tmp24 = uniform(min_y, max_y); #line 100 CHECK_NULL((void *)t); #line 100 t->y = __cil_tmp24; } else { #line 103 dir = ! dir != 0; #line 104 __cil_tmp17 = median(min_y, max_y, n); #line 104 med = __cil_tmp17; #line 106 __cil_tmp18 = build_tree(n / 2, dir, lo + num_proc / 2, num_proc / 2, min_x, max_x, min_y, med); #line 106 CHECK_NULL((void *)t); #line 106 CHECK_STOREPTR((void *)(& t->left), (void *)((struct tree */* */)__cil_tmp18), (void *)(& ___first_local)); #line 106 t->left = (struct tree */* */)__cil_tmp18; #line 107 __cil_tmp19 = build_tree(n / 2, dir, lo, num_proc / 2, min_x, max_x, med, max_y); #line 107 CHECK_NULL((void *)t); #line 107 CHECK_STOREPTR((void *)(& t->right), (void *)((struct tree */* */)__cil_tmp19), (void *)(& ___first_local)); #line 107 t->right = (struct tree */* */)__cil_tmp19; #line 113 CHECK_NULL((void *)t); #line 113 t->y = med; #line 114 __cil_tmp20 = uniform(min_x, max_x); #line 114 CHECK_NULL((void *)t); #line 114 t->x = __cil_tmp20; } #line 116 CHECK_NULL((void *)t); #line 116 t->sz = n; #line 117 CHECK_NULL((void *)t); #line 117 CHECK_STOREPTR((void *)(& t->next), (void *)((struct tree */* */)0), (void *)(& ___first_local)); #line 117 t->next = (struct tree */* */)0; #line 118 CHECK_NULL((void *)t); #line 118 CHECK_STOREPTR((void *)(& t->prev), (void *)((struct tree */* */)0), (void *)(& ___first_local)); #line 118 t->prev = (struct tree */* */)0; #line 123 CHECK_RETURNPTR((void *)((struct tree */* */)t), (void *)(& ___first_local)); #line 123 return ((struct tree */* */)t); } #line 77 CHECK_RETURNPTR((void *)__retres, (void *)(& ___first_local)); #line 77 return (__retres); } } #line 23 "tsp.h" double wallclock ; #line 15 "main.c" int flag ; #line 16 "main.c" int __NumNodes ; #line 16 "main.c" int __NDim ; #line 18 int mylog(int num ) ; #line 18 "main.c" int mylog(int num ) { int j ; int k ; int __retres ; { #line 20 j = 0; #line 20 k = 1; #line 22 while (k < num) { #line 22 k = k * 2; #line 22 j = j + 1; } #line 23 __retres = j; #line 18 return (__retres); } } #line 26 int dealwithargs(void) ; #line 26 "main.c" int dealwithargs(void) { int num ; int __retres ; int __cil_tmp3 ; { #line 30 flag = 0; #line 31 __NumNodes = 4; #line 33 __cil_tmp3 = mylog(__NumNodes); #line 33 __NDim = __cil_tmp3; #line 35 num = 150000; #line 37 __retres = num; #line 26 return (__retres); } } #line 47 extern int __ccured_va_count ; #line 47 "main.c" static char __string1[11] = #line 47 { 'x', '=', '%', 'f', ',', 'y', '=', '%', 'f', '\n', '\000'}; #line 40 void print_tree(struct tree * t ) ; #line 40 "main.c" void print_tree(struct tree * t ) { struct tree * left ; struct tree * right ; double x ; double y ; int __a_local ; { #line 40 right = (struct tree */* */)0; #line 40 left = (struct tree */* */)0; #line 40 if ((unsigned int )(& __a_local) <= ___stack_threshhold) { #line 40 ___stack_overflow(); } { #line 45 if (! ((int )t)) { #line 45 return; } #line 46 CHECK_NULL((void *)t); #line 46 x = t->x; #line 46 CHECK_NULL((void *)t); #line 46 y = t->y; #line 47 __ccured_va_count = -1; #line 47 printf((char */* */)(& __string1[0]), x, y); #line 48 CHECK_NULL((void *)t); #line 48 left = (struct tree */* */)t->left; #line 48 CHECK_NULL((void *)t); #line 48 right = (struct tree */* */)t->right; #line 49 print_tree((struct tree */* */)left); #line 50 print_tree((struct tree */* */)right); #line 51 return; } #line 40 return; } } #line 60 "main.c" static char __string2[7] = { '%', 'f', ' ', '%', 'f', '\n', '\000'}; #line 64 "main.c" static char __string3[7] = { '%', 'f', ' ', '%', 'f', '\n', '\000'}; #line 53 void print_list(struct tree * t ) ; #line 53 "main.c" void print_list(struct tree * t ) { struct tree * tmp ; double x ; double y ; { #line 66 tmp = (struct tree */* */)0; #line 58 if (! ((int )t)) { goto return_label; } #line 59 CHECK_NULL((void *)t); #line 59 x = t->x; #line 59 CHECK_NULL((void *)t); #line 59 y = t->y; #line 60 __ccured_va_count = -1; #line 60 printf((char */* */)(& __string2[0]), x, y); #line 61 CHECK_NULL((void *)t); #line 61 tmp = (struct tree */* */)t->next; #line 61 while ((unsigned int )tmp != (unsigned int )t) { #line 63 CHECK_NULL((void *)tmp); #line 63 x = tmp->x; #line 63 CHECK_NULL((void *)tmp); #line 63 y = tmp->y; #line 64 __ccured_va_count = -1; #line 64 printf((char */* */)(& __string3[0]), x, y); #line 61 CHECK_NULL((void *)tmp); #line 61 tmp = (struct tree */* */)tmp->next; } return_label: /* CIL Label */ #line 53 return; } } #line 77 "main.c" static char __string4[26] = #line 77 { 'B', 'u', 'i', 'l', 'd', 'i', 'n', 'g', ' ', 't', 'r', 'e', 'e', ' ', 'o', 'f', ' ', 's', 'i', 'z', 'e', ' ', '%', 'd', '\n', '\000'}; #line 82 "main.c" static char __string5[12] = #line 82 { 'P', 'a', 's', 't', ' ', 'b', 'u', 'i', 'l', 'd', '\n', '\000'}; #line 83 "main.c" static char __string6[10] = #line 83 { 'n', 'e', 'w', 'g', 'r', 'a', 'p', 'h', '\n', '\000'}; #line 84 "main.c" static char __string7[14] = #line 84 { 'n', 'e', 'w', 'c', 'u', 'r', 'v', 'e', ' ', 'p', 't', 's', '\n', '\000'}; #line 91 "main.c" static char __string8[16] = #line 91 { 'l', 'i', 'n', 'e', 't', 'y', 'p', 'e', ' ', 's', 'o', 'l', 'i', 'd', '\n', '\000'}; #line 92 "main.c" static char __string9[19] = #line 92 { 'T', 'i', 'm', 'e', ' ', 'f', 'o', 'r', ' ', 'T', 'S', 'P', ' ', '=', ' ', '%', 'f', '\n', '\000'}; #line 70 int main(void) ; #line 70 "main.c" int main(void) { struct tree * t ; int num ; clock_t tmp___0 ; int __retres ; unsigned int __cil_tmp7 ; int __cil_tmp8 ; struct tree * __cil_tmp9 ; clock_t __cil_tmp10 ; clock_t __cil_tmp11 ; { #line 70 t = (struct tree */* */)0; #line 70 __ccuredAlwaysStopOnError = 1; #line 70 __ccuredUseStrings = 0; #line 70 __ccuredLogNonPointers = 0; #line 70 __ccuredInit(); #line 70 __cil_tmp7 = ___compute_stack_threshhold(); #line 70 ___stack_threshhold = __cil_tmp7; { #line 75 __cil_tmp8 = dealwithargs(); #line 75 num = __cil_tmp8; #line 77 __ccured_va_count = -1; #line 77 printf((char */* */)(& __string4[0]), num); #line 78 __cil_tmp9 = build_tree(num, 0, 0, __NumNodes, 0.0, 1.0, 0.0, 1.0); #line 78 t = (struct tree */* */)__cil_tmp9; #line 82 if (! flag) { #line 82 __ccured_va_count = -1; #line 82 printf((char */* */)(& __string5[0])); } #line 83 if (flag) { #line 83 __ccured_va_count = -1; #line 83 printf((char */* */)(& __string6[0])); } #line 84 if (flag) { #line 84 __ccured_va_count = -1; #line 84 printf((char */* */)(& __string7[0])); } #line 87 __cil_tmp10 = clock(); #line 87 wallclock = (double )__cil_tmp10; #line 88 tsp((struct tree */* */)t, 150, __NumNodes); #line 89 __cil_tmp11 = clock(); #line 89 tmp___0 = __cil_tmp11; #line 89 wallclock = (1000000.0 * ((double )tmp___0 - wallclock)) / (double )1000; #line 90 if (flag) { #line 90 print_list((struct tree */* */)t); } #line 91 if (flag) { #line 91 __ccured_va_count = -1; #line 91 printf((char */* */)(& __string8[0])); } #line 92 __ccured_va_count = -1; #line 92 printf((char */* */)(& __string9[0]), wallclock / 1000.0); #line 100 exit(0); } #line 70 return (__retres); } }