support clang's __builtin_flt_rounds
This commit is contained in:
parent
f97c169f57
commit
d1a7403fbf
|
@ -0,0 +1,31 @@
|
|||
// This is C99, but currently only works with clang.
|
||||
// gcc and Visual Studio appear to hard-wire FLT_ROUNDS to 1.
|
||||
|
||||
#ifdef __clang__
|
||||
|
||||
#include <assert.h>
|
||||
#include <fenv.h>
|
||||
#include <float.h>
|
||||
|
||||
int main()
|
||||
{
|
||||
fesetround(FE_DOWNWARD);
|
||||
assert(FLT_ROUNDS==3);
|
||||
|
||||
fesetround(FE_TONEAREST);
|
||||
assert(FLT_ROUNDS==1);
|
||||
|
||||
fesetround(FE_TOWARDZERO);
|
||||
assert(FLT_ROUNDS==0);
|
||||
|
||||
fesetround(FE_UPWARD);
|
||||
assert(FLT_ROUNDS==2);
|
||||
}
|
||||
|
||||
#else
|
||||
|
||||
int main()
|
||||
{
|
||||
}
|
||||
|
||||
#endif
|
|
@ -0,0 +1,8 @@
|
|||
CORE
|
||||
main.c
|
||||
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
^VERIFICATION SUCCESSFUL$
|
||||
--
|
||||
^warning: ignoring
|
|
@ -1,3 +1,5 @@
|
|||
typedef float __gcc_v4sf __attribute__ ((__vector_size__ (16)));
|
||||
|
||||
__gcc_v4sf __builtin_shufflevector(__gcc_v4sf, __gcc_v4sf, ...);
|
||||
|
||||
int __builtin_flt_rounds(void);
|
||||
|
|
|
@ -67,3 +67,19 @@ inline int _isnan(double x)
|
|||
{
|
||||
return __CPROVER_isnand(x);
|
||||
}
|
||||
|
||||
/* FUNCTION: __builtin_flt_rounds */
|
||||
|
||||
extern int __CPROVER_rounding_mode;
|
||||
|
||||
inline int __builtin_flt_rounds(void)
|
||||
{
|
||||
// This is a clang builtin for FLT_ROUNDS
|
||||
// The magic numbers are C99 and different from the
|
||||
// x86 encoding that CPROVER uses.
|
||||
return __CPROVER_rounding_mode==0?1: // to nearest
|
||||
__CPROVER_rounding_mode==1?3: // downward
|
||||
__CPROVER_rounding_mode==2?2: // upward
|
||||
__CPROVER_rounding_mode==3?0: // to zero
|
||||
-1;
|
||||
}
|
||||
|
|
Loading…
Reference in New Issue