/* 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 15 "power.h" struct demand { double P ; double Q ; }; #line 15 "power.h" typedef struct demand Demand; #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 60 "power.h" struct lateral; #line 60 "power.h" struct root { Demand D ; double theta_R ; double theta_I ; Demand last ; double last_theta_R ; double last_theta_I ; struct lateral * ( __FSEQ feeders)[10] ; }; #line 70 struct branch; #line 70 "power.h" struct lateral { Demand D ; double alpha ; double beta ; double R ; double X ; struct lateral * next_lateral ; struct branch * branch ; }; #line 80 struct leaf; #line 80 "power.h" struct branch { Demand D ; double alpha ; double beta ; double R ; double X ; struct branch * next_branch ; struct leaf * ( __FSEQ leaves)[10] ; }; #line 90 "power.h" struct leaf { Demand D ; double pi_R ; double pi_I ; }; #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 46 "d:/home/db/postdoc/Blast/ccured/include/gcc_3.3.1/time.h" extern clock_t ( __attribute__((__cdecl__)) clock)(void) ; #line 36 "power.h" double wallclock ; #line 43 "/usr/include/math.h" extern double fabs(double ) ; #line 61 extern double sqrt(double ) ; #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 104 "power.h" struct root * build_tree(void) ; #line 105 struct lateral * build_lateral(int i , int num ) ; #line 106 struct branch * build_branch(int i , int j , int num ) ; #line 107 struct leaf * build_leaf(void) ; #line 109 void Compute_Tree(struct root * r ) ; #line 110 Demand Compute_Lateral(struct lateral * l , double theta_R , double theta_I , double pi_R , double pi_I ) ; #line 112 Demand Compute_Branch(struct branch * br , double theta_R , double theta_I , double pi_R , double pi_I ) ; #line 114 Demand Compute_Leaf(struct leaf * l , double pi_R , double pi_I ) ; #line 20 "compute.c" static double P = 1.0; #line 21 "compute.c" static double Q = 1.0; #line 27 void optimize_node(double pi_R , double pi_I ) ; #line 28 double find_g(void) ; #line 29 double find_h(void) ; #line 30 "compute.c" struct meta_fseqp_double { void *_e ; } ; #line 30 double find_gradient_f_f(double pi_R , double pi_I , double * __FSEQ gradient , void *gradient_e ) ; #line 31 double find_gradient_g_f(double * __FSEQ gradient , void *gradient_e ) ; #line 32 double find_gradient_h_f(double * __FSEQ gradient , void *gradient_e ) ; #line 33 void find_dd_grad_f_f(double pi_R , double pi_I , double * __FSEQ dd_grad , void *dd_grad_e ) ; #line 34 double make_orthogonal_ff(double * __FSEQ v_mod , void *v_mod_e , double * __FSEQ v_static , void *v_static_e ) ; #line 37 void Compute_Tree(struct root * r ) ; #line 37 "compute.c" void Compute_Tree(struct root * r ) { register int i ; struct lateral * l ; Demand a ; Demand tmp ; double theta_R ; double theta_I ; Demand __cil_tmp8 ; { #line 75 l = (struct lateral */* */)0; #line 48 tmp.P = 0.0; #line 49 tmp.Q = 0.0; #line 51 i = 0; #line 51 while (i < 10) { #line 52 CHECK_NULL((void *)r); #line 52 CHECK_GEU(9U, (unsigned int )i); #line 52 l = (struct lateral */* */)r->feeders[i]; #line 53 CHECK_NULL((void *)r); #line 53 theta_R = r->theta_R; #line 54 CHECK_NULL((void *)r); #line 54 theta_I = r->theta_I; #line 55 __cil_tmp8 = Compute_Lateral((struct lateral */* */)l, theta_R, theta_I, theta_R, theta_I); #line 55 a = __cil_tmp8; #line 56 tmp.P = tmp.P + a.P; #line 57 tmp.Q = tmp.Q + a.Q; #line 51 i = i + 1; } #line 73 CHECK_NULL((void *)r); #line 73 r->D.P = tmp.P; #line 74 CHECK_NULL((void *)r); #line 74 r->D.Q = tmp.Q; #line 37 return; } } #line 77 Demand Compute_Lateral(struct lateral * l , double theta_R , double theta_I , double pi_R , double pi_I ) ; #line 77 "compute.c" Demand Compute_Lateral(struct lateral * l , double theta_R , double theta_I , double pi_R , double pi_I ) { Demand a1 ; Demand a2 ; double new_pi_R ; double new_pi_I ; double a ; double b ; double c ; double root ; struct lateral * next ; struct branch * br ; double tmp ; int __a_local ; Demand __retres ; Demand __cil_tmp19 ; Demand __cil_tmp20 ; double __cil_tmp21 ; { #line 77 br = (struct branch */* */)0; #line 77 next = (struct lateral */* */)0; #line 77 if ((unsigned int )(& __a_local) <= ___stack_threshhold) { #line 77 ___stack_overflow(); } { #line 90 CHECK_NULL((void *)l); #line 90 CHECK_NULL((void *)l); #line 90 CHECK_NULL((void *)l); #line 90 new_pi_R = pi_R + l->alpha * (theta_R + (theta_I * l->X) / l->R); #line 91 CHECK_NULL((void *)l); #line 91 CHECK_NULL((void *)l); #line 91 CHECK_NULL((void *)l); #line 91 new_pi_I = pi_I + l->beta * (theta_I + (theta_R * l->R) / l->X); #line 93 CHECK_NULL((void *)l); #line 93 next = (struct lateral */* */)l->next_lateral; #line 94 if ((unsigned int )next != 0) { #line 96 __cil_tmp19 = Compute_Lateral((struct lateral */* */)next, theta_R, theta_I, new_pi_R, new_pi_I); #line 96 a1 = __cil_tmp19; } #line 101 CHECK_NULL((void *)l); #line 101 br = (struct branch */* */)l->branch; #line 102 __cil_tmp20 = Compute_Branch((struct branch */* */)br, theta_R, theta_I, new_pi_R, new_pi_I); #line 102 a2 = __cil_tmp20; #line 104 if ((unsigned int )next != 0) { #line 106 CHECK_NULL((void *)l); #line 106 l->D.P = a1.P + a2.P; #line 107 CHECK_NULL((void *)l); #line 107 l->D.Q = a1.Q + a2.Q; } else { #line 114 CHECK_NULL((void *)l); #line 114 l->D.P = a2.P; #line 115 CHECK_NULL((void *)l); #line 115 l->D.Q = a2.Q; } #line 119 CHECK_NULL((void *)l); #line 119 CHECK_NULL((void *)l); #line 119 CHECK_NULL((void *)l); #line 119 CHECK_NULL((void *)l); #line 119 a = l->R * l->R + l->X * l->X; #line 120 CHECK_NULL((void *)l); #line 120 CHECK_NULL((void *)l); #line 120 CHECK_NULL((void *)l); #line 120 CHECK_NULL((void *)l); #line 120 CHECK_NULL((void *)l); #line 120 CHECK_NULL((void *)l); #line 120 CHECK_NULL((void *)l); #line 120 b = ((((double )2 * l->R) * l->X) * l->D.Q - (((double )2 * l->X) * l->X) * l->D.P) - l->R; #line 121 CHECK_NULL((void *)l); #line 121 CHECK_NULL((void *)l); #line 121 CHECK_NULL((void *)l); #line 121 CHECK_NULL((void *)l); #line 121 c = l->R * l->D.Q - l->X * l->D.P; #line 122 CHECK_NULL((void *)l); #line 122 CHECK_NULL((void *)l); #line 122 c = c * c + l->R * l->D.P; #line 123 __cil_tmp21 = sqrt(b * b - ((double )4 * a) * c); #line 123 tmp = __cil_tmp21; #line 123 root = (- b - tmp) / ((double )2 * a); #line 124 CHECK_NULL((void *)l); #line 124 CHECK_NULL((void *)l); #line 124 CHECK_NULL((void *)l); #line 124 CHECK_NULL((void *)l); #line 124 CHECK_NULL((void *)l); #line 124 l->D.Q = l->D.Q + ((root - l->D.P) * l->X) / l->R; #line 125 CHECK_NULL((void *)l); #line 125 l->D.P = root; #line 128 CHECK_NULL((void *)l); #line 128 CHECK_NULL((void *)l); #line 128 a = ((double )2 * l->R) * l->D.P; #line 129 CHECK_NULL((void *)l); #line 129 CHECK_NULL((void *)l); #line 129 b = ((double )2 * l->X) * l->D.Q; #line 130 CHECK_NULL((void *)l); #line 130 l->alpha = a / (((double )1 - a) - b); #line 131 CHECK_NULL((void *)l); #line 131 l->beta = b / (((double )1 - a) - b); #line 132 CHECK_NULL((void *)l); #line 132 return (l->D); } #line 77 return (__retres); } } #line 135 Demand Compute_Branch(struct branch * br , double theta_R , double theta_I , double pi_R , double pi_I ) ; #line 135 "compute.c" Demand Compute_Branch(struct branch * br , double theta_R , double theta_I , double pi_R , double pi_I ) { Demand a2 ; Demand tmp ; double new_pi_R ; double new_pi_I ; double a ; double b ; double c ; double root ; struct leaf * l ; struct branch * next ; int i ; Demand a1 ; double tmp___0 ; int __a_local ; Demand __retres ; Demand __cil_tmp21 ; Demand __cil_tmp22 ; double __cil_tmp23 ; { #line 135 next = (struct branch */* */)0; #line 135 l = (struct leaf */* */)0; #line 135 if ((unsigned int )(& __a_local) <= ___stack_threshhold) { #line 135 ___stack_overflow(); } { #line 149 CHECK_NULL((void *)br); #line 149 CHECK_NULL((void *)br); #line 149 CHECK_NULL((void *)br); #line 149 new_pi_R = pi_R + br->alpha * (theta_R + (theta_I * br->X) / br->R); #line 150 CHECK_NULL((void *)br); #line 150 CHECK_NULL((void *)br); #line 150 CHECK_NULL((void *)br); #line 150 new_pi_I = pi_I + br->beta * (theta_I + (theta_R * br->R) / br->X); #line 152 CHECK_NULL((void *)br); #line 152 next = (struct branch */* */)br->next_branch; #line 153 if ((unsigned int )next != 0) { #line 155 __cil_tmp21 = Compute_Branch((struct branch */* */)next, theta_R, theta_I, new_pi_R, new_pi_I); #line 155 a1 = __cil_tmp21; } #line 162 tmp.P = 0.0; #line 162 tmp.Q = 0.0; #line 164 i = 0; #line 164 while (i < 10) { #line 165 CHECK_NULL((void *)br); #line 165 CHECK_GEU(9U, (unsigned int )i); #line 165 l = (struct leaf */* */)br->leaves[i]; #line 166 __cil_tmp22 = Compute_Leaf((struct leaf */* */)l, new_pi_R, new_pi_I); #line 166 a2 = __cil_tmp22; #line 167 tmp.P = tmp.P + a2.P; #line 168 tmp.Q = tmp.Q + a2.Q; #line 164 i = i + 1; } #line 170 if ((unsigned int )next != 0) { #line 172 CHECK_NULL((void *)br); #line 172 br->D.P = a1.P + tmp.P; #line 173 CHECK_NULL((void *)br); #line 173 br->D.Q = a1.Q + tmp.Q; } else { #line 180 CHECK_NULL((void *)br); #line 180 br->D.P = tmp.P; #line 181 CHECK_NULL((void *)br); #line 181 br->D.Q = tmp.Q; } #line 185 CHECK_NULL((void *)br); #line 185 CHECK_NULL((void *)br); #line 185 CHECK_NULL((void *)br); #line 185 CHECK_NULL((void *)br); #line 185 a = br->R * br->R + br->X * br->X; #line 186 CHECK_NULL((void *)br); #line 186 CHECK_NULL((void *)br); #line 186 CHECK_NULL((void *)br); #line 186 CHECK_NULL((void *)br); #line 186 CHECK_NULL((void *)br); #line 186 CHECK_NULL((void *)br); #line 186 CHECK_NULL((void *)br); #line 186 b = ((((double )2 * br->R) * br->X) * br->D.Q - (((double )2 * br->X) * br->X) * br->D.P) - br->R; #line 187 CHECK_NULL((void *)br); #line 187 CHECK_NULL((void *)br); #line 187 CHECK_NULL((void *)br); #line 187 CHECK_NULL((void *)br); #line 187 c = br->R * br->D.Q - br->X * br->D.P; #line 188 CHECK_NULL((void *)br); #line 188 CHECK_NULL((void *)br); #line 188 c = c * c + br->R * br->D.P; #line 189 __cil_tmp23 = sqrt(b * b - ((double )4 * a) * c); #line 189 tmp___0 = __cil_tmp23; #line 189 root = (- b - tmp___0) / ((double )2 * a); #line 190 CHECK_NULL((void *)br); #line 190 CHECK_NULL((void *)br); #line 190 CHECK_NULL((void *)br); #line 190 CHECK_NULL((void *)br); #line 190 CHECK_NULL((void *)br); #line 190 br->D.Q = br->D.Q + ((root - br->D.P) * br->X) / br->R; #line 191 CHECK_NULL((void *)br); #line 191 br->D.P = root; #line 193 CHECK_NULL((void *)br); #line 193 CHECK_NULL((void *)br); #line 193 a = ((double )2 * br->R) * br->D.P; #line 194 CHECK_NULL((void *)br); #line 194 CHECK_NULL((void *)br); #line 194 b = ((double )2 * br->X) * br->D.Q; #line 195 CHECK_NULL((void *)br); #line 195 br->alpha = a / (((double )1 - a) - b); #line 196 CHECK_NULL((void *)br); #line 196 br->beta = b / (((double )1 - a) - b); #line 198 CHECK_NULL((void *)br); #line 198 return (br->D); } #line 135 return (__retres); } } #line 201 Demand Compute_Leaf(struct leaf * l , double pi_R , double pi_I ) ; #line 201 "compute.c" Demand Compute_Leaf(struct leaf * l , double pi_R , double pi_I ) { Demand __retres ; { #line 202 CHECK_NULL((void *)l); #line 202 P = l->D.P; #line 203 CHECK_NULL((void *)l); #line 203 Q = l->D.Q; #line 205 optimize_node(pi_R, pi_I); #line 207 if (P < 0.0) { #line 208 P = 0.0; #line 209 Q = 0.0; } #line 211 CHECK_NULL((void *)l); #line 211 l->D.P = P; #line 212 CHECK_NULL((void *)l); #line 212 l->D.Q = Q; #line 213 CHECK_NULL((void *)l); #line 213 __retres = l->D; #line 201 return (__retres); } } #line 218 void optimize_node(double pi_R , double pi_I ) ; #line 218 "compute.c" void optimize_node(double pi_R , double pi_I ) { double g ; double h ; double ( __FSEQ grad_f)[2] ; double ( __FSEQ grad_g)[2] ; double ( __FSEQ grad_h)[2] ; double ( __FSEQ dd_grad_f)[2] ; double magnitude ; int i ; double total ; double max_dist ; double tmp ; double tmp___0 ; double tmp___1 ; double tmp___2 ; double tmp___3 ; double tmp___4 ; double tmp___5 ; double tmp___6 ; double __cil_tmp22 ; double __cil_tmp23 ; double * __FSEQ __cil_tmp24 ; double __cil_tmp25 ; double __cil_tmp26 ; double * __FSEQ __cil_tmp27 ; double __cil_tmp28 ; double * __FSEQ __cil_tmp29 ; double * __FSEQ __cil_tmp30 ; double * __FSEQ __cil_tmp31 ; double __cil_tmp32 ; double * __FSEQ __cil_tmp33 ; double __cil_tmp34 ; double * __FSEQ __cil_tmp35 ; double __cil_tmp36 ; double * __FSEQ __cil_tmp37 ; double * __FSEQ __cil_tmp38 ; double * __FSEQ __cil_tmp39 ; double __cil_tmp40 ; double * __FSEQ __cil_tmp41 ; double __cil_tmp42 ; double __cil_tmp43 ; double __cil_tmp44 ; double * __FSEQ __cil_tmp45 ; double * __FSEQ __cil_tmp46 ; double __cil_tmp47 ; double __cil_tmp48 ; double __cil_tmp49 ; void *__cil_tmp24_e63 ; void *__cil_tmp27_e64 ; void *__cil_tmp29_e65 ; void *__cil_tmp30_e66 ; void *__cil_tmp31_e67 ; void *__cil_tmp33_e68 ; void *__cil_tmp35_e69 ; void *__cil_tmp37_e70 ; void *__cil_tmp38_e71 ; void *__cil_tmp39_e72 ; void *__cil_tmp41_e73 ; void *__cil_tmp45_e74 ; void *__cil_tmp46_e75 ; { #line 233 while (1) { #line 235 __cil_tmp22 = find_h(); #line 235 h = __cil_tmp22; #line 236 __cil_tmp23 = fabs(h); #line 236 tmp = __cil_tmp23; #line 236 if (tmp > 0.000001) { #line 237 CHECK_SEQ2FSEQ((void *)(grad_h), (void *)(grad_h + 2), (void *)(grad_h)); #line 237 __cil_tmp24 = (double */* __FSEQ */)(grad_h); #line 237 __cil_tmp24_e63 = grad_h + 2; #line 237 __cil_tmp25 = find_gradient_h_f(__cil_tmp24, __cil_tmp24_e63); #line 237 magnitude = __cil_tmp25; #line 238 total = h / magnitude; #line 239 P = P - total * grad_h[0]; #line 240 Q = Q - total * grad_h[1]; } #line 244 __cil_tmp26 = find_g(); #line 244 g = __cil_tmp26; #line 245 if (g > 0.000001) { #line 246 CHECK_SEQ2FSEQ((void *)(grad_g), (void *)(grad_g + 2), (void *)(grad_g)); #line 246 __cil_tmp27 = (double */* __FSEQ */)(grad_g); #line 246 __cil_tmp27_e64 = grad_g + 2; #line 246 __cil_tmp28 = find_gradient_g_f(__cil_tmp27, __cil_tmp27_e64); #line 246 magnitude = __cil_tmp28; #line 247 CHECK_SEQ2FSEQ((void *)(grad_h), (void *)(grad_h + 2), (void *)(grad_h)); #line 247 __cil_tmp29 = (double */* __FSEQ */)(grad_h); #line 247 __cil_tmp29_e65 = grad_h + 2; #line 247 find_gradient_h_f(__cil_tmp29, __cil_tmp29_e65); #line 248 CHECK_SEQ2FSEQ((void *)(grad_g), (void *)(grad_g + 2), (void *)(grad_g)); #line 248 __cil_tmp30 = (double */* __FSEQ */)(grad_g); #line 248 __cil_tmp30_e66 = grad_g + 2; #line 248 CHECK_SEQ2FSEQ((void *)(grad_h), (void *)(grad_h + 2), (void *)(grad_h)); #line 248 __cil_tmp31 = (double */* __FSEQ */)(grad_h); #line 248 __cil_tmp31_e67 = grad_h + 2; #line 248 __cil_tmp32 = make_orthogonal_ff(__cil_tmp30, __cil_tmp30_e66, __cil_tmp31, __cil_tmp31_e67); #line 248 tmp___0 = __cil_tmp32; #line 248 magnitude = magnitude * tmp___0; #line 249 total = g / magnitude; #line 250 P = P - total * grad_g[0]; #line 251 Q = Q - total * grad_g[1]; } #line 255 CHECK_SEQ2FSEQ((void *)(grad_f), (void *)(grad_f + 2), (void *)(grad_f)); #line 255 __cil_tmp33 = (double */* __FSEQ */)(grad_f); #line 255 __cil_tmp33_e68 = grad_f + 2; #line 255 __cil_tmp34 = find_gradient_f_f(pi_R, pi_I, __cil_tmp33, __cil_tmp33_e68); #line 255 magnitude = __cil_tmp34; #line 256 CHECK_SEQ2FSEQ((void *)(dd_grad_f), (void *)(dd_grad_f + 2), (void *)(dd_grad_f)); #line 256 __cil_tmp35 = (double */* __FSEQ */)(dd_grad_f); #line 256 __cil_tmp35_e69 = dd_grad_f + 2; #line 256 find_dd_grad_f_f(pi_R, pi_I, __cil_tmp35, __cil_tmp35_e69); #line 257 total = 0.0; #line 258 i = 0; #line 258 while (i < 2) { #line 259 CHECK_GEU(1U, (unsigned int )i); #line 259 CHECK_GEU(1U, (unsigned int )i); #line 259 total = total + grad_f[i] * dd_grad_f[i]; #line 258 i = i + 1; } #line 260 __cil_tmp36 = fabs(total); #line 260 tmp___1 = __cil_tmp36; #line 260 magnitude = magnitude / tmp___1; #line 261 CHECK_SEQ2FSEQ((void *)(grad_h), (void *)(grad_h + 2), (void *)(grad_h)); #line 261 __cil_tmp37 = (double */* __FSEQ */)(grad_h); #line 261 __cil_tmp37_e70 = grad_h + 2; #line 261 find_gradient_h_f(__cil_tmp37, __cil_tmp37_e70); #line 262 CHECK_SEQ2FSEQ((void *)(grad_f), (void *)(grad_f + 2), (void *)(grad_f)); #line 262 __cil_tmp38 = (double */* __FSEQ */)(grad_f); #line 262 __cil_tmp38_e71 = grad_f + 2; #line 262 CHECK_SEQ2FSEQ((void *)(grad_h), (void *)(grad_h + 2), (void *)(grad_h)); #line 262 __cil_tmp39 = (double */* __FSEQ */)(grad_h); #line 262 __cil_tmp39_e72 = grad_h + 2; #line 262 __cil_tmp40 = make_orthogonal_ff(__cil_tmp38, __cil_tmp38_e71, __cil_tmp39, __cil_tmp39_e72); #line 262 tmp___2 = __cil_tmp40; #line 262 magnitude = magnitude * tmp___2; #line 263 CHECK_SEQ2FSEQ((void *)(grad_g), (void *)(grad_g + 2), (void *)(grad_g)); #line 263 __cil_tmp41 = (double */* __FSEQ */)(grad_g); #line 263 __cil_tmp41_e73 = grad_g + 2; #line 263 find_gradient_g_f(__cil_tmp41, __cil_tmp41_e73); #line 264 total = 0.0; #line 265 i = 0; #line 265 while (i < 2) { #line 266 CHECK_GEU(1U, (unsigned int )i); #line 266 CHECK_GEU(1U, (unsigned int )i); #line 266 total = total + grad_f[i] * grad_g[i]; #line 265 i = i + 1; } #line 267 if (total > 0) { #line 268 __cil_tmp42 = find_g(); #line 268 tmp___3 = __cil_tmp42; #line 268 max_dist = - (tmp___3 / total); #line 269 if (magnitude > max_dist) { #line 270 magnitude = max_dist; } } #line 272 P = P + magnitude * grad_f[0]; #line 273 Q = Q + magnitude * grad_f[1]; #line 275 __cil_tmp43 = find_h(); #line 275 h = __cil_tmp43; #line 276 __cil_tmp44 = find_g(); #line 276 g = __cil_tmp44; #line 277 CHECK_SEQ2FSEQ((void *)(grad_f), (void *)(grad_f + 2), (void *)(grad_f)); #line 277 __cil_tmp45 = (double */* __FSEQ */)(grad_f); #line 277 __cil_tmp45_e74 = grad_f + 2; #line 277 find_gradient_f_f(pi_R, pi_I, __cil_tmp45, __cil_tmp45_e74); #line 278 CHECK_SEQ2FSEQ((void *)(grad_h), (void *)(grad_h + 2), (void *)(grad_h)); #line 278 __cil_tmp46 = (double */* __FSEQ */)(grad_h); #line 278 __cil_tmp46_e75 = grad_h + 2; #line 278 find_gradient_h_f(__cil_tmp46, __cil_tmp46_e75); #line 233 __cil_tmp47 = fabs(h); #line 233 tmp___4 = __cil_tmp47; #line 233 if (! (tmp___4 > 0.000001)) { #line 233 if (! (g > 0.000001)) { #line 233 __cil_tmp48 = fabs(g); #line 233 tmp___5 = __cil_tmp48; #line 233 if (tmp___5 > 0.000001) { #line 233 __cil_tmp49 = fabs(grad_f[0] * grad_h[1] - grad_f[1] * grad_h[0]); #line 233 tmp___6 = __cil_tmp49; #line 233 if (! (tmp___6 > 0.000001)) { #line 233 break; } } else { #line 233 break; } } } } #line 218 return; } } #line 285 double find_g(void) ; #line 285 "compute.c" double find_g(void) { double __retres ; { #line 287 __retres = (P * P + Q * Q) - 0.8; #line 285 return (__retres); } } #line 290 double find_h(void) ; #line 290 "compute.c" double find_h(void) { double __retres ; { #line 292 __retres = P - (double )5 * Q; #line 290 return (__retres); } } #line 295 double find_gradient_f_f(double pi_R , double pi_I , double * __FSEQ gradient , void *gradient_e ) ; #line 295 "compute.c" double find_gradient_f_f(double pi_R , double pi_I , double * __FSEQ gradient , void *gradient_e ) { int i ; double magnitude ; double __retres ; double __cil_tmp7 ; { #line 298 magnitude = 0.0; #line 300 CHECK_FSEQ2SAFE(gradient_e, (void *)gradient, sizeof(double ), sizeof(double ), 1, 0); #line 300 (*gradient) = (double )1 / ((double )1 + P) - pi_R; #line 301 CHECK_FSEQARITH((void *)gradient, sizeof(double ), (void *)(gradient + 1)); #line 301 CHECK_FSEQ2SAFE(gradient_e, (void *)(gradient + 1), sizeof(double ), sizeof(double ), 1, 0); #line 301 (*(gradient + 1)) = (double )1 / ((double )1 + Q) - pi_I; #line 302 i = 0; #line 302 while (i < 2) { #line 303 CHECK_FSEQARITH2SAFE((void *)gradient, gradient_e, (void *)(gradient + i), sizeof(double ), sizeof(double ), 1, 0); #line 303 CHECK_FSEQARITH2SAFE((void *)gradient, gradient_e, (void *)(gradient + i), sizeof(double ), sizeof(double ), 1, 0); #line 303 magnitude = magnitude + (*(gradient + i)) * (*(gradient + i)); #line 302 i = i + 1; } #line 304 __cil_tmp7 = sqrt(magnitude); #line 304 magnitude = __cil_tmp7; #line 305 i = 0; #line 305 while (i < 2) { #line 306 CHECK_FSEQARITH((void *)gradient, sizeof(double ), (void *)(gradient + i)); #line 306 CHECK_FSEQARITH2SAFE((void *)gradient, gradient_e, (void *)(gradient + i), sizeof(double ), sizeof(double ), 1, 0); #line 306 CHECK_FSEQ2SAFE(gradient_e, (void *)(gradient + i), sizeof(double ), sizeof(double ), 1, 0); #line 306 (*(gradient + i)) = (*(gradient + i)) / magnitude; #line 305 i = i + 1; } #line 308 __retres = magnitude; #line 295 return (__retres); } } #line 311 double find_gradient_g_f(double * __FSEQ gradient , void *gradient_e ) ; #line 311 "compute.c" double find_gradient_g_f(double * __FSEQ gradient , void *gradient_e ) { int i ; double magnitude ; double __retres ; double __cil_tmp5 ; { #line 314 magnitude = 0.0; #line 316 CHECK_FSEQ2SAFE(gradient_e, (void *)gradient, sizeof(double ), sizeof(double ), 1, 0); #line 316 (*gradient) = (double )2 * P; #line 317 CHECK_FSEQARITH((void *)gradient, sizeof(double ), (void *)(gradient + 1)); #line 317 CHECK_FSEQ2SAFE(gradient_e, (void *)(gradient + 1), sizeof(double ), sizeof(double ), 1, 0); #line 317 (*(gradient + 1)) = (double )2 * Q; #line 318 i = 0; #line 318 while (i < 2) { #line 319 CHECK_FSEQARITH2SAFE((void *)gradient, gradient_e, (void *)(gradient + i), sizeof(double ), sizeof(double ), 1, 0); #line 319 CHECK_FSEQARITH2SAFE((void *)gradient, gradient_e, (void *)(gradient + i), sizeof(double ), sizeof(double ), 1, 0); #line 319 magnitude = magnitude + (*(gradient + i)) * (*(gradient + i)); #line 318 i = i + 1; } #line 320 __cil_tmp5 = sqrt(magnitude); #line 320 magnitude = __cil_tmp5; #line 321 i = 0; #line 321 while (i < 2) { #line 322 CHECK_FSEQARITH((void *)gradient, sizeof(double ), (void *)(gradient + i)); #line 322 CHECK_FSEQARITH2SAFE((void *)gradient, gradient_e, (void *)(gradient + i), sizeof(double ), sizeof(double ), 1, 0); #line 322 CHECK_FSEQ2SAFE(gradient_e, (void *)(gradient + i), sizeof(double ), sizeof(double ), 1, 0); #line 322 (*(gradient + i)) = (*(gradient + i)) / magnitude; #line 321 i = i + 1; } #line 324 __retres = magnitude; #line 311 return (__retres); } } #line 327 double find_gradient_h_f(double * __FSEQ gradient , void *gradient_e ) ; #line 327 "compute.c" double find_gradient_h_f(double * __FSEQ gradient , void *gradient_e ) { int i ; double magnitude ; double __retres ; double __cil_tmp5 ; { #line 330 magnitude = 0.0; #line 332 CHECK_FSEQ2SAFE(gradient_e, (void *)gradient, sizeof(double ), sizeof(double ), 1, 0); #line 332 (*gradient) = 1.0; #line 333 CHECK_FSEQARITH((void *)gradient, sizeof(double ), (void *)(gradient + 1)); #line 333 CHECK_FSEQ2SAFE(gradient_e, (void *)(gradient + 1), sizeof(double ), sizeof(double ), 1, 0); #line 333 (*(gradient + 1)) = - 5.0; #line 334 i = 0; #line 334 while (i < 2) { #line 335 CHECK_FSEQARITH2SAFE((void *)gradient, gradient_e, (void *)(gradient + i), sizeof(double ), sizeof(double ), 1, 0); #line 335 CHECK_FSEQARITH2SAFE((void *)gradient, gradient_e, (void *)(gradient + i), sizeof(double ), sizeof(double ), 1, 0); #line 335 magnitude = magnitude + (*(gradient + i)) * (*(gradient + i)); #line 334 i = i + 1; } #line 336 __cil_tmp5 = sqrt(magnitude); #line 336 magnitude = __cil_tmp5; #line 337 i = 0; #line 337 while (i < 2) { #line 338 CHECK_FSEQARITH((void *)gradient, sizeof(double ), (void *)(gradient + i)); #line 338 CHECK_FSEQARITH2SAFE((void *)gradient, gradient_e, (void *)(gradient + i), sizeof(double ), sizeof(double ), 1, 0); #line 338 CHECK_FSEQ2SAFE(gradient_e, (void *)(gradient + i), sizeof(double ), sizeof(double ), 1, 0); #line 338 (*(gradient + i)) = (*(gradient + i)) / magnitude; #line 337 i = i + 1; } #line 340 __retres = magnitude; #line 327 return (__retres); } } #line 343 void find_dd_grad_f_f(double pi_R , double pi_I , double * __FSEQ dd_grad , void *dd_grad_e ) ; #line 343 "compute.c" void find_dd_grad_f_f(double pi_R , double pi_I , double * __FSEQ dd_grad , void *dd_grad_e ) { double P_plus_1_inv ; double Q_plus_1_inv ; double P_grad_term ; double Q_grad_term ; double grad_mag ; double __cil_tmp9 ; { #line 345 P_plus_1_inv = (double )1 / (P + (double )1); #line 346 Q_plus_1_inv = (double )1 / (Q + (double )1); #line 347 P_grad_term = P_plus_1_inv - pi_R; #line 348 Q_grad_term = Q_plus_1_inv - pi_I; #line 351 __cil_tmp9 = sqrt(P_grad_term * P_grad_term + Q_grad_term * Q_grad_term); #line 351 grad_mag = __cil_tmp9; #line 353 CHECK_FSEQ2SAFE(dd_grad_e, (void *)dd_grad, sizeof(double ), sizeof(double ), 1, 0); #line 353 (*dd_grad) = - (((P_plus_1_inv * P_plus_1_inv) * P_grad_term) / grad_mag); #line 354 CHECK_FSEQARITH((void *)dd_grad, sizeof(double ), (void *)(dd_grad + 1)); #line 354 CHECK_FSEQ2SAFE(dd_grad_e, (void *)(dd_grad + 1), sizeof(double ), sizeof(double ), 1, 0); #line 354 (*(dd_grad + 1)) = - (((Q_plus_1_inv * Q_plus_1_inv) * Q_grad_term) / grad_mag); #line 343 return; } } #line 357 double make_orthogonal_ff(double * __FSEQ v_mod , void *v_mod_e , double * __FSEQ v_static , void *v_static_e ) ; #line 357 "compute.c" double make_orthogonal_ff(double * __FSEQ v_mod , void *v_mod_e , double * __FSEQ v_static , void *v_static_e ) { int i ; double total ; double length ; double tmp ; double __retres ; double __cil_tmp8 ; double __cil_tmp9 ; { #line 360 total = 0.0; #line 361 length = 0.0; #line 363 i = 0; #line 363 while (i < 2) { #line 364 CHECK_FSEQARITH2SAFE((void *)v_mod, v_mod_e, (void *)(v_mod + i), sizeof(double ), sizeof(double ), 1, 0); #line 364 CHECK_FSEQARITH2SAFE((void *)v_static, v_static_e, (void *)(v_static + i), sizeof(double ), sizeof(double ), 1, 0); #line 364 total = total + (*(v_mod + i)) * (*(v_static + i)); #line 363 i = i + 1; } #line 365 i = 0; #line 365 while (i < 2) { #line 366 CHECK_FSEQARITH((void *)v_mod, sizeof(double ), (void *)(v_mod + i)); #line 366 CHECK_FSEQARITH2SAFE((void *)v_mod, v_mod_e, (void *)(v_mod + i), sizeof(double ), sizeof(double ), 1, 0); #line 366 CHECK_FSEQARITH2SAFE((void *)v_static, v_static_e, (void *)(v_static + i), sizeof(double ), sizeof(double ), 1, 0); #line 366 CHECK_FSEQ2SAFE(v_mod_e, (void *)(v_mod + i), sizeof(double ), sizeof(double ), 1, 0); #line 366 (*(v_mod + i)) = (*(v_mod + i)) - total * (*(v_static + i)); #line 367 CHECK_FSEQARITH2SAFE((void *)v_mod, v_mod_e, (void *)(v_mod + i), sizeof(double ), sizeof(double ), 1, 0); #line 367 CHECK_FSEQARITH2SAFE((void *)v_mod, v_mod_e, (void *)(v_mod + i), sizeof(double ), sizeof(double ), 1, 0); #line 367 length = length + (*(v_mod + i)) * (*(v_mod + i)); #line 365 i = i + 1; } #line 369 __cil_tmp8 = sqrt(length); #line 369 length = __cil_tmp8; #line 370 i = 0; #line 370 while (i < 2) { #line 371 CHECK_FSEQARITH((void *)v_mod, sizeof(double ), (void *)(v_mod + i)); #line 371 CHECK_FSEQARITH2SAFE((void *)v_mod, v_mod_e, (void *)(v_mod + i), sizeof(double ), sizeof(double ), 1, 0); #line 371 CHECK_FSEQ2SAFE(v_mod_e, (void *)(v_mod + i), sizeof(double ), sizeof(double ), 1, 0); #line 371 (*(v_mod + i)) = (*(v_mod + i)) / length; #line 370 i = i + 1; } #line 373 if ((double )1 - total * total < 0) { #line 374 __retres = (double )0; goto return_label; } #line 376 __cil_tmp9 = sqrt((double )1 - total * total); #line 376 tmp = __cil_tmp9; #line 376 __retres = tmp; return_label: /* CIL Label */ ; #line 357 return (__retres); } } extern unsigned int ( __attribute__((__cdecl__)) /*9*/malloc)(size_t __size ) ; #line 15 "build.c" struct root * build_tree(void) ; #line 15 "build.c" struct root * build_tree(void) { int volatile ___first_local ; register int i ; register struct root * t ; register struct lateral * l ; struct root * __retres ; struct root * __cil_tmp6 ; struct root * __cil_tmp7 ; int iter8 ; struct lateral * __cil_tmp9 ; { #line 44 __retres = (struct root */* */)0; #line 44 l = (struct lateral */* */)0; #line 44 t = (struct root */* */)0; #line 26 __cil_tmp7 = (struct root */* */)/*9*/malloc(((sizeof((*t)) + 3U) >> 2) << 2); #line 26 if (__cil_tmp7) { #line 26 __cil_tmp6 = __cil_tmp7; #line 26 CHECK_POSITIVE((int )(((sizeof((*t)) + 3U) >> 2) << 2) - (int )sizeof(struct root )); iter8 = 0; while (iter8 < 10) { #line 26 __cil_tmp7->feeders[iter8] = (struct lateral */* */)0; iter8 = iter8 + 1; } } else { #line 26 __cil_tmp6 = 0; } #line 26 t = __cil_tmp6; #line 36 i = 0; #line 36 while (i < 10) { #line 38 __cil_tmp9 = build_lateral(i * 20, 20); #line 38 l = (struct lateral */* */)__cil_tmp9; #line 39 CHECK_NULL((void *)t); #line 39 CHECK_GEU(9U, (unsigned int )i); #line 39 CHECK_STOREPTR((void *)(& t->feeders[i]), (void *)((struct lateral */* */)l), (void *)(& ___first_local)); #line 39 t->feeders[i] = (struct lateral */* */)l; #line 36 i = i + 1; } #line 42 CHECK_NULL((void *)t); #line 42 t->theta_R = 0.8; #line 43 CHECK_NULL((void *)t); #line 43 t->theta_I = 0.16; #line 44 __retres = (struct root */* */)t; #line 15 CHECK_RETURNPTR((void *)__retres, (void *)(& ___first_local)); #line 15 return (__retres); } } #line 47 struct lateral * build_lateral(int i , int num ) ; #line 47 "build.c" struct lateral * build_lateral(int i , int num ) { int volatile ___first_local ; register struct lateral * l ; register struct branch * b ; register struct lateral * next ; int __a_local ; struct lateral * __retres ; struct lateral * __cil_tmp12 ; struct lateral * __cil_tmp13 ; struct lateral * __cil_tmp14 ; struct branch * __cil_tmp15 ; { #line 47 __retres = (struct lateral */* */)0; #line 47 next = (struct lateral */* */)0; #line 47 b = (struct branch */* */)0; #line 47 l = (struct lateral */* */)0; #line 47 if ((unsigned int )(& __a_local) <= ___stack_threshhold) { #line 47 ___stack_overflow(); } { #line 58 if (num == 0) { #line 58 CHECK_RETURNPTR((void *)((struct lateral */* */)0), (void *)(& ___first_local)); #line 58 return ((struct lateral */* */)0); } #line 70 __cil_tmp13 = (struct lateral */* */)/*9*/malloc(((sizeof((*l)) + 3U) >> 2) << 2); #line 70 if (__cil_tmp13) { #line 70 __cil_tmp12 = __cil_tmp13; #line 70 CHECK_POSITIVE((int )(((sizeof((*l)) + 3U) >> 2) << 2) - (int )sizeof(struct lateral )); #line 70 __cil_tmp13->branch = (struct branch */* */)0; #line 70 __cil_tmp13->next_lateral = (struct lateral */* */)0; } else { #line 70 __cil_tmp12 = 0; } #line 70 l = __cil_tmp12; #line 78 __cil_tmp14 = build_lateral(i, num - 1); #line 78 next = (struct lateral */* */)__cil_tmp14; #line 79 __cil_tmp15 = build_branch(i * 5, (num - 1) * 5, 5); #line 79 b = (struct branch */* */)__cil_tmp15; #line 87 CHECK_NULL((void *)l); #line 87 CHECK_STOREPTR((void *)(& l->next_lateral), (void *)((struct lateral */* */)next), (void *)(& ___first_local)); #line 87 l->next_lateral = (struct lateral */* */)next; #line 89 CHECK_NULL((void *)l); #line 89 CHECK_STOREPTR((void *)(& l->branch), (void *)((struct branch */* */)b), (void *)(& ___first_local)); #line 89 l->branch = (struct branch */* */)b; #line 90 CHECK_NULL((void *)l); #line 90 l->R = (double )1 / 300000.0; #line 91 CHECK_NULL((void *)l); #line 91 l->X = 0.000001; #line 92 CHECK_NULL((void *)l); #line 92 l->alpha = 0.0; #line 93 CHECK_NULL((void *)l); #line 93 l->beta = 0.0; #line 94 CHECK_RETURNPTR((void *)((struct lateral */* */)l), (void *)(& ___first_local)); #line 94 return ((struct lateral */* */)l); } #line 47 CHECK_RETURNPTR((void *)__retres, (void *)(& ___first_local)); #line 47 return (__retres); } } #line 97 struct branch * build_branch(int i , int j , int num ) ; #line 97 "build.c" struct branch * build_branch(int i , int j , int num ) { int volatile ___first_local ; register struct leaf * l ; register struct branch * b ; int __a_local ; struct branch * __retres ; struct branch * __cil_tmp10 ; struct branch * __cil_tmp11 ; int iter12 ; struct branch * __cil_tmp13 ; struct leaf * __cil_tmp14 ; { #line 97 __retres = (struct branch */* */)0; #line 97 b = (struct branch */* */)0; #line 97 l = (struct leaf */* */)0; #line 97 if ((unsigned int )(& __a_local) <= ___stack_threshhold) { #line 97 ___stack_overflow(); } { #line 105 if (num == 0) { #line 105 CHECK_RETURNPTR((void *)((struct branch */* */)0), (void *)(& ___first_local)); #line 105 return ((struct branch */* */)0); } #line 117 __cil_tmp11 = (struct branch */* */)/*9*/malloc(((sizeof((*b)) + 3U) >> 2) << 2); #line 117 if (__cil_tmp11) { #line 117 __cil_tmp10 = __cil_tmp11; #line 117 CHECK_POSITIVE((int )(((sizeof((*b)) + 3U) >> 2) << 2) - (int )sizeof(struct branch )); iter12 = 0; while (iter12 < 10) { #line 117 __cil_tmp11->leaves[iter12] = (struct leaf */* */)0; iter12 = iter12 + 1; } #line 117 __cil_tmp11->next_branch = (struct branch */* */)0; } else { #line 117 __cil_tmp10 = 0; } #line 117 b = __cil_tmp10; #line 122 __cil_tmp13 = build_branch(i, j, num - 1); #line 122 CHECK_NULL((void *)b); #line 122 CHECK_STOREPTR((void *)(& b->next_branch), (void *)((struct branch */* */)__cil_tmp13), (void *)(& ___first_local)); #line 122 b->next_branch = (struct branch */* */)__cil_tmp13; #line 127 i = 0; #line 127 while (i < 10) { #line 128 __cil_tmp14 = build_leaf(); #line 128 l = (struct leaf */* */)__cil_tmp14; #line 129 CHECK_NULL((void *)b); #line 129 CHECK_GEU(9U, (unsigned int )i); #line 129 CHECK_STOREPTR((void *)(& b->leaves[i]), (void *)((struct leaf */* */)l), (void *)(& ___first_local)); #line 129 b->leaves[i] = (struct leaf */* */)l; #line 127 i = i + 1; } #line 139 CHECK_NULL((void *)b); #line 139 b->R = 0.0001; #line 140 CHECK_NULL((void *)b); #line 140 b->X = 0.00002; #line 141 CHECK_NULL((void *)b); #line 141 b->alpha = 0.0; #line 142 CHECK_NULL((void *)b); #line 142 b->beta = 0.0; #line 143 CHECK_RETURNPTR((void *)((struct branch */* */)b), (void *)(& ___first_local)); #line 143 return ((struct branch */* */)b); } #line 97 CHECK_RETURNPTR((void *)__retres, (void *)(& ___first_local)); #line 97 return (__retres); } } #line 146 struct leaf * build_leaf(void) ; #line 146 "build.c" struct leaf * build_leaf(void) { int volatile ___first_local ; register struct leaf * l ; struct leaf * __retres ; struct leaf * __cil_tmp4 ; struct leaf * __cil_tmp5 ; { #line 153 __retres = (struct leaf */* */)0; #line 153 l = (struct leaf */* */)0; #line 150 __cil_tmp5 = (struct leaf */* */)/*9*/malloc(((sizeof((*l)) + 3U) >> 2) << 2); #line 150 if (__cil_tmp5) { #line 150 __cil_tmp4 = __cil_tmp5; #line 150 CHECK_POSITIVE((int )(((sizeof((*l)) + 3U) >> 2) << 2) - (int )sizeof(struct leaf )); } else { #line 150 __cil_tmp4 = 0; } #line 150 l = __cil_tmp4; #line 151 CHECK_NULL((void *)l); #line 151 l->D.P = 1.0; #line 152 CHECK_NULL((void *)l); #line 152 l->D.Q = 1.0; #line 153 __retres = (struct leaf */* */)l; #line 146 CHECK_RETURNPTR((void *)__retres, (void *)(& ___first_local)); #line 146 return (__retres); } } #line 36 "power.h" double wallclock ; #line 18 "main.c" double ( __FSEQ map_P)[36] = #line 18 { 8752.218091048, 8446.106670416, 8107.990680283, 7776.191574285, 7455.920518777, 7146.602181352, 6847.709026813, 6558.734204024, 6279.213382291, 6008.702199986, 5746.786181029, 5493.078256495, 5247.206333097, 5008.828069358, 4777.615815166, 4553.258735900, 4335.470002316, 4123.971545694, 3918.501939675, 3718.817618538, 3524.683625800, 3335.876573044, 3152.188635673, 2973.421417103, 2799.382330486, 2629.892542617, 2464.782829705, 2303.889031418, 2147.054385395, 1994.132771399, 1844.985347313, 1699.475053321, 1557.474019598, 1418.860479043, 1283.520126656, 1151.338004216}; #line 37 "main.c" double ( __FSEQ map_Q)[36] = #line 37 { 1768.846590190, 1706.229490046, 1637.253873079, 1569.637451623, 1504.419525242, 1441.477913810, 1380.700660446, 1321.980440476, 1265.218982201, 1210.322424636, 1157.203306183, 1105.780028163, 1055.974296746, 1007.714103979, 960.930643875, 915.558722782, 871.538200178, 828.810882006, 787.322098340, 747.020941334, 707.858376214, 669.787829741, 632.765987756, 596.751545633, 561.704466609, 527.587580585, 494.365739051, 462.004890691, 430.472546686, 399.738429196, 369.773787595, 340.550287137, 312.041496095, 284.222260660, 257.068973074, 230.557938283}; extern void * /*15*/__trusted_cast(unsigned int p ) ; extern unsigned int /*16*/wrapperAlloc(unsigned int ) ; extern char * /*17*/__mkptr_string(char * p ) ; extern void * /*19*/__trusted_deepcast(void * p ) ; struct meta_seq_void { void *_b ; void *_e ; } ; #line 65 extern int __ccured_va_count ; #line 59 "main.c" struct meta_seq_p_char { void *_b ; void *_e ; } ; #line 65 "main.c" static char __string1[21] = #line 65 { 'P', 'a', 's', 't', ' ', 'i', 'n', 'i', 't', 'i', 'a', 'l', 'i', 'z', 'a', 't', 'i', 'o', 'n', '\n', '\000'}; #line 71 "main.c" static char __string2[12] = #line 71 { 'B', 'u', 'i', 'l', 't', ' ', 't', 'r', 'e', 'e', '\n', '\000'}; #line 82 "main.c" static char __string3[44] = #line 82 { 'T', 'R', '=', '%', '1', '3', '.', '9', 'f', ',', ' ', 'T', 'I', '=', '%', '1', '3', '.', '9', 'f', ',', ' ', 'P', '0', '=', '%', '1', '3', '.', '9', 'f', ',', ' ', 'Q', '0', '=', '%', '1', '3', '.', '9', 'f', '\n', '\000'}; #line 100 "main.c" static char __string4[24] = #line 100 { 'D', ' ', 'T', 'R', '-', '%', '1', '3', '.', '9', 'f', ',', ' ', 'T', 'I', '=', '%', '1', '3', '.', '9', 'f', '\n', '\000'}; #line 110 "main.c" static char __string5[17] = #line 110 { 'E', 'l', 'a', 'p', 's', 'e', 'd', ' ', 't', 'i', 'm', 'e', ' ', '%', 'f', '\n', '\000'}; #line 59 int main(int argc , char * __ROSTRING * __argv_input ) ; #line 59 "main.c" int main(int argc , char * __ROSTRING * __argv_input ) { int volatile ___first_local ; char * * __SEQ argv ; struct root * r ; int i ; int finished ; double d_theta_R ; double d_theta_I ; double tmp___0 ; double tmp___1 ; clock_t tmp___2 ; int no_mangling14 ; int num_strings15 ; char * * p_argv16 ; unsigned int argvsize17 ; char * * tmp_argv18 ; int __retres ; void * __cil_tmp20 ; char * * __SEQ __cil_tmp21 ; char * * __SEQ __cil_tmp22 ; unsigned int __cil_tmp23 ; char * * __SEQ __cil_tmp24 ; char * __cil_tmp25 ; void * __cil_tmp27 ; void * __cil_tmp28 ; void * __SEQ __cil_tmp29 ; void * __SEQ __cil_tmp30 ; void * __SEQ __cil_tmp31 ; char * * __SEQ __cil_tmp32 ; unsigned int __cil_tmp33 ; clock_t __cil_tmp34 ; struct root * __cil_tmp35 ; double __cil_tmp36 ; double __cil_tmp37 ; clock_t __cil_tmp38 ; void *argv_b46 ; void *argv_e47 ; void *__cil_tmp21_b48 ; void *__cil_tmp21_e49 ; void *__cil_tmp24_b50 ; void *__cil_tmp24_e51 ; void *__cil_tmp29_b52 ; void *__cil_tmp29_e53 ; void *__cil_tmp30_b54 ; void *__cil_tmp30_e55 ; void *__cil_tmp31_b56 ; void *__cil_tmp31_e57 ; void *__cil_tmp32_b58 ; void *__cil_tmp32_e59 ; { #line 59 tmp_argv18 = (char * */* */)0; #line 59 p_argv16 = (char * */* */)0; #line 59 r = (struct root */* */)0; #line 59 argv_e47 = (void *)0; #line 59 argv_b46 = (void *)0; #line 59 argv = (char * */* __SEQ */)0; { #line 59 no_mangling14 = 0; #line 59 if ((int )__argv_input) { { #line 59 no_mangling14 = 0; #line 59 if (no_mangling14) { { #line 59 no_mangling14 = 1; } } } } else { { #line 59 no_mangling14 = 1; } } #line 59 if (no_mangling14) { { #line 59 __cil_tmp28 = /*19*/__trusted_deepcast((void */* */)__argv_input); #line 59 tmp_argv18 = (char * */* */)__cil_tmp28; #line 59 if ((void */* */)tmp_argv18) { #line 59 __cil_tmp30 = (void */* */)tmp_argv18; #line 59 __cil_tmp30_b54 = (void */* */)tmp_argv18; #line 59 __cil_tmp30_e55 = (void */* */)tmp_argv18 + sizeof((*argv)); #line 59 __cil_tmp29_e53 = __cil_tmp30_e55; #line 59 __cil_tmp29_b52 = __cil_tmp30_b54; #line 59 __cil_tmp29 = __cil_tmp30; } else { #line 59 __cil_tmp31 = 0; #line 59 __cil_tmp31_b56 = (void *)0; #line 59 __cil_tmp31_e57 = (void *)0; #line 59 __cil_tmp29_e53 = __cil_tmp31_e57; #line 59 __cil_tmp29_b52 = __cil_tmp31_b56; #line 59 __cil_tmp29 = __cil_tmp31; } #line 59 CHECK_SEQALIGN(sizeof(char */* */), (void *)((char * */* __SEQ */)__cil_tmp29), __cil_tmp29_b52, __cil_tmp29_e53); #line 59 __cil_tmp32 = (char * */* __SEQ */)__cil_tmp29; #line 59 __cil_tmp32_b58 = __cil_tmp29_b52; #line 59 __cil_tmp32_e59 = __cil_tmp29_e53; #line 59 argv_e47 = __cil_tmp32_e59; #line 59 argv_b46 = __cil_tmp32_b58; #line 59 argv = __cil_tmp32; } } else { { #line 59 num_strings15 = 0; #line 59 p_argv16 = (char * */* */)__argv_input; #line 59 while (1) { #line 59 CHECK_NULL((void *)p_argv16); #line 59 if (! ((int )((unsigned int )(*p_argv16)))) { #line 59 break; } { #line 59 num_strings15 = num_strings15 + 1; #line 59 __cil_tmp20 = /*15*/__trusted_cast((unsigned int )((void */* */)((long )p_argv16 + sizeof((*__argv_input))))); #line 59 p_argv16 = (char * */* */)__cil_tmp20; } } #line 59 argvsize17 = (unsigned int )((1 + num_strings15) * sizeof((*argv))); #line 59 __cil_tmp22 = (char * */* __SEQ */)/*16*/wrapperAlloc(((argvsize17 + 3U) >> 2) << 2); #line 59 if (__cil_tmp22) { #line 59 __cil_tmp21 = __cil_tmp22; #line 59 __cil_tmp21_b48 = (void *)__cil_tmp22; #line 59 __cil_tmp23 = (unsigned int )__cil_tmp22 + (((argvsize17 + 3U) >> 2) << 2); while ((unsigned int )__cil_tmp22 + sizeof(char */* */) <= __cil_tmp23) { #line 59 (*__cil_tmp22) = (char */* */)0; #line 59 __cil_tmp22 = __cil_tmp22 + 1; } #line 59 __cil_tmp21_e49 = __cil_tmp22; } else { #line 59 __cil_tmp21 = 0; #line 59 __cil_tmp21_b48 = (void *)0; #line 59 __cil_tmp21_e49 = (void *)0; } #line 59 __cil_tmp24 = __cil_tmp21; #line 59 __cil_tmp24_b50 = __cil_tmp21_b48; #line 59 __cil_tmp24_e51 = __cil_tmp21_e49; #line 59 argv_e47 = __cil_tmp24_e51; #line 59 argv_b46 = __cil_tmp24_b50; #line 59 argv = __cil_tmp24; #line 59 while (num_strings15 >= 0) { { #line 59 CHECK_NULL((void *)p_argv16); #line 59 __cil_tmp25 = /*17*/__mkptr_string((char */* */)(*p_argv16)); #line 59 CHECK_SEQ2SAFE(argv_b46, argv_e47, (void *)(argv + num_strings15), sizeof(char */* */), sizeof(char */* */), 1, 0); #line 59 CHECK_STOREPTR((void *)(argv + num_strings15), (void *)((char */* */)__cil_tmp25), (void *)(& ___first_local)); #line 59 (*(argv + num_strings15)) = (char */* */)__cil_tmp25; #line 59 __cil_tmp27 = /*15*/__trusted_cast((unsigned int )((void */* */)((long )p_argv16 - sizeof((*__argv_input))))); #line 59 p_argv16 = (char * */* */)__cil_tmp27; #line 59 num_strings15 = num_strings15 - 1; } } } } } #line 59 __ccuredAlwaysStopOnError = 1; #line 59 __ccuredUseStrings = 0; #line 59 __ccuredLogNonPointers = 0; #line 59 __ccuredInit(); #line 59 __cil_tmp33 = ___compute_stack_threshhold(); #line 59 ___stack_threshhold = __cil_tmp33; { #line 62 finished = 0; #line 65 __ccured_va_count = -1; #line 65 printf((char */* */)(& __string1[0])); #line 67 __cil_tmp34 = clock(); #line 67 wallclock = (double )__cil_tmp34; #line 70 __cil_tmp35 = build_tree(); #line 70 r = (struct root */* */)__cil_tmp35; #line 71 __ccured_va_count = -1; #line 71 printf((char */* */)(& __string2[0])); #line 72 Compute_Tree((struct root */* */)r); #line 73 CHECK_NULL((void *)r); #line 73 CHECK_NULL((void *)r); #line 73 r->last.P = r->D.P; #line 74 CHECK_NULL((void *)r); #line 74 CHECK_NULL((void *)r); #line 74 r->last.Q = r->D.Q; #line 75 CHECK_NULL((void *)r); #line 75 CHECK_NULL((void *)r); #line 75 r->last_theta_R = r->theta_R; #line 76 CHECK_NULL((void *)r); #line 76 CHECK_NULL((void *)r); #line 76 r->last_theta_I = r->theta_I; #line 77 CHECK_NULL((void *)r); #line 77 r->theta_R = 0.7; #line 78 CHECK_NULL((void *)r); #line 78 r->theta_I = 0.14; #line 80 while (! finished) { #line 81 Compute_Tree((struct root */* */)r); #line 82 __ccured_va_count = -1; #line 82 CHECK_NULL((void *)r); #line 82 CHECK_NULL((void *)r); #line 82 CHECK_NULL((void *)r); #line 82 CHECK_NULL((void *)r); #line 82 printf((char */* */)(& __string3[0]), r->theta_R, r->theta_I, r->D.P, r->D.Q); #line 84 CHECK_NULL((void *)r); #line 84 CHECK_NULL((void *)r); #line 84 __cil_tmp36 = fabs(r->D.P / 10000.0 - r->theta_R); #line 84 tmp___0 = __cil_tmp36; #line 84 if (tmp___0 < 0.00001) { #line 84 CHECK_NULL((void *)r); #line 84 CHECK_NULL((void *)r); #line 84 __cil_tmp37 = fabs(r->D.Q / 10000.0 - r->theta_I); #line 84 tmp___1 = __cil_tmp37; #line 84 if (tmp___1 < 0.00001) { #line 86 finished = 1; } else { goto _L; } } else { _L: /* CIL Label */ #line 88 CHECK_NULL((void *)r); #line 88 i = (int )((r->theta_R - 0.65) / 0.01); #line 89 if (i < 0) { #line 89 i = 0; } #line 90 if (i > 35) { #line 90 i = 35; } #line 91 CHECK_NULL((void *)r); #line 91 CHECK_NULL((void *)r); #line 91 CHECK_GEU(35U, (unsigned int )i + 1); #line 91 CHECK_GEU(35U, (unsigned int )i); #line 91 d_theta_R = - ((r->theta_R - r->D.P / 10000.0) / ((double )1 - (map_P[i + 1] - map_P[i]) / (0.01 * 10000.0))); #line 94 CHECK_NULL((void *)r); #line 94 i = (int )((r->theta_I - 0.13) / 0.002); #line 95 if (i < 0) { #line 95 i = 0; } #line 96 if (i > 35) { #line 96 i = 35; } #line 97 CHECK_NULL((void *)r); #line 97 CHECK_NULL((void *)r); #line 97 CHECK_GEU(35U, (unsigned int )i + 1); #line 97 CHECK_GEU(35U, (unsigned int )i); #line 97 d_theta_I = - ((r->theta_I - r->D.Q / 10000.0) / ((double )1 - (map_Q[i + 1] - map_Q[i]) / (0.002 * 10000.0))); #line 100 __ccured_va_count = -1; #line 100 printf((char */* */)(& __string4[0]), d_theta_R, d_theta_I); #line 101 CHECK_NULL((void *)r); #line 101 CHECK_NULL((void *)r); #line 101 r->last.P = r->D.P; #line 102 CHECK_NULL((void *)r); #line 102 CHECK_NULL((void *)r); #line 102 r->last.Q = r->D.Q; #line 103 CHECK_NULL((void *)r); #line 103 CHECK_NULL((void *)r); #line 103 r->last_theta_R = r->theta_R; #line 104 CHECK_NULL((void *)r); #line 104 CHECK_NULL((void *)r); #line 104 r->last_theta_I = r->theta_I; #line 105 CHECK_NULL((void *)r); #line 105 CHECK_NULL((void *)r); #line 105 r->theta_R = r->theta_R + d_theta_R; #line 106 CHECK_NULL((void *)r); #line 106 CHECK_NULL((void *)r); #line 106 r->theta_I = r->theta_I + d_theta_I; } } #line 109 __cil_tmp38 = clock(); #line 109 tmp___2 = __cil_tmp38; #line 109 wallclock = (1000000.0 * ((double )tmp___2 - wallclock)) / (double )1000; #line 110 __ccured_va_count = -1; #line 110 printf((char */* */)(& __string5[0]), wallclock / 1000.0); #line 115 return (0); } #line 59 return (__retres); } }