/* 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 12 "perimeter.h" enum __anonenum_Color_1 { black = 0, white = 1, grey = 2 }; #line 12 "perimeter.h" typedef enum __anonenum_Color_1 Color; #line 13 enum __anonenum_ChildType_2 { northwest = 0, northeast = 1, southwest = 2, southeast = 3 }; #line 13 "perimeter.h" typedef enum __anonenum_ChildType_2 ChildType; #line 14 enum __anonenum_Direction_3 { north = 0, east = 1, south = 2, west = 3 }; #line 14 "perimeter.h" typedef enum __anonenum_Direction_3 Direction; #line 16 "perimeter.h" struct quad_struct { Color color ; ChildType childtype ; struct quad_struct * nw ; struct quad_struct * ne ; struct quad_struct * sw ; struct quad_struct * se ; struct quad_struct * parent ; }; #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 26 "perimeter.h" struct quad_struct * MakeTree(int size , int center_x , int center_y , int lo_proc , int hi_proc , struct quad_struct * parent , ChildType ct , int level ) ; #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 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 35 "perimeter.h" int __NumNodes ; #line 46 "d:/home/db/postdoc/Blast/ccured/include/gcc_3.3.1/time.h" extern clock_t ( __attribute__((__cdecl__)) clock)(void) ; #line 44 "perimeter.h" double wallclock ; #line 3 "maketree.c" static int CheckOutside(int x , int y ) ; #line 3 "maketree.c" static int CheckOutside(int x , int y ) { int euclid ; int __retres ; { #line 5 euclid = x * x + y * y; #line 7 if (euclid > 4194304) { #line 7 __retres = 1; goto return_label; } #line 8 if (euclid < 1048576) { #line 8 __retres = -1; goto return_label; } #line 9 __retres = 0; return_label: /* CIL Label */ ; #line 3 return (__retres); } } #line 12 static int CheckIntersect(int center_x , int center_y , int size ) ; #line 12 "maketree.c" static int CheckIntersect(int center_x , int center_y , int size ) { int sum ; int tmp ; int tmp___0 ; int tmp___1 ; int tmp___2 ; int tmp___3 ; int tmp___4 ; int tmp___5 ; int tmp___6 ; int __retres ; int __cil_tmp14 ; int __cil_tmp15 ; int __cil_tmp16 ; int __cil_tmp17 ; int __cil_tmp18 ; int __cil_tmp19 ; int __cil_tmp20 ; int __cil_tmp21 ; { #line 16 __cil_tmp14 = CheckOutside(center_x + size, center_y + size); #line 16 tmp = __cil_tmp14; #line 16 if (! tmp) { #line 16 __cil_tmp15 = CheckOutside(center_x + size, center_y - size); #line 16 tmp___0 = __cil_tmp15; #line 16 if (! tmp___0) { #line 16 __cil_tmp16 = CheckOutside(center_x - size, center_y - size); #line 16 tmp___1 = __cil_tmp16; #line 16 if (! tmp___1) { #line 16 __cil_tmp17 = CheckOutside(center_x - size, center_y + size); #line 16 tmp___2 = __cil_tmp17; #line 16 if (! tmp___2) { #line 19 __retres = 2; goto return_label; } } } } #line 20 __cil_tmp18 = CheckOutside(center_x + size, center_y + size); #line 20 tmp___3 = __cil_tmp18; #line 20 __cil_tmp19 = CheckOutside(center_x + size, center_y - size); #line 20 tmp___4 = __cil_tmp19; #line 20 __cil_tmp20 = CheckOutside(center_x - size, center_y - size); #line 20 tmp___5 = __cil_tmp20; #line 20 __cil_tmp21 = CheckOutside(center_x - size, center_y + size); #line 20 tmp___6 = __cil_tmp21; #line 20 sum = ((tmp___3 + tmp___4) + tmp___5) + tmp___6; #line 24 if (sum == 4) { #line 24 __retres = 0; goto return_label; } else { #line 24 if (sum == -4) { #line 24 __retres = 0; goto return_label; } } #line 25 __retres = 1; return_label: /* CIL Label */ ; #line 12 return (__retres); } } extern unsigned int ( __attribute__((__cdecl__)) /*9*/malloc)(size_t __size ) ; #line 28 struct quad_struct * MakeTree(int size , int center_x , int center_y , int lo_proc , int hi_proc , struct quad_struct * parent , ChildType ct , int level ) ; #line 28 "maketree.c" struct quad_struct * MakeTree(int size , int center_x , int center_y , int lo_proc , int hi_proc , struct quad_struct * parent , ChildType ct , int level ) { int volatile ___first_local ; int intersect ; struct quad_struct * retval ; int mid1 ; int mid2 ; int __a_local ; struct quad_struct * __retres ; struct quad_struct * __cil_tmp16 ; struct quad_struct * __cil_tmp17 ; int __cil_tmp19 ; struct quad_struct * __cil_tmp20 ; struct quad_struct * __cil_tmp21 ; struct quad_struct * __cil_tmp22 ; struct quad_struct * __cil_tmp23 ; { #line 28 __retres = (struct quad_struct */* */)0; #line 28 retval = (struct quad_struct */* */)0; #line 28 if ((unsigned int )(& __a_local) <= ___stack_threshhold) { #line 28 ___stack_overflow(); } { #line 31 intersect = 0; #line 37 __cil_tmp17 = (struct quad_struct */* */)/*9*/malloc(((sizeof((*retval)) + 3U) >> 2) << 2); #line 37 if (__cil_tmp17) { #line 37 __cil_tmp16 = __cil_tmp17; #line 37 __cil_tmp17->parent = (struct quad_struct */* */)0; #line 37 __cil_tmp17->se = (struct quad_struct */* */)0; #line 37 __cil_tmp17->sw = (struct quad_struct */* */)0; #line 37 __cil_tmp17->ne = (struct quad_struct */* */)0; #line 37 __cil_tmp17->nw = (struct quad_struct */* */)0; } else { #line 37 __cil_tmp16 = 0; } #line 37 retval = __cil_tmp16; #line 39 CHECK_NULL((void *)retval); #line 39 CHECK_STOREPTR((void *)(& retval->parent), (void *)((struct quad_struct */* */)parent), (void *)(& ___first_local)); #line 39 retval->parent = (struct quad_struct */* */)parent; #line 40 retval->childtype = ct; #line 42 __cil_tmp19 = CheckIntersect(center_x, center_y, size); #line 42 intersect = __cil_tmp19; #line 43 size = size / 2; #line 44 if (intersect == 0) { #line 44 if (size < 512) { #line 46 CHECK_NULL((void *)retval); #line 46 retval->color = (Color )1; #line 47 CHECK_STOREPTR((void *)(& retval->nw), (void *)((struct quad_struct */* */)0), (void *)(& ___first_local)); #line 47 retval->nw = (struct quad_struct */* */)0; #line 48 CHECK_STOREPTR((void *)(& retval->ne), (void *)((struct quad_struct */* */)0), (void *)(& ___first_local)); #line 48 retval->ne = (struct quad_struct */* */)0; #line 49 CHECK_STOREPTR((void *)(& retval->sw), (void *)((struct quad_struct */* */)0), (void *)(& ___first_local)); #line 49 retval->sw = (struct quad_struct */* */)0; #line 50 CHECK_STOREPTR((void *)(& retval->se), (void *)((struct quad_struct */* */)0), (void *)(& ___first_local)); #line 50 retval->se = (struct quad_struct */* */)0; } else { goto _L; } } else { _L: /* CIL Label */ ; #line 52 if (intersect == 2) { #line 54 CHECK_NULL((void *)retval); #line 54 retval->color = (Color )0; #line 55 CHECK_STOREPTR((void *)(& retval->nw), (void *)((struct quad_struct */* */)0), (void *)(& ___first_local)); #line 55 retval->nw = (struct quad_struct */* */)0; #line 56 CHECK_STOREPTR((void *)(& retval->ne), (void *)((struct quad_struct */* */)0), (void *)(& ___first_local)); #line 56 retval->ne = (struct quad_struct */* */)0; #line 57 CHECK_STOREPTR((void *)(& retval->sw), (void *)((struct quad_struct */* */)0), (void *)(& ___first_local)); #line 57 retval->sw = (struct quad_struct */* */)0; #line 58 CHECK_STOREPTR((void *)(& retval->se), (void *)((struct quad_struct */* */)0), (void *)(& ___first_local)); #line 58 retval->se = (struct quad_struct */* */)0; } else { #line 62 if (! level) { #line 64 CHECK_NULL((void *)retval); #line 64 retval->color = (Color )0; #line 65 CHECK_STOREPTR((void *)(& retval->nw), (void *)((struct quad_struct */* */)0), (void *)(& ___first_local)); #line 65 retval->nw = (struct quad_struct */* */)0; #line 66 CHECK_STOREPTR((void *)(& retval->ne), (void *)((struct quad_struct */* */)0), (void *)(& ___first_local)); #line 66 retval->ne = (struct quad_struct */* */)0; #line 67 CHECK_STOREPTR((void *)(& retval->sw), (void *)((struct quad_struct */* */)0), (void *)(& ___first_local)); #line 67 retval->sw = (struct quad_struct */* */)0; #line 68 CHECK_STOREPTR((void *)(& retval->se), (void *)((struct quad_struct */* */)0), (void *)(& ___first_local)); #line 68 retval->se = (struct quad_struct */* */)0; } else { #line 77 mid1 = (lo_proc + hi_proc) / 2; #line 78 mid2 = ((lo_proc + hi_proc) + 1) / 2; #line 81 __cil_tmp20 = MakeTree(size, center_x - size, center_y - size, ((mid2 + hi_proc) + 1) / 2, hi_proc, (struct quad_struct */* */)retval, (ChildType )2, level - 1); #line 81 CHECK_NULL((void *)retval); #line 81 CHECK_STOREPTR((void *)(& retval->sw), (void *)((struct quad_struct */* */)__cil_tmp20), (void *)(& ___first_local)); #line 81 retval->sw = (struct quad_struct */* */)__cil_tmp20; #line 84 __cil_tmp21 = MakeTree(size, center_x + size, center_y - size, mid2, (mid2 + hi_proc) / 2, (struct quad_struct */* */)retval, (ChildType )3, level - 1); #line 84 CHECK_STOREPTR((void *)(& retval->se), (void *)((struct quad_struct */* */)__cil_tmp21), (void *)(& ___first_local)); #line 84 retval->se = (struct quad_struct */* */)__cil_tmp21; #line 87 __cil_tmp22 = MakeTree(size, center_x + size, center_y + size, ((lo_proc + mid1) + 1) / 2, mid1, (struct quad_struct */* */)retval, (ChildType )1, level - 1); #line 87 CHECK_STOREPTR((void *)(& retval->ne), (void *)((struct quad_struct */* */)__cil_tmp22), (void *)(& ___first_local)); #line 87 retval->ne = (struct quad_struct */* */)__cil_tmp22; #line 90 __cil_tmp23 = MakeTree(size, center_x - size, center_y + size, lo_proc, (lo_proc + mid1) / 2, (struct quad_struct */* */)retval, (ChildType )0, level - 1); #line 90 CHECK_STOREPTR((void *)(& retval->nw), (void *)((struct quad_struct */* */)__cil_tmp23), (void *)(& ___first_local)); #line 90 retval->nw = (struct quad_struct */* */)__cil_tmp23; #line 113 retval->color = (Color )2; } } } #line 116 CHECK_RETURNPTR((void *)((struct quad_struct */* */)retval), (void *)(& ___first_local)); #line 116 return ((struct quad_struct */* */)retval); } #line 28 CHECK_RETURNPTR((void *)__retres, (void *)(& ___first_local)); #line 28 return (__retres); } } #line 35 "perimeter.h" int __NumNodes ; #line 44 "perimeter.h" double wallclock ; #line 13 "main.c" static int adj(Direction d , ChildType ct ) ; #line 13 "main.c" static int adj(Direction d , ChildType ct ) { int tmp ; int tmp___0 ; int tmp___1 ; int tmp___2 ; int __retres ; { #line 16 switch ((int )d) { case 0: ; #line 19 if ((int )ct == 1) { #line 19 tmp = 1; } else { #line 19 if ((int )ct == 0) { #line 19 tmp = 1; } else { #line 19 tmp = 0; } } #line 19 __retres = tmp; goto return_label; case 2: ; #line 21 if ((int )ct == 3) { #line 21 tmp___0 = 1; } else { #line 21 if ((int )ct == 2) { #line 21 tmp___0 = 1; } else { #line 21 tmp___0 = 0; } } #line 21 __retres = tmp___0; goto return_label; case 1: ; #line 23 if ((int )ct == 1) { #line 23 tmp___1 = 1; } else { #line 23 if ((int )ct == 3) { #line 23 tmp___1 = 1; } else { #line 23 tmp___1 = 0; } } #line 23 __retres = tmp___1; goto return_label; case 3: ; #line 25 if ((int )ct == 2) { #line 25 tmp___2 = 1; } else { #line 25 if ((int )ct == 0) { #line 25 tmp___2 = 1; } else { #line 25 tmp___2 = 0; } } #line 25 __retres = tmp___2; goto return_label; } #line 27 __retres = 0; return_label: /* CIL Label */ ; #line 13 return (__retres); } } #line 29 static ChildType reflect(Direction d , ChildType ct ) ; #line 29 "main.c" static ChildType reflect(Direction d , ChildType ct ) { ChildType __retres ; { #line 32 if ((int )d == 3) { goto _L; } else { #line 32 if ((int )d == 1) { _L: /* CIL Label */ ; #line 34 switch ((int )ct) { case 0: #line 37 __retres = (ChildType )1; goto return_label; case 1: #line 39 __retres = (ChildType )0; goto return_label; case 3: #line 41 __retres = (ChildType )2; goto return_label; case 2: #line 43 __retres = (ChildType )3; goto return_label; } } } #line 46 switch ((int )ct) { case 0: #line 49 __retres = (ChildType )2; goto return_label; case 1: #line 51 __retres = (ChildType )3; goto return_label; case 3: #line 53 __retres = (ChildType )1; goto return_label; case 2: #line 55 __retres = (ChildType )0; goto return_label; } #line 57 __retres = (ChildType )0; return_label: /* CIL Label */ ; #line 29 return (__retres); } } #line 59 int CountTree(struct quad_struct * tree ) ; #line 59 "main.c" int CountTree(struct quad_struct * tree ) { struct quad_struct * nw ; struct quad_struct * ne ; struct quad_struct * sw ; struct quad_struct * se ; int tmp ; int tmp___0 ; int tmp___1 ; int tmp___2 ; int __a_local ; int __retres ; int __cil_tmp12 ; int __cil_tmp13 ; int __cil_tmp14 ; int __cil_tmp15 ; int __cil_tmp16 ; int __cil_tmp17 ; int __cil_tmp18 ; int __cil_tmp19 ; int __cil_tmp20 ; int __cil_tmp21 ; int __cil_tmp22 ; int __cil_tmp23 ; int __cil_tmp24 ; int __cil_tmp25 ; int __cil_tmp26 ; int __cil_tmp27 ; { #line 59 se = (struct quad_struct */* */)0; #line 59 sw = (struct quad_struct */* */)0; #line 59 ne = (struct quad_struct */* */)0; #line 59 nw = (struct quad_struct */* */)0; #line 59 if ((unsigned int )(& __a_local) <= ___stack_threshhold) { #line 59 ___stack_overflow(); } { #line 64 CHECK_NULL((void *)tree); #line 64 nw = (struct quad_struct */* */)tree->nw; #line 64 ne = (struct quad_struct */* */)tree->ne; #line 64 sw = (struct quad_struct */* */)tree->sw; #line 64 se = (struct quad_struct */* */)tree->se; #line 65 if ((unsigned int )nw == 0) { #line 65 if ((unsigned int )ne == 0) { #line 65 if ((unsigned int )sw == 0) { #line 65 if ((unsigned int )se == 0) { #line 66 return (1); } else { #line 68 __cil_tmp24 = CountTree((struct quad_struct */* */)nw); #line 68 tmp = __cil_tmp24; #line 68 __cil_tmp25 = CountTree((struct quad_struct */* */)ne); #line 68 tmp___0 = __cil_tmp25; #line 68 __cil_tmp26 = CountTree((struct quad_struct */* */)sw); #line 68 tmp___1 = __cil_tmp26; #line 68 __cil_tmp27 = CountTree((struct quad_struct */* */)se); #line 68 tmp___2 = __cil_tmp27; #line 68 return (((tmp + tmp___0) + tmp___1) + tmp___2); } } else { #line 68 __cil_tmp20 = CountTree((struct quad_struct */* */)nw); #line 68 tmp = __cil_tmp20; #line 68 __cil_tmp21 = CountTree((struct quad_struct */* */)ne); #line 68 tmp___0 = __cil_tmp21; #line 68 __cil_tmp22 = CountTree((struct quad_struct */* */)sw); #line 68 tmp___1 = __cil_tmp22; #line 68 __cil_tmp23 = CountTree((struct quad_struct */* */)se); #line 68 tmp___2 = __cil_tmp23; #line 68 return (((tmp + tmp___0) + tmp___1) + tmp___2); } } else { #line 68 __cil_tmp16 = CountTree((struct quad_struct */* */)nw); #line 68 tmp = __cil_tmp16; #line 68 __cil_tmp17 = CountTree((struct quad_struct */* */)ne); #line 68 tmp___0 = __cil_tmp17; #line 68 __cil_tmp18 = CountTree((struct quad_struct */* */)sw); #line 68 tmp___1 = __cil_tmp18; #line 68 __cil_tmp19 = CountTree((struct quad_struct */* */)se); #line 68 tmp___2 = __cil_tmp19; #line 68 return (((tmp + tmp___0) + tmp___1) + tmp___2); } } else { #line 68 __cil_tmp12 = CountTree((struct quad_struct */* */)nw); #line 68 tmp = __cil_tmp12; #line 68 __cil_tmp13 = CountTree((struct quad_struct */* */)ne); #line 68 tmp___0 = __cil_tmp13; #line 68 __cil_tmp14 = CountTree((struct quad_struct */* */)sw); #line 68 tmp___1 = __cil_tmp14; #line 68 __cil_tmp15 = CountTree((struct quad_struct */* */)se); #line 68 tmp___2 = __cil_tmp15; #line 68 return (((tmp + tmp___0) + tmp___1) + tmp___2); } } #line 59 return (__retres); } } #line 72 static struct quad_struct * child(struct quad_struct * tree , ChildType ct ) ; #line 72 "main.c" static struct quad_struct * child(struct quad_struct * tree , ChildType ct ) { int volatile ___first_local ; struct quad_struct * __retres ; { #line 86 __retres = (struct quad_struct */* */)0; #line 75 switch ((int )ct) { case 1: #line 78 CHECK_NULL((void *)tree); #line 78 __retres = (struct quad_struct */* */)tree->ne; goto return_label; case 0: #line 80 CHECK_NULL((void *)tree); #line 80 __retres = (struct quad_struct */* */)tree->nw; goto return_label; case 3: #line 82 CHECK_NULL((void *)tree); #line 82 __retres = (struct quad_struct */* */)tree->se; goto return_label; case 2: #line 84 CHECK_NULL((void *)tree); #line 84 __retres = (struct quad_struct */* */)tree->sw; goto return_label; } #line 86 __retres = (struct quad_struct */* */)0; return_label: /* CIL Label */ #line 72 CHECK_RETURNPTR((void *)__retres, (void *)(& ___first_local)); #line 72 return (__retres); } } #line 88 static struct quad_struct * gtequal_adj_neighbor(struct quad_struct * tree , Direction d ) ; #line 88 "main.c" static struct quad_struct * gtequal_adj_neighbor(struct quad_struct * tree , Direction d ) { int volatile ___first_local ; struct quad_struct * q ; struct quad_struct * parent ; ChildType ct ; int tmp ; ChildType tmp___0 ; struct quad_struct * tmp___1 ; int __a_local ; struct quad_struct * __retres ; int __cil_tmp11 ; struct quad_struct * __cil_tmp12 ; ChildType __cil_tmp14 ; struct quad_struct * __cil_tmp15 ; { #line 88 __retres = (struct quad_struct */* */)0; #line 88 tmp___1 = (struct quad_struct */* */)0; #line 88 parent = (struct quad_struct */* */)0; #line 88 q = (struct quad_struct */* */)0; #line 88 if ((unsigned int )(& __a_local) <= ___stack_threshhold) { #line 88 ___stack_overflow(); } { #line 94 CHECK_NULL((void *)tree); #line 94 parent = (struct quad_struct */* */)tree->parent; #line 95 ct = tree->childtype; #line 96 if ((unsigned int )parent != 0) { #line 96 __cil_tmp11 = adj(d, ct); #line 96 tmp = __cil_tmp11; #line 96 if (tmp) { #line 97 __cil_tmp12 = gtequal_adj_neighbor((struct quad_struct */* */)parent, d); #line 97 q = (struct quad_struct */* */)__cil_tmp12; } else { #line 98 q = (struct quad_struct */* */)parent; } } else { #line 98 q = (struct quad_struct */* */)parent; } #line 99 if ((int )q) { #line 99 CHECK_NULL((void *)q); #line 99 if ((int )q->color == 2) { #line 100 __cil_tmp14 = reflect(d, ct); #line 100 tmp___0 = __cil_tmp14; #line 100 __cil_tmp15 = child((struct quad_struct */* */)q, tmp___0); #line 100 tmp___1 = (struct quad_struct */* */)__cil_tmp15; #line 100 CHECK_RETURNPTR((void *)((struct quad_struct */* */)tmp___1), (void *)(& ___first_local)); #line 100 return ((struct quad_struct */* */)tmp___1); } else { #line 102 CHECK_RETURNPTR((void *)((struct quad_struct */* */)q), (void *)(& ___first_local)); #line 102 return ((struct quad_struct */* */)q); } } else { #line 102 CHECK_RETURNPTR((void *)((struct quad_struct */* */)q), (void *)(& ___first_local)); #line 102 return ((struct quad_struct */* */)q); } } #line 88 CHECK_RETURNPTR((void *)__retres, (void *)(& ___first_local)); #line 88 return (__retres); } } #line 105 static int sum_adjacent(struct quad_struct * p , ChildType q1 , ChildType q2 , int size ) ; #line 105 "main.c" static int sum_adjacent(struct quad_struct * p , ChildType q1 , ChildType q2 , int size ) { struct quad_struct * tmp ; int tmp___0 ; struct quad_struct * tmp___1 ; int tmp___2 ; int __a_local ; int __retres ; struct quad_struct * __cil_tmp11 ; int __cil_tmp12 ; struct quad_struct * __cil_tmp13 ; int __cil_tmp14 ; { #line 105 tmp___1 = (struct quad_struct */* */)0; #line 105 tmp = (struct quad_struct */* */)0; #line 105 if ((unsigned int )(& __a_local) <= ___stack_threshhold) { #line 105 ___stack_overflow(); } { #line 108 CHECK_NULL((void *)p); #line 108 if ((int )p->color == 2) { #line 110 __cil_tmp11 = child((struct quad_struct */* */)p, q1); #line 110 tmp = (struct quad_struct */* */)__cil_tmp11; #line 110 __cil_tmp12 = sum_adjacent((struct quad_struct */* */)tmp, q1, q2, size / 2); #line 110 tmp___0 = __cil_tmp12; #line 110 __cil_tmp13 = child((struct quad_struct */* */)p, q2); #line 110 tmp___1 = (struct quad_struct */* */)__cil_tmp13; #line 110 __cil_tmp14 = sum_adjacent((struct quad_struct */* */)tmp___1, q1, q2, size / 2); #line 110 tmp___2 = __cil_tmp14; #line 110 return (tmp___0 + tmp___2); } else { #line 113 if ((int )p->color == 1) { #line 115 return (size); } else { #line 117 return (0); } } } #line 105 return (__retres); } } #line 120 int perimeter(struct quad_struct * tree , int size ) ; #line 120 "main.c" int perimeter(struct quad_struct * tree , int size ) { int retval ; struct quad_struct * neighbor ; struct quad_struct * child___0 ; int tmp ; int tmp___0 ; int tmp___1 ; int tmp___2 ; int tmp___3 ; int tmp___4 ; int tmp___5 ; int tmp___6 ; int __a_local ; int __retres ; struct quad_struct * __cil_tmp16 ; int __cil_tmp17 ; struct quad_struct * __cil_tmp18 ; int __cil_tmp19 ; struct quad_struct * __cil_tmp20 ; int __cil_tmp21 ; struct quad_struct * __cil_tmp22 ; int __cil_tmp23 ; int __cil_tmp24 ; int __cil_tmp25 ; int __cil_tmp26 ; int __cil_tmp27 ; { #line 120 child___0 = (struct quad_struct */* */)0; #line 120 neighbor = (struct quad_struct */* */)0; #line 120 if ((unsigned int )(& __a_local) <= ___stack_threshhold) { #line 120 ___stack_overflow(); } { #line 122 retval = 0; #line 126 CHECK_NULL((void *)tree); #line 126 if ((int )tree->color == 2) { #line 134 child___0 = (struct quad_struct */* */)tree->sw; #line 135 __cil_tmp24 = perimeter((struct quad_struct */* */)child___0, size / 2); #line 135 tmp = __cil_tmp24; #line 135 retval = retval + tmp; #line 136 child___0 = (struct quad_struct */* */)tree->se; #line 137 __cil_tmp25 = perimeter((struct quad_struct */* */)child___0, size / 2); #line 137 tmp___0 = __cil_tmp25; #line 137 retval = retval + tmp___0; #line 138 child___0 = (struct quad_struct */* */)tree->ne; #line 139 __cil_tmp26 = perimeter((struct quad_struct */* */)child___0, size / 2); #line 139 tmp___1 = __cil_tmp26; #line 139 retval = retval + tmp___1; #line 140 child___0 = (struct quad_struct */* */)tree->nw; #line 141 __cil_tmp27 = perimeter((struct quad_struct */* */)child___0, size / 2); #line 141 tmp___2 = __cil_tmp27; #line 141 retval = retval + tmp___2; } else { #line 157 if ((int )tree->color == 0) { #line 160 __cil_tmp16 = gtequal_adj_neighbor((struct quad_struct */* */)tree, (Direction )0); #line 160 neighbor = (struct quad_struct */* */)__cil_tmp16; #line 161 if ((unsigned int )neighbor == 0) { #line 161 retval = retval + size; } else { #line 161 CHECK_NULL((void *)neighbor); #line 161 if ((int )neighbor->color == 1) { #line 161 retval = retval + size; } else { #line 162 if ((int )neighbor->color == 2) { #line 163 __cil_tmp17 = sum_adjacent((struct quad_struct */* */)neighbor, (ChildType )3, (ChildType )2, size); #line 163 tmp___3 = __cil_tmp17; #line 163 retval = retval + tmp___3; } } } #line 165 __cil_tmp18 = gtequal_adj_neighbor((struct quad_struct */* */)tree, (Direction )1); #line 165 neighbor = (struct quad_struct */* */)__cil_tmp18; #line 166 if ((unsigned int )neighbor == 0) { #line 166 retval = retval + size; } else { #line 166 CHECK_NULL((void *)neighbor); #line 166 if ((int )neighbor->color == 1) { #line 166 retval = retval + size; } else { #line 167 if ((int )neighbor->color == 2) { #line 168 __cil_tmp19 = sum_adjacent((struct quad_struct */* */)neighbor, (ChildType )2, (ChildType )0, size); #line 168 tmp___4 = __cil_tmp19; #line 168 retval = retval + tmp___4; } } } #line 170 __cil_tmp20 = gtequal_adj_neighbor((struct quad_struct */* */)tree, (Direction )2); #line 170 neighbor = (struct quad_struct */* */)__cil_tmp20; #line 171 if ((unsigned int )neighbor == 0) { #line 171 retval = retval + size; } else { #line 171 CHECK_NULL((void *)neighbor); #line 171 if ((int )neighbor->color == 1) { #line 171 retval = retval + size; } else { #line 172 if ((int )neighbor->color == 2) { #line 173 __cil_tmp21 = sum_adjacent((struct quad_struct */* */)neighbor, (ChildType )0, (ChildType )1, size); #line 173 tmp___5 = __cil_tmp21; #line 173 retval = retval + tmp___5; } } } #line 175 __cil_tmp22 = gtequal_adj_neighbor((struct quad_struct */* */)tree, (Direction )3); #line 175 neighbor = (struct quad_struct */* */)__cil_tmp22; #line 176 if ((unsigned int )neighbor == 0) { #line 176 retval = retval + size; } else { #line 176 CHECK_NULL((void *)neighbor); #line 176 if ((int )neighbor->color == 1) { #line 176 retval = retval + size; } else { #line 177 if ((int )neighbor->color == 2) { #line 178 __cil_tmp23 = sum_adjacent((struct quad_struct */* */)neighbor, (ChildType )1, (ChildType )3, size); #line 178 tmp___6 = __cil_tmp23; #line 178 retval = retval + tmp___6; } } } } } #line 180 return (retval); } #line 120 return (__retres); } } #line 199 extern int __ccured_va_count ; #line 199 "main.c" static char __string1[43] = #line 199 { 'P', 'e', 'r', 'i', 'm', 'e', 't', 'e', 'r', ' ', 'w', 'i', 't', 'h', ' ', '%', 'd', ' ', 'l', 'e', 'v', 'e', 'l', 's', ' ', 'o', 'n', ' ', '%', 'd', ' ', 'p', 'r', 'o', 'c', 'e', 's', 's', 'o', 'r', 's', '\n', '\000'}; #line 205 "main.c" static char __string2[19] = #line 205 { '#', ' ', 'o', 'f', ' ', 'l', 'e', 'a', 'v', 'e', 's', ' ', 'i', 's', ' ', '%', 'd', '\n', '\000'}; #line 214 "main.c" static char __string3[17] = #line 214 { 'p', 'e', 'r', 'i', 'm', 'e', 't', 'e', 'r', ' ', 'i', 's', ' ', '%', 'd', '\n', '\000'}; #line 215 "main.c" static char __string4[32] = #line 215 { 'T', 'i', 'm', 'e', ' ', 'e', 'l', 'a', 'p', 's', 'e', 'd', ' ', '=', ' ', '%', 'f', ' ', 'm', 'i', 'l', 'l', 'i', 's', 'e', 'c', 'o', 'n', 'd', 's', '\n', '\000'}; #line 188 int main(void) ; #line 188 "main.c" int main(void) { struct quad_struct * tree ; int count ; int level ; int i ; clock_t tmp___0 ; int __retres ; unsigned int __cil_tmp9 ; struct quad_struct * __cil_tmp10 ; int __cil_tmp11 ; clock_t __cil_tmp12 ; int __cil_tmp13 ; clock_t __cil_tmp14 ; { #line 188 tree = (struct quad_struct */* */)0; #line 188 __ccuredAlwaysStopOnError = 1; #line 188 __ccuredUseStrings = 0; #line 188 __ccuredLogNonPointers = 0; #line 188 __ccuredInit(); #line 188 __cil_tmp9 = ___compute_stack_threshhold(); #line 188 ___stack_threshhold = __cil_tmp9; { #line 196 level = 12; #line 197 __NumNodes = 1; #line 199 __ccured_va_count = -1; #line 199 printf((char */* */)(& __string1[0]), level, __NumNodes); #line 200 __cil_tmp10 = MakeTree(2048, 0, 0, 0, __NumNodes - 1, (struct quad_struct */* */)0, (ChildType )3, level); #line 200 tree = (struct quad_struct */* */)__cil_tmp10; #line 204 __cil_tmp11 = CountTree((struct quad_struct */* */)tree); #line 204 count = __cil_tmp11; #line 205 __ccured_va_count = -1; #line 205 printf((char */* */)(& __string2[0]), count); #line 208 __cil_tmp12 = clock(); #line 208 wallclock = (double )__cil_tmp12; #line 209 i = 0; #line 209 while (i < 100) { #line 210 __cil_tmp13 = perimeter((struct quad_struct */* */)tree, 4096); #line 210 count = __cil_tmp13; #line 209 i = i + 1; } #line 212 __cil_tmp14 = clock(); #line 212 tmp___0 = __cil_tmp14; #line 212 wallclock = (1000000.0 * ((double )tmp___0 - wallclock)) / (double )1000; #line 214 __ccured_va_count = -1; #line 214 printf((char */* */)(& __string3[0]), count); #line 215 __ccured_va_count = -1; #line 215 printf((char */* */)(& __string4[0]), wallclock / 1000.0); #line 219 exit(0); } #line 188 return (__retres); } }