add test case

goblint · Nov 23, 2023 · fde7d4d · fde7d4d
1 parent a7265c8
commit fde7d4d
Showing 1 changed file with 15 additions and 0 deletions.
diff --git a/tests/regression/39-signed-overflows/11-cos-noninf-nonnan.c b/tests/regression/39-signed-overflows/11-cos-noninf-nonnan.c
@@ -0,0 +1,15 @@
+// PARAM: --enable ana.int.interval --enable ana.float.interval --set ana.activated[+] tmpSpecial --html
+
+#include <math.h>
+
+int main() /* check_lower_bound */
+{
+    float x;
+
+    if(!(!__builtin_isnan (x) && !__builtin_isinf_sign (x))) abort();
+    float y = cosf(x);
+    if(!(__builtin_isgreaterequal(y, -1.0f)))
+      __goblint_check(0); // NOWARN (unreachable)
+    return 0;
+
+}