Skip to content

Commit 8f094e2

Browse files
author
Daniel Kroening
committed
added model for FreeBSD __flt_rounds
1 parent da34ceb commit 8f094e2

File tree

1 file changed

+10
-0
lines changed

1 file changed

+10
-0
lines changed

src/ansi-c/library/float.c

+10
Original file line numberDiff line numberDiff line change
@@ -83,3 +83,13 @@ inline int __builtin_flt_rounds(void)
8383
__CPROVER_rounding_mode==3?0: // to zero
8484
-1;
8585
}
86+
87+
/* FUNCTION: __flt_rounds */
88+
89+
int __builtin_flt_rounds(void);
90+
91+
inline int __flt_rounds(void)
92+
{
93+
// Spotted on FreeBSD
94+
return __builtin_flt_rounds();
95+
}

0 commit comments

Comments
 (0)