source: CIVL/text/include/math.cvl@ 09d10de

1.23 2.0 acw/focus-triggers main test-branch
Last change on this file since 09d10de was 869af89, checked in by Ziqing Luo <ziqing@…>, 12 years ago

Complete math.cvl and add 5 new examples under examples/arithmetic/

git-svn-id: svn://vsl.cis.udel.edu/civl/trunk@1790 fb995dde-84ed-4084-dfe6-e5aef3e2452c

  • Property mode set to 100644
File size: 22.6 KB
Line 
1/* CIVL model of math.h */
2
3#ifdef __MATH_CIVL__
4#else
5#define __MATH_CIVL__
6#include <math.h>
7
8double acos(double x) {
9 $abstract double ACOS(double X);
10
11 $assert -1 <= x && x <=1 :
12 "Argument x should be in interval[-1, 1]";
13 $assume ACOS(x) >= 0;
14 return ACOS(x);
15}
16
17float acosf(float x) {
18 $abstract float ACOSF(float X);
19
20 $assert -1 <= x && x <=1 :
21 "Argument x should be in interval[-1, 1]";
22 $assume ACOSF(x) >= 0;
23 return ACOSF(x);
24}
25
26long double acosl(long double x) {
27 $abstract long double ACOSL(long double X);
28
29 $assert -1 <= x && x <=1 :
30 "Argument x should be in interval[-1, 1]";
31 $assume ACOSL(x) >= 0;
32 return ACOSL(x);
33}
34
35double asin(double x) {
36 $abstract double ASIN(double X);
37
38 $assert -1 <= x && x <= 1;
39 "Argument x should be in interval[-1, 1]";
40 return ASIN(x);
41}
42
43float asinf(float x) {
44 $abstract float ASINF(float X);
45
46 $assert -1 <= x && x <= 1;
47 "Argument x should be in interval[-1, 1]";
48 return ASINF(x);
49}
50
51long double asinl(long double x) {
52 $abstract long double ASINL(long double X);
53
54 $assert -1 <= x && x <= 1;
55 "Argument x should be in interval[-1, 1]";
56 return ASINL(x);
57}
58
59double atan(double x) {
60 $abstract double ATAN(double X);
61 return ATAN(x);
62}
63
64float atanf(float x) {
65 $abstract float ATANF(float X);
66 return ATANF(x);
67}
68
69long double atanl(long double x) {
70 $abstract long double ATANL(long double X);
71 return ATANL(x);
72}
73
74double atan2(double x, double y) {
75 $abstract double ATAN2(double X, double Y);
76
77 $assert x!=0 || y !=0 : "Arguments x and y"
78 "should not be both 0";
79 return ATAN2(x, y);
80}
81
82float atan2f(float x, float y) {
83 $abstract float ATAN2F(float X, float Y);
84
85 $assert x!=0.0 || y !=0.0 :
86 "Arguments x and y should not be both 0";
87 return ATAN2F(x, y);
88}
89
90long double atan2l(long double x, long double y) {
91 $abstract long double ATAN2L(long double X,
92 long double Y);
93
94 $assert x!=0.0 || y !=0.0 :
95 "Arguments x and y should not be both 0";
96 return ATAN2L(x, y);
97}
98
99double cos(double x) {
100 $abstract double COS(double X);
101
102 return COS(x);
103}
104
105float cosf(float x) {
106 $abstract float COSF(float X);
107
108 return COSF(x);
109}
110
111long double cosl(long double x) {
112 $abstract long double COSL(long double X);
113
114 return COSL(x);
115}
116
117double sin(double x) {
118 $abstract double SIN(double X);
119
120 return SIN(x);
121}
122
123float sinf(float x) {
124 $abstract float SINF(float X);
125
126 return SINF(x);
127}
128
129long double sinl(long double x) {
130 $abstract long double SINL(long double X);
131
132 return SINL(x);
133}
134
135double tan(double x) {
136 $abstract double TAN(double X);
137
138 return TAN(x);
139}
140
141float tanf(float x) {
142 $abstract float TANF(float X);
143
144 return TANF(x);
145}
146
147long double tanl(long double x) {
148 $abstract long double TANL(long double X);
149
150 return TANL(x);
151}
152
153double acosh(double x) {
154 $abstract double ACOSH(double X);
155
156 $assert x >= 1 : "Argument x should not less than 1.";
157 return ACOSH(x);
158}
159
160float acoshf(float x) {
161 $abstract float ACOSHF(float X);
162
163 $assert x >= 1 : "Argument x should not less than 1.";
164 return ACOSHF(x);
165}
166
167long double acoshl(long double x) {
168 $abstract long double ACOSHL(long double X);
169
170 $assert x >= 1 : "Argument x should not less than 1.";
171 return ACOSHL(x);
172}
173
174double asinh(double x) {
175 $abstract double ASINH(double X);
176
177 return ASINH(x);
178}
179
180float asinhf(float x) {
181 $abstract float ASINHF(float X);
182
183 return ASINHF(x);
184}
185
186long double asinhl(long double x) {
187 $abstract long double ASINHL(long double X);
188
189 return ASINHL(x);
190}
191
192double atanh(double x) {
193 $abstract double ATANH(double X);
194
195 $assert -1 < x && x < 1 :
196 "Argument x should be in the interval (-1, 1)";
197 return ATANH(x);
198}
199
200float atanhf(float x) {
201 $abstract float ATANHF(float X);
202
203 $assert -1 < x && x < 1 :
204 "Argument x should be in the interval (-1, 1)";
205 return ATANHF(x);
206}
207
208long double atanhl(long double x) {
209 $abstract long double ATANHL(long double X);
210
211 $assert -1 < x && x < 1 :
212 "Argument x should be in the interval (-1, 1)";
213 return ATANHL(x);
214}
215
216double cosh(double x) {
217 $abstract double COSH(double X);
218
219 return COSH(x);
220}
221
222float coshf(float x) {
223 $abstract float COSHF(float X);
224
225 return COSHF(x);
226}
227
228long double coshl(long double x) {
229 $abstract long double COSHL(long double X);
230
231 return COSHL(x);
232}
233
234double sinh(double x) {
235 $abstract double SINH(double X);
236
237 return SINH(x);
238}
239
240float sinhf(float x) {
241 $abstract float SINHF(float X);
242
243 return SINHF(x);
244}
245
246long double sinhl(long double x) {
247 $abstract long double SINHL(long double X);
248
249 return SINHL(x);
250}
251
252double tanh(double x) {
253 $abstract double TANH(double X);
254
255 return TANH(x);
256}
257
258float tanhf(float x) {
259 $abstract float TANHF(float X);
260
261 return TANHF(x);
262}
263
264long double tanhl(long double x) {
265 $abstract long double TANHL(long double X);
266
267 return TANHL(x);
268}
269
270double exp(double x) {
271 $abstract double EXP(double X);
272
273 $assume EXP(x) > 0;
274 return EXP(x);
275}
276
277float expf(float x) {
278 $abstract float EXPF(float X);
279
280 $assume EXPF(x) > 0;
281 return EXPF(x);
282}
283
284long double expl(long double x) {
285 $abstract long double EXPL(long double X);
286
287 $assume EXPL(x) > 0;
288 return EXPL(x);
289}
290
291double exp2(double x) {
292 $abstract double EXP2(double X);
293
294 $assume EXP2(x) > 0;
295 return EXP2(x);
296}
297
298float exp2f(float x) {
299 $abstract float EXP2F(float X);
300
301 $assume EXP2F(x) > 0;
302 return EXP2F(x);
303}
304
305long double exp2l(long double x) {
306 $abstract long double EXP2L(long double X);
307
308 $assume EXP2L(x) > 0;
309 return EXP2L(x);
310}
311
312double expm1(double x) {
313 $abstract double EXPM1(double X);
314
315 $assume EXPM1(x) > -1;
316 return EXPM1(x);
317}
318
319float expm1f(float x) {
320 $abstract float EXPM1F(float X);
321
322 $assume EXPM1F(x) > -1;
323 return EXPM1F(x);
324}
325
326long double expm1l(long double x) {
327 $abstract long double EXPM1L(long double X);
328
329 $assume EXPM1L(x) > -1;
330 return EXPM1L(x);
331}
332
333double frexp(double x, int * exp) {
334 $abstract double FREXP_X(double X);
335 $abstract int FREXP_EXP(double X);
336
337 (*exp) = FREXP_EXP(x);
338 $assume (FREXP_X(x) >= 1/2 && FREXP_X(x) < 1) ||
339 FREXP_X(x) == 0;
340 return FREXP_X(x);
341}
342
343float frexpf(float x, int *exp) {
344 $abstract float FREXPF_X(float X);
345 $abstract int FREXPF_EXP(float X);
346
347 (*exp) = FREXPF_EXP(x);
348 $assume (FREXPF_X(x) >= 1/2 && FREXPF_X(x) < 1) ||
349 FREXPF_X(x) == 0;
350 return FREXPF_X(x);
351}
352
353long double frexpl(long double x, int *exp) {
354 $abstract long double FREXPL_X(long double X);
355 $abstract int FREXPL_EXP(long double X);
356
357 (*exp) = FREXPL_EXP(x);
358 $assume (FREXPL_X(x) >= 1/2 && FREXPL_X(x) < 1) ||
359 FREXPL_X(x) == 0;
360 return FREXPL_X(x);
361}
362
363int ilogb(double x) {
364 $abstract int ILOGB(double X);
365
366 //TODO: x can not be infinite or NaN neither.
367 $assert x != 0 : "Argument x cannot be zero.";
368 return ILOGB(x);
369}
370
371int ilogbf(float x) {
372 $abstract int ILOGBF(float X);
373
374 //TODO: x can not be infinite or NaN neither.
375 $assert x != 0 : "Argument x cannot be zero.";
376 return ILOGBF(x);
377}
378
379int ilogbl(long double x) {
380 $abstract int ILOGBL(long double X);
381
382 //TODO: x can not be infinite or NaN neither.
383 $assert x != 0 : "Argument x cannot be zero.";
384 return ILOGBL(x);
385}
386
387double ldexp(double x, int exp) {
388 $abstract double LDEXP(double X, int EXP);
389
390 return LDEXP(x, exp);
391}
392
393float ldexpf(float x, int exp) {
394 $abstract float LDEXPF(float X, int EXP);
395
396 return LDEXPF(x, exp);
397}
398
399long double ldexpl(long double x, int exp) {
400 $abstract long double LDEXPL(long double X, int EXP);
401
402 return LDEXPL(x, exp);
403}
404
405double log(double x) {
406 $abstract double LOG(double X);
407
408 $assert x > 0 : "Argument x should be greater than 0";
409 return LOG(x);
410}
411
412float logf(float x) {
413 $abstract float LOGF(float X);
414
415 $assert x > 0 : "Argument x should be greater than 0";
416 return LOGF(x);
417}
418
419long double logl(long double x) {
420 $abstract long double LOGL(long double X);
421
422 $assert x > 0 : "Argument x should be greater than 0";
423 return LOGL(x);
424}
425
426double log10(double x) {
427 $abstract double LOG10(double X);
428
429 $assert x > 0 : "Argument x should be greater than 0";
430 return LOG10(x);
431}
432
433float log10f(float x) {
434 $abstract float LOG10F(float X);
435
436 $assert x > 0 : "Argument x should be greater than 0";
437 return LOG10F(x);
438}
439
440long double log10l(long double x) {
441 $abstract long double LOG10L(long double X);
442
443 $assert x > 0 : "Argument x should be greater than 0";
444 return LOG10L(x);
445}
446
447double log1p(double x) {
448 $abstract double LOG1P(double X);
449
450 $assert x > -1 : "Argument x should be greater than -1";
451 return LOG1P(x);
452}
453
454float log1pf(float x) {
455 $abstract float LOG1PF(float X);
456
457 $assert x > -1 : "Argument x should be greater than -1";
458 return LOG1PF(x);
459}
460
461long double log1pl(long double x) {
462 $abstract long double LOG1PL(long double X);
463
464 $assert x > -1 : "Argument x should be greater than -1";
465 return LOG1PL(x);
466}
467
468double log2(double x) {
469 $abstract double LOG2(double X);
470
471 $assert x > 0 : "Argument x should be greater than 0";
472 return LOG2(x);
473}
474
475float log2f(float x) {
476 $abstract float LOG2F(float X);
477
478 $assert x > 0 : "Argument x should be greater than 0";
479 return LOG2F(x);
480}
481
482long double log2l(long double x) {
483 $abstract long double LOG2L(long double X);
484
485 $assert x > 0 : "Argument x should be greater than 0";
486 return LOG2L(x);
487}
488
489double logb(double x) {
490 $abstract double LOGB(double X);
491
492 $assert x != 0 : "Argument x should not equal to 0";
493 return LOGB(x);
494}
495
496float logbf(float x) {
497 $abstract float LOGBF(float X);
498
499 $assert x != 0 : "Argument x should not equal to 0";
500 return LOGBF(x);
501}
502
503long double logbl(long double x) {
504 $abstract long double LOGBL(long double X);
505
506 $assert x != 0 : "Argument x should not equal to 0";
507 return LOGBL(x);
508}
509
510double modf(double value, double *iptr) {
511 $abstract double MODF_VALUE(double v);
512 $abstract double MODF_EXP(double v);
513
514 (*iptr) = MODF_EXP(value);
515 return MODF_VALUE(value);
516}
517
518float modff(float value, float *iptr) {
519 $abstract float MODFF_VALUE(float v);
520 $abstract float MODFF_EXP(float v);
521
522 (*iptr) = MODFF_EXP(value);
523 return MODFF_VALUE(value);
524}
525
526long double modfl(long double value, long double *iptr) {
527 $abstract long double MODFL_VALUE(long double v);
528 $abstract long double MODFL_EXP(long double v);
529
530 (*iptr) = MODFL_EXP(value);
531 return MODFL_VALUE(value);
532}
533
534double scalbn(double x, int n) {
535 $abstract double SCALBN(double x, int n);
536
537 return SCALBN(x, n);
538}
539
540float scalbnf(float x, int n) {
541 $abstract float SCALBNF(float x, int n);
542
543 return SCALBNF(x, n);
544}
545
546long double scalbnl(long double x, int n) {
547 $abstract long double SCALBNL(long double x, int n);
548
549 return SCALBNL(x, n);
550}
551
552double scalbln(double x, int n) {
553 $abstract double SCALBLN(double x, int n);
554
555 return SCALBLN(x, n);
556}
557
558float scalblnf(float x, int n) {
559 $abstract float SCALBLNF(float x, int n);
560
561 return SCALBLNF(x, n);
562}
563
564long double scalblnl(long double x, int n) {
565 $abstract long double SCALBLNL(long double x, int n);
566
567 return SCALBLNL(x, n);
568}
569
570double cbrt(double x) {
571 $abstract double CBRT(double x);
572
573 return CBRT(x);
574}
575
576float cbrtf(float x) {
577 $abstract float CBRTF(float x);
578
579 return CBRTF(x);
580}
581
582long double cbrtl(long double x) {
583 $abstract long double CBRTL(long double x);
584
585 return CBRTL(x);
586}
587
588double fabs(double x) {
589 if(x >= 0)
590 return x;
591 else
592 return -x;
593}
594
595float fabsf(float x) {
596 if(x >= 0)
597 return x;
598 else
599 return -x;
600}
601
602long double fabsl(long double x) {
603 if(x >= 0)
604 return x;
605 else
606 return -x;
607}
608
609double sqrt(double x) {
610 $abstract double SQRT(double x);
611
612 $assert x >= 0 : "Argument x should be greater than 0.";
613 $assume SQRT(x) >= 0;
614 return SQRT(x);
615}
616
617float sqrtf(float x) {
618 $abstract float SQRTF(float x);
619
620 $assert x >= 0 : "Argument x should be greater than 0.";
621 $assume SQRTF(x) >= 0;
622 return SQRTF(x);
623}
624
625long double sqrtl(long double x) {
626 $abstract long double SQRTL(long double x);
627
628 $assert x >= 0 : "Argument x should be greater than 0.";
629 $assume SQRTL(x) >= 0;
630 return SQRTL(x);
631}
632
633double hypot(double x, double y) {
634 double xsqrPLUSysqr = x*x + y*y;
635
636 return sqrt(xsqrPLUSysqr);
637}
638
639float hypotf(float x, float y) {
640 double xsqrPLUSysqr = x*x + y*y;
641
642 return sqrtf(xsqrPLUSysqr);
643}
644
645long double hypotl(long double x, long double y) {
646 double xsqrPLUSysqr = x*x + y*y;
647
648 return sqrtl(xsqrPLUSysqr);
649}
650
651double pow(double x, double y) {
652 $abstract double POW(double x, double y);
653
654 $assert x != 0 && y <= 0 : "It's invalid that argument x "
655 "is 0 and y is no greater than 0.";
656 return POW(x, y);
657}
658
659float powf(float x, float y) {
660 $abstract float POWF(float x, float y);
661
662 $assert x != 0 && y <= 0 : "It's invalid that argument x "
663 "is 0 and y is no greater than 0.";
664 return POWF(x, y);
665}
666
667long double powl(long double x, long double y) {
668 $abstract long double POWL(long double x,
669 long double y);
670
671 $assert x != 0 && y <= 0 : "It's invalid that argument x "
672 "is 0 and y is no greater than 0.";
673 return POWL(x, y);
674}
675
676double erf(double x) {
677 $abstract double ERF(double x);
678
679 return ERF(x);
680}
681
682float erff(float x) {
683 $abstract float ERFF(float x);
684
685 return ERFF(x);
686}
687
688long double erfl(long double x) {
689 $abstract long double ERFL(long double x);
690
691 return ERFL(x);
692}
693
694double erfc(double x) {
695 $abstract double ERFC(double x);
696
697 return ERFC(x);
698}
699
700float erfcf(float x) {
701 $abstract float ERFCF(float x);
702
703 return ERFCF(x);
704}
705
706long double erfcl(long double x) {
707 $abstract long double ERFCL(long double x);
708
709 return ERFCL(x);
710}
711
712double lgamma(double x) {
713 $abstract double LGAMMA(double x);
714
715 $assert(x > 0) :"Argument x should be greater than 0";
716 return LGAMMA(x);
717}
718
719float lgammaf(float x) {
720 $abstract float LGAMMAF(float x);
721
722 $assert(x > 0) :"Argument x should be greater than 0";
723 return LGAMMAF(x);
724}
725
726long double lgammal(long double x) {
727 $abstract long double LGAMMAL(long double x);
728
729 $assert(x > 0) :"Argument x should be greater than 0";
730 return LGAMMAL(x);
731}
732
733double tgamma(double x) {
734 $abstract double TGAMMA(double x);
735
736 $assert(x > 0) :"Argument x should be greater than 0";
737 return TGAMMA(x);
738}
739
740float tgammaf(float x) {
741 $abstract float TGAMMAF(float x);
742
743 $assert(x > 0) :"Argument x should be greater than 0";
744 return TGAMMAF(x);
745}
746
747long double tgammal(long double x) {
748 $abstract long double TGAMMAL(long double x);
749
750 $assert(x > 0) :"Argument x should be greater than 0";
751 return TGAMMAL(x);
752}
753
754double ceil(double x) {
755 $abstract double CEIL(double x);
756
757 $assume CEIL(x) >= x && CEIL(x) < (x + 1);
758 return CEIL(x);
759}
760
761float ceilf(float x) {
762 $abstract float CEILF(float x);
763
764 $assume CEILF(x) >= x && CEILF(x) < (x + 1);
765 return CEILF(x);
766}
767
768long double ceill(long double x) {
769 $abstract long double CEILL(long double x);
770
771 $assume CEILL(x) >= x && CEILL(x) < (x + 1);
772 return CEILL(x);
773}
774
775double floor(double x) {
776 $abstract double FLOOR(double x);
777
778 $assume FLOOR(x) <= x && FLOOR(x) > (x - 1);
779 return FLOOR(x);
780}
781
782float floorf(float x) {
783 $abstract float FLOORF(float x);
784
785 $assume FLOORF(x) <= x && FLOORF(x) > (x - 1);
786 return FLOORF(x);
787}
788
789long double floorl(long double x) {
790 $abstract long double FLOORL(long double x);
791
792 $assume FLOORL(x) <= x && FLOORL(x) > (x - 1);
793 return FLOORL(x);
794}
795
796double nearbyint(double x) {
797 $abstract double NEARBYINT(double x);
798
799 $assume NEARBYINT(x) < (x+1) && NEARBYINT(x) > (x-1);
800 return NEARBYINT(x);
801}
802
803float nearbyintf(float x) {
804 $abstract float NEARBYINTF(float x);
805
806 $assume NEARBYINTF(x) < (x+1) && NEARBYINTF(x) > (x-1);
807 return NEARBYINTF(x);
808}
809
810long double nearbyintl(long double x) {
811 $abstract long double NEARBYINTL(long double x);
812
813 $assume NEARBYINTL(x) < (x+1) && NEARBYINTL(x) > (x-1);
814 return NEARBYINTL(x);
815}
816
817double rint(double x) {
818 $abstract double RINT(double x);
819
820 $assume RINT(x) < (x+1) && RINT(x) > (x-1);
821 return RINT(x);
822}
823
824float rintf(float x) {
825 $abstract float RINTF(float x);
826
827 $assume RINTF(x) < (x+1) && RINTF(x) > (x-1);
828 return RINTF(x);
829}
830
831long double rintl(long double x) {
832 $abstract long double RINTL(long double x);
833
834 $assume RINTL(x) < (x+1) && RINTL(x) > (x-1);
835 return RINTL(x);
836}
837
838long int lrint(double x) {
839 $abstract long int LRINT(double x);
840
841 $assume LRINT(x) < (x+1) && LRINT(x) > (x-1);
842 return LRINT(x);
843}
844
845long int lrintf(float x) {
846 $abstract long int LRINTF(float x);
847
848 $assume LRINTF(x) < (x+1) && LRINTF(x) > (x-1);
849 return LRINTF(x);
850}
851
852long int lrintl(long double x) {
853 $abstract long int LRINTL(long double x);
854
855 $assume LRINTL(x) < (x+1) && LRINTL(x) > (x-1);
856 return LRINTL(x);
857}
858
859long long int llrint(double x) {
860 $abstract long long int LLRINT(double x);
861
862 $assume LLRINT(x) < (x+1) && LLRINT(x) > (x-1);
863 return LLRINT(x);
864}
865
866long long int llrintf(float x) {
867 $abstract long long int LLRINTF(float x);
868
869 $assume LLRINTF(x) < (x+1) && LLRINTF(x) > (x-1);
870 return LLRINTF(x);
871}
872
873long long int llrintl(long double x) {
874 $abstract long long int LLRINTL(long double x);
875
876 $assume LLRINTL(x) < (x+1) && LLRINTL(x) > (x-1);
877 return LLRINTL(x);
878}
879
880double round(double x) {
881 $abstract double ROUND(double x);
882
883 $assume ROUND(x) < (x+1) && ROUND(x) > (x-1);
884 return ROUND(x);
885}
886
887float roundf(float x) {
888 $abstract float ROUNDF(float x);
889
890 $assume ROUNDF(x) < (x+1) && ROUNDF(x) > (x-1);
891 return ROUNDF(x);
892}
893
894long double roundl(long double x) {
895 $abstract long double ROUNDL(long double x);
896
897 $assume ROUNDL(x) < (x+1) && ROUNDL(x) > (x-1);
898 return ROUNDL(x);
899}
900
901long int lround(double x) {
902 $abstract long int LROUND(double x);
903
904 $assume LROUND(x) < (x+1) && LROUND(x) > (x-1);
905 return LROUND(x);
906}
907
908long int lroundf(float x) {
909 $abstract long int LROUNDF(float x);
910
911 $assume LROUNDF(x) < (x+1) && LROUNDF(x) > (x-1);
912 return LROUNDF(x);
913}
914
915long int lroundl(long double x) {
916 $abstract long int LROUNDL(long double x);
917
918 $assume LROUNDL(x) < (x+1) && LROUNDL(x) > (x-1);
919 return LROUNDL(x);
920}
921
922long long int llround(double x) {
923 $abstract long long int LLROUND(double x);
924
925 $assume LLROUND(x) < (x+1) && LLROUND(x) > (x-1);
926 return LLROUND(x);
927}
928
929long long int llroundf(float x) {
930 $abstract long long int LLROUNDF(float x);
931
932 $assume LLROUNDF(x) < (x+1) && LLROUNDF(x) > (x-1);
933 return LLROUNDF(x);
934}
935
936long long int llroundl(long double x) {
937 $abstract long long int LLROUNDL(long double x);
938
939 $assume LLROUNDL(x) < (x+1) && LLROUNDL(x) > (x-1);
940 return LLROUNDL(x);
941}
942
943double trunc(double x) {
944 $abstract double TRUNC(double x);
945
946 $assume TRUNC(x) < (x) && TRUNC(x) > (x-1);
947 return TRUNC(x);
948}
949
950float truncf(float x) {
951 $abstract float TRUNCF(float x);
952
953 $assume TRUNCF(x) < (x) && TRUNCF(x) > (x-1);
954 return TRUNCF(x);
955}
956
957long double truncl(long double x) {
958 $abstract long double TRUNCL(long double x);
959
960 $assume TRUNCL(x) < (x) && TRUNCL(x) > (x-1);
961 return TRUNCL(x);
962}
963
964double fmod(double x, double y) {
965 $abstract double FMOD(double x, double y);
966
967 $assert y != 0 : "Argument y should not be 0";
968 return FMOD(x,y);
969}
970
971float fmodf(float x, float y) {
972 $abstract float FMODF(float x, float y);
973
974 $assert y != 0 : "Argument y should not be 0";
975 return FMODF(x,y);
976}
977
978long double fmodl(long double x, long double y) {
979 $abstract long double FMODL(long double x, long double y);
980
981 $assert y != 0 : "Argument y should not be 0";
982 return FMODL(x,y);
983}
984
985double remainder(double x, double y) {
986 $abstract double REMAINDER(double x, double y);
987
988 $assert y != 0 : "Argument y should not be 0";
989 return REMAINDER(x,y);
990}
991
992float remainderf(float x, float y) {
993 $abstract float REMAINDERF(float x, float y);
994
995 $assert y != 0 : "Argument y should not be 0";
996 return REMAINDERF(x,y);
997}
998
999long double remainderl(long double x, long double y) {
1000 $abstract long double REMAINDERL(long double x, long double y);
1001
1002 $assert y != 0 : "Argument y should not be 0";
1003 return REMAINDERL(x,y);
1004}
1005
1006
1007double remquo(double x, double y, int *quo) {
1008 $abstract double REMQUO(double x, double y);
1009 $abstract int REMQUO_QUO(double x, double y);
1010
1011 $assert y != 0 : "Argument y should not be 0";
1012 (*quo) = REMQUO_QUO(x, y);
1013 return REMQUO(x,y);
1014}
1015
1016float remquof(float x, float y, int *quo) {
1017 $abstract float REMQUOF(float x, float y);
1018 $abstract int REMQUOF_QUO(float x, float y);
1019
1020 $assert y != 0 : "Argument y should not be 0";
1021 (*quo) = REMQUOF_QUO(x, y);
1022 return REMQUOF(x,y);
1023}
1024
1025long double remquol(long double x, long double y, int *quo) {
1026 $abstract long double REMQUOL(long double x, long double y);
1027 $abstract int REMQUOL_QUO(long double x, long double y);
1028
1029 $assert y != 0 : "Argument y should not be 0";
1030 (*quo) = REMQUOL_QUO(x, y);
1031 return REMQUOL(x,y);
1032}
1033
1034double copysign(double x, double y) {
1035 $abstract double COPYSIGN(double x, double y);
1036
1037 return COPYSIGN(x,y);
1038}
1039
1040float copysignf(float x, float y) {
1041 $abstract float COPYSIGNF(float x, float y);
1042
1043 return COPYSIGNF(x,y);
1044}
1045
1046long double copysignl(long double x, long double y) {
1047 $abstract long double COPYSIGNL(long double x, long double y);
1048
1049 return COPYSIGNL(x,y);
1050}
1051
1052double nan(const char *tagp) {
1053 $abstract double NAN(const char *tagp);
1054
1055 return NAN(tagp);
1056}
1057
1058float nanf(const char *tagp) {
1059 $abstract float NANF(const char *tagp);
1060
1061 return NANF(tagp);
1062}
1063
1064long double nanl(const char *tagp) {
1065 $abstract long double NANL(const char *tagp);
1066
1067 return NANL(tagp);
1068}
1069
1070double nextafter(double x, double y) {
1071 $abstract double NEXTAFTER(double x, double y);
1072
1073 return NEXTAFTER(x,y);
1074}
1075
1076float nextafterf(float x, float y) {
1077 $abstract float NEXTAFTERF(float x, float y);
1078
1079 return NEXTAFTERF(x,y);
1080}
1081
1082long double nextafterl(long double x, long double y) {
1083 $abstract long double NEXTAFTERL(long double x, long double y);
1084
1085 return NEXTAFTERL(x,y);
1086}
1087
1088double nexttoward(double x, long double y) {
1089 $abstract double NEXTTOWARD(double x, long double y);
1090
1091 return NEXTTOWARD(x,y);
1092}
1093
1094float nexttowardf(float x, long double y) {
1095 $abstract float NEXTTOWARDF(float x, long double y);
1096
1097 return NEXTTOWARDF(x,y);
1098}
1099
1100long double nexttowardl(long double x, long double y) {
1101 $abstract long double NEXTTOWARDL(long double x, long double y);
1102
1103 return NEXTTOWARDL(x,y);
1104}
1105
1106double fdim(double x, double y) {
1107 return (x>y)?(x-y):0;
1108}
1109
1110float fdimf(float x, float y) {
1111 return (x>y)?(x-y):0;
1112}
1113
1114long double fdiml(long double x, long double y) {
1115 return (x>y)?(x-y):0;
1116}
1117
1118double fmax(double x, double y) {
1119 return (x>y)?(x):(y);
1120}
1121
1122float fmaxf(float x, float y) {
1123 return (x>y)?(x):(y);
1124}
1125
1126long double fmaxl(long double x, long double y) {
1127 return (x>y)?(x):(y);
1128}
1129
1130double fmin(double x, double y) {
1131 return (x<y)?(x):(y);
1132}
1133
1134float fminf(float x, float y) {
1135 return (x<y)?(x):(y);
1136}
1137
1138long double fminl(long double x, long double y) {
1139 return (x<y)?(x):(y);
1140}
1141
1142double fma(double x, double y, double z) {
1143 $abstract double FMA(double x, double y, double z);
1144
1145 return FMA(x,y,z);
1146}
1147
1148float fmaf(float x, float y, float z) {
1149 $abstract float FMAF(float x, float y, float z);
1150
1151 return FMAF(x,y,z);
1152}
1153
1154long double fmal(long double x, long double y, long double z) {
1155 $abstract long double FMAL(long double x,
1156 long double y, long double z);
1157
1158 return FMAL(x,y,z);
1159}
1160
1161#define isgreater(X,Y) ((X)>(Y))
1162#define isgreaterequal(X,Y) ((X)>=(Y))
1163#define isless(X,Y) ((X)<(Y))
1164#define islessequal(X,Y) ((X)<=(Y))
1165#define islessgreater(X,Y) ((X)<(Y))||((X)>(Y))
1166#define isunordered(X,Y) (X>Y)?1:0
1167
1168
1169
1170#endif
1171
1172
Note: See TracBrowser for help on using the repository browser.