Skip to content

Commit

Permalink
added model for FreeBSD __flt_rounds
Browse files Browse the repository at this point in the history
  • Loading branch information
Daniel Kroening committed Jun 6, 2018
1 parent da34ceb commit 8f094e2
Showing 1 changed file with 10 additions and 0 deletions.
10 changes: 10 additions & 0 deletions src/ansi-c/library/float.c
Original file line number Diff line number Diff line change
Expand Up @@ -83,3 +83,13 @@ inline int __builtin_flt_rounds(void)
__CPROVER_rounding_mode==3?0: // to zero
-1;
}

/* FUNCTION: __flt_rounds */

int __builtin_flt_rounds(void);

inline int __flt_rounds(void)
{
// Spotted on FreeBSD
return __builtin_flt_rounds();
}

0 comments on commit 8f094e2

Please sign in to comment.