We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
2 parents d7b229e + d504358 commit 7d01374Copy full SHA for 7d01374
regression/cbmc-library/feraiseexcept-01/main.c
@@ -1,9 +1,18 @@
1
#include <assert.h>
2
#include <fenv.h>
3
4
+int nondet_int();
5
+
6
int main()
7
{
- 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
15
feraiseexcept(exceptions);
16
+#endif
17
return 0;
18
}
0 commit comments