Merge pull request #1778 from jmid/adjust-div-zero-result-top-test

Adjust `test_FI_div_zero_result_top` QCheck test property to account for the 0/0 case

Author: sim642

src/cdomain/value/cdomains/floatDomain.ml

@@ -220,7 +220,9 @@ module FloatIntervalImpl(Float_t : CFloatType) = struct
     | _ -> Top
 
   (**for QCheck: should describe how to generate random values and shrink possible counter examples *)
-  let arbitrary () = QCheck.map convert_arb (QCheck.option (QCheck.pair QCheck.float QCheck.float))
+  let arbitrary () =
+    let gen = QCheck.map convert_arb (QCheck.option (QCheck.pair QCheck.float QCheck.float)) in
+    QCheck.set_print show gen
 
   let of_interval' interval =
     let x = norm @@ Interval interval

tests/unit/cdomains/floatDomainTest.ml

@@ -265,7 +265,10 @@ struct
 
   let test_FI_div_zero_result_top =
     QCheck.Test.make ~name:"test_FI_div_zero_result_top" (FI.arbitrary ()) (fun arg ->
-        FI.is_top (FI.div arg (FI.of_const 0.)))
+        let res = FI.div arg (FI.of_const 0.) in
+        if FI.equal arg fi_zero
+        then FI.equal res (FI.nan ())
+        else FI.is_top res)
 
   let test_FI_accurate_neg =
     QCheck.Test.make ~name:"test_FI_accurate_neg" QCheck.float (fun arg ->