Skip to content

Commit 7d01374

Browse files
authored
Merge pull request #8232 from diffblue/feraiseexcept
Visual Studio: fix feraiseexcept test failure
2 parents d7b229e + d504358 commit 7d01374

File tree

1 file changed

+10
-1
lines changed
  • regression/cbmc-library/feraiseexcept-01

1 file changed

+10
-1
lines changed
Lines changed: 10 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,9 +1,18 @@
11
#include <assert.h>
22
#include <fenv.h>
33

4+
int nondet_int();
5+
46
int main()
57
{
6-
int exceptions;
8+
int exceptions = nondet_int();
9+
#ifdef _MSC_VER
10+
// Visual Studio's fenv.h includes an inlined implementation of
11+
// feraiseexcept, which prevents us from using the one in
12+
// our library.
13+
__CPROVER_assert(0, "dummy assertion");
14+
#else
715
feraiseexcept(exceptions);
16+
#endif
817
return 0;
918
}

0 commit comments

Comments
 (0)