Handle NaN in fib (#254)

UnitTestBot · Feb 17, 2025 · f8e9180 · f8e9180
1 parent 3f8f361
commit f8e9180
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 2 deletions.
diff --git a/usvm-ts/src/test/kotlin/org/usvm/samples/Call.kt b/usvm-ts/src/test/kotlin/org/usvm/samples/Call.kt
@@ -30,20 +30,24 @@ class Call : TsMethodTestRunner() {
         val method = getMethod("Call", "fib")
         discoverProperties<TsValue.TsNumber, TsValue.TsNumber>(
             method = method,
+            { n, r -> n.number.isNaN() && r.number == 0.0 },
             { n, r -> n.number < 0.0 && r.number == -1.0 },
             { n, r -> n.number > 10.0 && r.number == -2.0 },
             { n, r -> n.number == 0.0 && r.number == 1.0 },
             { n, r -> n.number == 1.0 && r.number == 1.0 },
-            { n, r -> n.number > 0 && n.number != 1.0 && fib(n.number) == r.number },
+            { n, r -> n.number > 0 && n.number != 1.0 && n.number <= 10.0 && fib(n.number) == r.number },
+            invariants = arrayOf(
+                { n, r -> fib(n.number) == r.number }
+            )
         )
     }
 }
 
 fun fib(n: Double): Double {
+    if (n.isNaN()) return 0.0
     if (n < 0) return -1.0
     if (n > 10) return -2.0
     if (n == 0.0) return 1.0
     if (n == 1.0) return 1.0
-
     return fib(n - 1.0) + fib(n - 2.0)
 }
diff --git a/usvm-ts/src/test/resources/samples/Call.ts b/usvm-ts/src/test/resources/samples/Call.ts
@@ -8,6 +8,7 @@ class Call {
     }
 
     fib(n: number): number {
+        if (n != n) return 0
         if (n < 0) return -1
         if (n > 10) return -2
         if (n == 0) return 1