1 #include "fc3d_NaturalMapFABGenerated.h"
2 #include "funcodegen.h"
3 /*@
4 requires (0.0 <= rn <= 1.0e+6);
5 requires (-1.0e+6 <= rt1 <= 1.0e+6);
6 requires (-1.0e+6 <= rt2 <= 1.0e+6);
7 requires (-1.0e+6 <= un <= 1.0e+6);
8 requires (-1.0e+6 <= ut1 <= 1.0e+6);
9 requires (-1.0e+6 <= ut2 <= 1.0e+6);
10 requires (0.0 <= mu <= 1.0);
11 requires (-1.0e+6 <= rhon <= 1.0e+6);
12 requires (-1.0e+6 <= rhot1 <= 1.0e+6);
13 requires (-1.0e+6 <= rhot2 <= 1.0e+6);
14 assigns result[0..20];
15 ensures \is_finite((double) result[0]);
16 ensures \is_finite((double) result[1]);
17 ensures \is_finite((double) result[2]);
18 ensures \is_finite((double) result[3]);
19 ensures \is_finite((double) result[4]);
20 ensures \is_finite((double) result[5]);
21 ensures \is_finite((double) result[6]);
22 ensures \is_finite((double) result[7]);
23 ensures \is_finite((double) result[8]);
24 ensures \is_finite((double) result[9]);
25 ensures \is_finite((double) result[10]);
26 ensures \is_finite((double) result[11]);
27 ensures \is_finite((double) result[12]);
28 ensures \is_finite((double) result[13]);
29 ensures \is_finite((double) result[14]);
30 ensures \is_finite((double) result[15]);
31 ensures \is_finite((double) result[16]);
32 ensures \is_finite((double) result[17]);
33 ensures \is_finite((double) result[18]);
34 ensures \is_finite((double) result[19]);
35 ensures \is_finite((double) result[20]);*/
fc3d_NaturalMapFABGenerated(double rn,double rt1,double rt2,double un,double ut1,double ut2,double mu,double rhon,double rhot1,double rhot2,double * result)36 void fc3d_NaturalMapFABGenerated(
37 double rn,
38 double rt1,
39 double rt2,
40 double un,
41 double ut1,
42 double ut2,
43 double mu,
44 double rhon,
45 double rhot1,
46 double rhot2,
47 double *result)
48 {
49 /*@ assert \is_finite((double) ut1); */
50 /*@ assert \is_finite((double) epsilon); */
51 /*@ assert \is_finite((double) un); */
52 /*@ assert \is_finite((double) rt1); */
53 /*@ assert \is_finite((double) mu); */
54 /*@ assert \is_finite((double) ut2); */
55 /*@ assert \is_finite((double) rn); */
56 /*@ assert \is_finite((double) rt2); */
57 double x1 = 0.;
58 double x2 = 0.;
59 int x34 = 0;
60 int x35 = 0;
61 int x36 = 0;
62
63 double x4 = 0.;
64 double x6 = 0.;
65 double x29 = 0.;
66 double x30 = 0.;
67 double x31 = 0.;
68 double x32 = 0.;
69 double x33 = 0.;
70 double x81 = 0.;
71 double x82 = 0.;
72 double x83 = 0.;
73 double x103 = 0.;
74 double x104 = 0.;
75 double x125 = 0.;
76 double x126 = 0.;
77 double x127 = 0.;
78
79 x1 = rt1*rt1 + rt2*rt2;
80 /*@ assert x1 >= 0; */
81 x2 = ut1*ut1 + ut2*ut2;
82 /*@ assert x2 >= 0; */
83 x34 = x1 <= epsilon;
84 /*@ assert x34 <==> (x1 <= epsilon); */
85 x35 = x2 <= epsilon;
86 /*@ assert x35 <==> (x2 <= epsilon); */
87 x36 = x34 && x35;
88 /*@ assert x36 <==> (x34 && x35); */
89
90 int x47 = 0;
91 int x48 = 0;
92
93 double x7 = 0.;
94 double x37 = 0.;
95 double x38 = 0.;
96 double x39 = 0.;
97 double x40 = 0.;
98 double x41 = 0.;
99 double x42 = 0.;
100 double x43 = 0.;
101 double x44 = 0.;
102 double x45 = 0.;
103 double x46 = 0.;
104 double x65 = 0.;
105 double x84 = 0.;
106 double x85 = 0.;
107 double x86 = 0.;
108 double x87 = 0.;
109 double x88 = 0.;
110 double x89 = 0.;
111 double x90 = 0.;
112 double x91 = 0.;
113 double x92 = 0.;
114 double x93 = 0.;
115 double x94 = 0.;
116 double x95 = 0.;
117 double x96 = 0.;
118 double x97 = 0.;
119 double x98 = 0.;
120 double x105 = 0.;
121 double x106 = 0.;
122 double x107 = 0.;
123 double x108 = 0.;
124 double x109 = 0.;
125 double x128 = 0.;
126
127 x47 = x1 > epsilon;
128 /*@ assert x47 <==> (x1 > epsilon); */
129 x48 = x35 && x47;
130 /*@ assert x48 <==> (x35 && x47); */
131
132 double x10 = 0.;
133 double x11 = 0.;
134 double x12 = 0.;
135 double x13 = 0.;
136 double x14 = 0.;
137 double x15 = 0.;
138 double x16 = 0.;
139 int x49 = 0;
140 double x50 = 0.;
141 int x51 = 0;
142 int x52 = 0;
143
144 x10 = mu*ut1;
145 x11 = rt1 - x10;
146 x12 = x11*x11;
147 /*@ assert x12 >= 0; */
148 x13 = mu*ut2;
149 x14 = rt2 - x13;
150 x15 = x14*x14;
151 /*@ assert x15 >= 0; */
152 x16 = x12 + x15;
153 x49 = x2 >= epsilon;
154 /*@ assert x49 <==> (x2 >= epsilon); */
155 x50 = epsilon*(mu + 1);
156 /*@ assert x50 >= 0; */
157 /*@ assert x50 != 0; */
158 x51 = x16 <= x50;
159 /*@ assert x51 <==> (x16 <= x50); */
160 x52 = x34 && x49 && x51;
161 /*@ assert x52 <==> (x34 && x49 && x51); */
162
163 int x54 = 0;
164
165 double x53 = 0.;
166
167 x54 = x47 && x49 && x51;
168 /*@ assert x54 <==> (x47 && x49 && x51); */
169
170 int x62 = 0;
171 int x63 = 0;
172 int x64 = 0;
173
174 double x8 = 0.;
175 double x9 = 0.;
176 double x17 = 0.;
177 double x18 = 0.;
178 double x19 = 0.;
179 double x20 = 0.;
180 double x21 = 0.;
181 double x22 = 0.;
182 double x23 = 0.;
183 double x24 = 0.;
184 double x25 = 0.;
185 double x26 = 0.;
186 double x27 = 0.;
187 double x28 = 0.;
188 double x55 = 0.;
189 double x56 = 0.;
190 double x57 = 0.;
191 double x58 = 0.;
192 double x59 = 0.;
193 double x60 = 0.;
194 double x61 = 0.;
195 double x66 = 0.;
196 double x67 = 0.;
197 double x68 = 0.;
198 double x69 = 0.;
199 double x72 = 0.;
200 double x73 = 0.;
201 double x74 = 0.;
202 double x76 = 0.;
203 double x78 = 0.;
204 double x80 = 0.;
205 double x99 = 0.;
206 double x100 = 0.;
207 double x101 = 0.;
208 double x102 = 0.;
209 double x110 = 0.;
210 double x111 = 0.;
211 double x112 = 0.;
212 double x113 = 0.;
213 double x120 = 0.;
214 double x122 = 0.;
215 double x124 = 0.;
216 double x129 = 0.;
217
218 x62 = x49 && x51;
219 /*@ assert x62 <==> (x49 && x51); */
220 x63 = x35 || x62;
221 /*@ assert x63 <==> (x35 || x62); */
222 x64 = !x63;
223 /*@ assert x64 <==> (!x63); */
224
225 double x70 = 0.;
226 double x71 = 0.;
227
228 int x75 = 0;
229
230 double x77 = 0.;
231 double x79 = 0.;
232 double x114 = 0.;
233 double x115 = 0.;
234 double x116 = 0.;
235 double x117 = 0.;
236 double x118 = 0.;
237 double x119 = 0.;
238 double x121 = 0.;
239 double x123 = 0.;
240 double x130 = 0.;
241
242 x75 = x16 > x50;
243 /*@ assert x75 <==> (x16 > x50); */
244
245 if(x36)
246 {
247 x4 = 2*mu*mu - 2*mu + 1;
248 x6 = mu*rn;
249 /*@ assert x6 >= 0; */
250 /*@ assert 2 >= 0; */
251 x29 = sqrt(2);
252 /*@ assert x29 >= 0; */
253 /*@ assert x29 != 0; */
254 x30 = -1.0*un + x6;
255 x31 = Heaviside(x30);
256 x32 = mu*x31;
257 x33 = (1.0/2.0)*x29*x32;
258 /*@ assert x4 < -epsilon || x4 > epsilon; */
259 x81 = 1.0/x4;
260 x82 = mu - 1;
261 x83 = x82*x82;
262 /*@ assert x83 >= 0; */
263 x103 = mu*mu;
264 /*@ assert x103 >= 0; */
265 x104 = x31*x81;
266 x125 = -2.0*mu + 2*x103 + 1.0;
267 /*@ assert x125 < -epsilon || x125 > epsilon; */
268 x126 = 1.0/x125;
269 x127 = mu*mu*mu;
270 /*@ assert x127 >= 0; */
271
272 }
273 if(x48)
274 {
275 x6 = mu*rn;
276 x7 = -un;
277 /*@ assert 2 >= 0; */
278 x29 = sqrt(2);
279 x30 = -1.0*un + x6;
280 x37 = sqrt(x1);
281 /*@ assert x37 < -epsilon || x37 > epsilon; */
282 x38 = 1.0/x37;
283 x39 = 0.25*mu*x38;
284 x40 = Heaviside(x30 + x37);
285 x41 = 2*x40;
286 x42 = rt1*x41;
287 x43 = Heaviside(x30 - 1.0*x37);
288 x44 = 2.0*x43;
289 x45 = x29*x37;
290 x46 = x40*x45 + x43*x45;
291 x65 = rt2*x41;
292 /*@ assert x1 < -epsilon || x1 > epsilon; */
293 x84 = 1.0/((sqrt(x1))*(sqrt(x1))*(sqrt(x1)));
294 x85 = 0.25*mu*x84;
295 x86 = rt2*rt2;
296 /*@ assert x86 >= 0; */
297 x87 = x6 + x7;
298 x88 = Max(0, x37 + x87);
299 /*@ assert x88 >= 0; */
300 x89 = 2*x88;
301 x90 = Max(0, -x37 + x87);
302 /*@ assert x90 >= 0; */
303 x91 = 2.0*x90;
304 x92 = rt1*rt1;
305 /*@ assert x92 >= 0; */
306 x93 = 2*x37*x40;
307 x94 = 2*x37;
308 x95 = x43*x92;
309 x96 = rt1*rt1*rt1;
310 x97 = x40*x86;
311 x98 = x43*x86;
312 x105 = 2.0*x88;
313 x106 = 2*x90;
314 x107 = 2*x37*x43;
315 x108 = x40*x92;
316 x109 = x29*(x108 - x95 + x97 - x98);
317 x128 = rt2*rt2*rt2;
318
319 }
320 if(x52)
321 {
322 x6 = mu*rn;
323 /*@ assert 2 >= 0; */
324 x29 = sqrt(2);
325 x30 = -1.0*un + x6;
326 x31 = Heaviside(x30);
327 x32 = mu*x31;
328 x33 = (1.0/2.0)*x29*x32;
329
330 }
331 if(x54)
332 {
333 x6 = mu*rn;
334 x30 = -1.0*un + x6;
335 x37 = sqrt(x1);
336 /*@ assert x37 < -epsilon || x37 > epsilon; */
337 x38 = 1.0/x37;
338 x43 = Heaviside(x30 - 1.0*x37);
339 x53 = mu*x38*x43;
340
341 }
342 if(x64)
343 {
344 x6 = mu*rn;
345 x7 = -un;
346 x8 = sqrt(x2);
347 x9 = -mu*x8 + x6 + x7;
348 /*@ assert x16 >= 0; */
349 x17 = sqrt(x16);
350 x18 = x17 + x9;
351 x19 = Max(0, x18);
352 /*@ assert x19 >= 0; */
353 x20 = 0.5*x19;
354 x21 = -x20;
355 x22 = -x17 + x9;
356 x23 = Max(0, x22);
357 /*@ assert x23 >= 0; */
358 x24 = 0.5*x23;
359 x25 = Heaviside(x18);
360 x26 = 0.5*x25;
361 x27 = Heaviside(x22);
362 x28 = 0.5*x27;
363 /*@ assert x8 < -epsilon || x8 > epsilon; */
364 x55 = 1.0/x8;
365 x56 = -x10*x55;
366 /*@ assert x17 < -epsilon || x17 > epsilon; */
367 x57 = 1.0/x17;
368 x58 = mu*x57;
369 x59 = x11*x58;
370 x60 = x56 - x59;
371 x61 = x56 + x59;
372 x66 = -x13*x55;
373 x67 = x14*x58;
374 x68 = x66 - x67;
375 x69 = x66 + x67;
376 x72 = 0.5*x25*x57;
377 x73 = x11*x72;
378 x74 = 0.5*x27*x57;
379 x76 = x14*x72;
380 x78 = -rt1 + x10;
381 x80 = x74*x78;
382 x99 = -x58;
383 /*@ assert x16 < -epsilon || x16 > epsilon; */
384 x100 = 1.0/((sqrt(x16))*(sqrt(x16))*(sqrt(x16)));
385 x101 = mu*x100;
386 x102 = x11*x78;
387 x110 = x11*x14;
388 x111 = -0.5*mu*x100*x110*x19;
389 x112 = x14*x78;
390 x113 = 0.5*mu*x100*x23;
391 x120 = -rt2 + x13;
392 x122 = x11*x120;
393 x124 = x120*x74;
394 x129 = x120*x14;
395
396 }
397 if(x51)
398 {
399 x6 = mu*rn;
400 x7 = -un;
401 x8 = sqrt(x2);
402 x9 = -mu*x8 + x6 + x7;
403 /*@ assert x16 >= 0; */
404 x17 = sqrt(x16);
405 x18 = x17 + x9;
406 x19 = Max(0, x18);
407 x20 = 0.5*x19;
408 x21 = -x20;
409 x22 = -x17 + x9;
410 x23 = Max(0, x22);
411 x24 = 0.5*x23;
412 x25 = Heaviside(x18);
413 x26 = 0.5*x25;
414 x27 = Heaviside(x22);
415 x28 = 0.5*x27;
416 x30 = -1.0*un + x6;
417 x37 = sqrt(x1);
418 x43 = Heaviside(x30 - 1.0*x37);
419 x70 = -mu*x26;
420 x71 = mu*x28;
421
422 }
423 if(x75)
424 {
425 x6 = mu*rn;
426 x7 = -un;
427 x8 = sqrt(x2);
428 x9 = -mu*x8 + x6 + x7;
429 /*@ assert x16 >= 0; */
430 x17 = sqrt(x16);
431 x18 = x17 + x9;
432 x19 = Max(0, x18);
433 x20 = 0.5*x19;
434 x21 = -x20;
435 x22 = -x17 + x9;
436 x23 = Max(0, x22);
437 x24 = 0.5*x23;
438 x25 = Heaviside(x18);
439 x26 = 0.5*x25;
440 x27 = Heaviside(x22);
441 /*@ assert x17 < -epsilon || x17 > epsilon; */
442 x57 = 1.0/x17;
443 x58 = mu*x57;
444 x59 = x11*x58;
445 x67 = x14*x58;
446 x72 = 0.5*x25*x57;
447 x73 = x11*x72;
448 x74 = 0.5*x27*x57;
449 x76 = x14*x72;
450 x77 = 0.5*x19*x57;
451 x78 = -rt1 + x10;
452 x79 = 0.5*x23*x57;
453 x80 = x74*x78;
454 /*@ assert x16 < -epsilon || x16 > epsilon; */
455 x100 = 1.0/((sqrt(x16))*(sqrt(x16))*(sqrt(x16)));
456 x102 = x11*x78;
457 x110 = x11*x14;
458 x112 = x14*x78;
459 x114 = 0.5*mu*x27*x57;
460 x115 = 1.0/x16;
461 x116 = 0.5*x115*x25;
462 x117 = 0.5*x115*x27;
463 x118 = -x57;
464 x119 = x78*x78;
465 /*@ assert x119 >= 0; */
466 x120 = -rt2 + x13;
467 x121 = -x100*x120*x24*x78 - x110*x116;
468 x122 = x11*x120;
469 x123 = 0.5*x100*x19;
470 x124 = x120*x74;
471 x129 = x120*x14;
472 x130 = x120*x120;
473 /*@ assert x130 >= 0; */
474
475 }
476 if(x62)
477 {
478 x6 = mu*rn;
479 x30 = -1.0*un + x6;
480 x37 = sqrt(x1);
481 x43 = Heaviside(x30 - 1.0*x37);
482
483 }
484 x6 = mu*rn;
485 x7 = -un;
486 x8 = sqrt(x2);
487 x9 = -mu*x8 + x6 + x7;
488 /*@ assert x16 >= 0; */
489 x17 = sqrt(x16);
490 x18 = x17 + x9;
491 x19 = Max(0, x18);
492 x20 = 0.5*x19;
493 x21 = -x20;
494 x22 = -x17 + x9;
495 x23 = Max(0, x22);
496 x24 = 0.5*x23;
497 /*@ assigns result[0]; */
498 result[0] = x21 - x24 + x6;
499
500
501 /*@ assert x75 || x51; */
502 if(x75)
503 {
504 /*@ assigns result[1]; */
505 result[1] = rt1 - x11*x77 - x78*x79;
506
507 }
508 else if(x51)
509 {
510 /*@ assigns result[1]; */
511 result[1] = rt1;
512
513 }
514
515
516 if(x75)
517 {
518 /*@ assigns result[2]; */
519 result[2] = rt2 - x120*x79 - x14*x77;
520
521 }
522 else if(x51)
523 {
524 /*@ assigns result[2]; */
525 result[2] = rt2 + x21 + x24;
526
527 }
528
529 x25 = Heaviside(x18);
530 x26 = 0.5*x25;
531 x27 = Heaviside(x22);
532 x28 = 0.5*x27;
533 /*@ assigns result[3]; */
534 result[3] = x26 + x28;
535
536
537 if(x75)
538 {
539 /*@ assigns result[4]; */
540 result[4] = x73 + x80;
541
542 }
543 else if(x51)
544 {
545 /*@ assigns result[4]; */
546 result[4] = 0;
547 /*@ assert result[4] >= 0; */
548 }
549
550
551 if(x75)
552 {
553 /*@ assigns result[5]; */
554 result[5] = x124 + x76;
555
556 }
557 else if(x51)
558 {
559 /*@ assigns result[5]; */
560 result[5] = x26 - x28;
561
562 }
563
564
565 /*@ assert x36 || x48 || x52 || x54 || x64; */
566 if(x36)
567 {
568 /*@ assigns result[6]; */
569 result[6] = x33;
570
571 }
572 else if(x48)
573 {
574 /*@ assigns result[6]; */
575 result[6] = x39*(-rt1*x44 + x42 + x46);
576
577 }
578 else if(x52)
579 {
580 /*@ assigns result[6]; */
581 result[6] = x33;
582
583 }
584 else if(x54)
585 {
586 /*@ assigns result[6]; */
587 result[6] = rt1*x53;
588
589 }
590 else if(x64)
591 {
592 /*@ assigns result[6]; */
593 result[6] = -x26*x60 - x28*x61;
594
595 }
596
597
598 /*@ assert x36 || x48 || x62 || x64; */
599 if(x36)
600 {
601 /*@ assigns result[7]; */
602 result[7] = 1.0*x32*x81*x83;
603
604 }
605 else if(x48)
606 {
607 /*@ assigns result[7]; */
608 result[7] = x85*(x29*(rt1*x97 - rt1*x98 + x40*x96 - x43*x96) + x86*x89 - x86*x91 + x92*x93 + x94*x95);
609
610 }
611 else if(x62)
612 {
613 /*@ assigns result[7]; */
614 result[7] = 0.0;
615 /*@ assert result[7] >= 0; */
616 }
617 else if(x64)
618 {
619 /*@ assigns result[7]; */
620 result[7] = x21*(x101*x12 + x99) - x24*(x101*x102 - x99) - x60*x73 - x61*x80;
621
622 }
623
624
625 if(x36)
626 {
627 /*@ assigns result[8]; */
628 result[8] = 1.0*x103*x126*x31*x82;
629
630 }
631 else if(x48)
632 {
633 /*@ assigns result[8]; */
634 result[8] = rt2*x85*(-rt1*x105 + rt1*x106 + rt1*x107 + x109 + x37*x42);
635
636 }
637 else if(x62)
638 {
639 /*@ assigns result[8]; */
640 result[8] = 0.0;
641 /*@ assert result[8] >= 0; */
642 }
643 else if(x64)
644 {
645 /*@ assigns result[8]; */
646 result[8] = x111 - x113*x122 - x124*x61 - x60*x76;
647
648 }
649
650
651 if(x36)
652 {
653 /*@ assigns result[9]; */
654 result[9] = x33;
655
656 }
657 else if(x48)
658 {
659 /*@ assigns result[9]; */
660 result[9] = x39*(-rt2*x44 + x46 + x65);
661
662 }
663 else if(x52)
664 {
665 /*@ assigns result[9]; */
666 result[9] = x33;
667
668 }
669 else if(x54)
670 {
671 /*@ assigns result[9]; */
672 result[9] = rt2*x53;
673
674 }
675 else if(x64)
676 {
677 /*@ assigns result[9]; */
678 result[9] = -x26*x68 - x28*x69;
679
680 }
681
682
683 if(x36)
684 {
685 /*@ assigns result[10]; */
686 result[10] = x103*x104*(mu - 1.0);
687
688 }
689 else if(x48)
690 {
691 /*@ assigns result[10]; */
692 result[10] = rt1*x85*(-rt2*x105 + rt2*x106 + rt2*x107 + x109 + x37*x65);
693
694 }
695 else if(x62)
696 {
697 /*@ assigns result[10]; */
698 result[10] = 0.0;
699 /*@ assert result[10] >= 0; */
700 }
701 else if(x64)
702 {
703 /*@ assigns result[10]; */
704 result[10] = x111 - x112*x113 - x68*x73 - x69*x80;
705
706 }
707
708
709 if(x36)
710 {
711 /*@ assigns result[11]; */
712 result[11] = x104*x127;
713
714 }
715 else if(x48)
716 {
717 /*@ assigns result[11]; */
718 result[11] = x85*(x29*(rt2*x108 - rt2*x95 + x128*x40 - x128*x43) + x86*x93 + x89*x92 - x91*x92 + x94*x98);
719
720 }
721 else if(x62)
722 {
723 /*@ assigns result[11]; */
724 result[11] = mu*x43;
725
726 }
727 else if(x64)
728 {
729 /*@ assigns result[11]; */
730 result[11] = -x124*x69 + x21*(x101*x15 + x99) - x24*(x101*x129 - x99) - x68*x76;
731
732 }
733
734 x70 = -mu*x26;
735 x71 = mu*x28;
736 x82 = mu - 1;
737 /*@ assigns result[12]; */
738 result[12] = x70 - x71 + x82 + 1;
739
740
741 if(x75)
742 {
743 /*@ assigns result[13]; */
744 result[13] = -x114*x78 - x26*x59;
745
746 }
747 else if(x51)
748 {
749 /*@ assigns result[13]; */
750 result[13] = 0;
751 /*@ assert result[13] >= 0; */
752 }
753
754
755 if(x75)
756 {
757 /*@ assigns result[14]; */
758 result[14] = -x114*x120 - x26*x67;
759
760 }
761 else if(x51)
762 {
763 /*@ assigns result[14]; */
764 result[14] = x70 + x71;
765
766 }
767
768
769 /*@ assert x51 || x75; */
770 if(x51)
771 {
772 /*@ assigns result[15]; */
773 result[15] = 0.0;
774 /*@ assert result[15] >= 0; */
775 }
776 else if(x75)
777 {
778 /*@ assigns result[15]; */
779 result[15] = x11*x74 - x73;
780
781 }
782
783
784 if(x75)
785 {
786 /*@ assigns result[16]; */
787 result[16] = x102*x117 - x116*x12 + x21*(x100*x102 + x57) - x24*(x100*x119 + x118) + 1;
788
789 }
790 else if(x51)
791 {
792 /*@ assigns result[16]; */
793 result[16] = 1;
794 /*@ assert result[16] >= 0; */
795 /*@ assert result[16] != 0; */
796 }
797
798
799 if(x51)
800 {
801 /*@ assigns result[17]; */
802 result[17] = 0.0;
803 /*@ assert result[17] >= 0; */
804 }
805 else if(x75)
806 {
807 /*@ assigns result[17]; */
808 result[17] = -x112*x123 + x117*x122 + x121;
809
810 }
811
812
813 if(x51)
814 {
815 /*@ assigns result[18]; */
816 result[18] = 0.0;
817 /*@ assert result[18] >= 0; */
818 }
819 else if(x75)
820 {
821 /*@ assigns result[18]; */
822 result[18] = x14*x74 - x76;
823
824 }
825
826
827 if(x75)
828 {
829 /*@ assigns result[19]; */
830 result[19] = x112*x117 + x121 - x122*x123;
831
832 }
833 else if(x51)
834 {
835 /*@ assigns result[19]; */
836 result[19] = 0;
837 /*@ assert result[19] >= 0; */
838 }
839
840
841 if(x51)
842 {
843 /*@ assigns result[20]; */
844 result[20] = -1.0*x43 + 1.0;
845
846 }
847 else if(x75)
848 {
849 /*@ assigns result[20]; */
850 result[20] = -x116*x15 + x117*x129 + x21*(x100*x129 + x57) - x24*(x100*x130 + x118) + 1;
851
852 }
853 }
854 #ifdef __FRAMAC__
main()855 int main()
856 {
857 double rn = Frama_C_double_interval(0.0, 1.0e+6);
858 double rt1 = Frama_C_double_interval(-1.0e+6, 1.0e+6);
859 double rt2 = Frama_C_double_interval(-1.0e+6, 1.0e+6);
860 double un = Frama_C_double_interval(-1.0e+6, 1.0e+6);
861 double ut1 = Frama_C_double_interval(-1.0e+6, 1.0e+6);
862 double ut2 = Frama_C_double_interval(-1.0e+6, 1.0e+6);
863 double mu = Frama_C_double_interval(0.0, 1.0);
864 double rhon = Frama_C_double_interval(-1.0e+6, 1.0e+6);
865 double rhot1 = Frama_C_double_interval(-1.0e+6, 1.0e+6);
866 double rhot2 = Frama_C_double_interval(-1.0e+6, 1.0e+6);
867 double result[21];
868 fc3d_NaturalMapFABGenerated(rn, rt1, rt2, un, ut1, ut2, mu, rhon, rhot1, rhot2, result);
869 return(0);
870 }
871 #endif
872