Skip to content

Commit 7c053bf

Browse files
authored
Merge pull request #2290 from diffblue/flt_rounds
added model for FreeBSD __flt_rounds
2 parents 4a7a389 + 8f094e2 commit 7c053bf

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)