Skip to content

Commit d504358

Browse files
committed
Visual Studio: fix feraiseexcept test failure
We have a test that checks that our own implementation of feraiseexcept triggers an assertion failure when a non-zero argument is given. This test now fails since Visual Studio has in implementation for feraiseexcept in the fenv.h header file. This commit disables the test when using Visual Studio.
1 parent 9411c77 commit d504358

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)