final attempt
git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@5380 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
This commit is contained in:
parent
30f47ed188
commit
c1da4057ff
|
@ -1,14 +1,18 @@
|
|||
#include <assert.h>
|
||||
#include <math.h>
|
||||
|
||||
#ifdef _MSC_VER
|
||||
#include <float.h>
|
||||
#define isnan(x) ((x)!=(x))
|
||||
#if defined(_MSC_VER) && _MSC_VER < 1800
|
||||
// don't have fenv.h
|
||||
#else
|
||||
#include <fenv.h>
|
||||
#endif
|
||||
|
||||
int main (void) {
|
||||
#if defined(_MSC_VER) && _MSC_VER < 1800
|
||||
#else
|
||||
|
||||
#ifdef FE_UPWARD
|
||||
#ifdef FW_DOWNWARD
|
||||
float f;
|
||||
float g;
|
||||
|
||||
|
@ -16,25 +20,21 @@ int main (void) {
|
|||
__CPROVER_assume(!isnan(g));
|
||||
|
||||
if (f > g) {
|
||||
#ifdef _MSC_VER
|
||||
_controlfp(_RC_UP, _MCW_RC);
|
||||
#else
|
||||
fesetround(FE_UPWARD);
|
||||
#endif
|
||||
}
|
||||
|
||||
if (f < g) {
|
||||
#ifdef _MSC_VER
|
||||
_controlfp(_RC_DOWN, _MCW_RC);
|
||||
#else
|
||||
fesetround(FE_DOWNWARD);
|
||||
#endif
|
||||
}
|
||||
|
||||
if ((!isinf(f)) && (g > 0.0f)) {
|
||||
float h = f + g;
|
||||
assert(h >= f);
|
||||
}
|
||||
#endif
|
||||
#endif
|
||||
|
||||
#endif
|
||||
|
||||
return 1;
|
||||
}
|
||||
|
|
Loading…
Reference in New Issue