Do not set overflow flag on cast.

goblint · Nov 20, 2023 · 631f4fc · 631f4fc
1 parent 1e0a9de
commit 631f4fc
Showing 1 changed file with 6 additions and 6 deletions.
diff --git a/src/cdomains/intDomain.ml b/src/cdomains/intDomain.ml
@@ -3410,14 +3410,14 @@ module IntDomTupleImpl = struct
     | Some(_, {underflow; overflow}) -> not (underflow || overflow)
     | _ -> false
 
-  let check_ov ik intv intv_set =
+  let check_ov ~cast ik intv intv_set =
     let no_ov = (no_overflow ik intv) || (no_overflow ik intv_set) in
     if not no_ov && ( BatOption.is_some intv || BatOption.is_some intv_set) then (
       let (_,{underflow=underflow_intv; overflow=overflow_intv}) = match intv with None -> (I2.bot (), {underflow= true; overflow = true}) | Some x -> x in
       let (_,{underflow=underflow_intv_set; overflow=overflow_intv_set}) = match intv_set with None -> (I5.bot (), {underflow= true; overflow = true}) | Some x -> x in
       let underflow = underflow_intv && underflow_intv_set in
       let overflow = overflow_intv && overflow_intv_set in
-      set_overflow_flag ~cast:false ~underflow ~overflow ik;
+      set_overflow_flag ~cast ~underflow ~overflow ik;
     );
     no_ov
 
@@ -3426,7 +3426,7 @@ module IntDomTupleImpl = struct
     let map x = Option.map fst x in
     let intv =  f p2 @@ r.fi2_ovc (module I2) in
     let intv_set = f p5 @@ r.fi2_ovc (module I5) in
-    ignore (check_ov ik intv intv_set);
+    ignore (check_ov ~cast:false ik intv intv_set);
     map @@ f p1 @@ r.fi2_ovc (module I1), map @@ f p2 @@ r.fi2_ovc (module I2), map @@ f p3 @@ r.fi2_ovc (module I3), map @@ f p4 @@ r.fi2_ovc (module I4), map @@ f p5 @@ r.fi2_ovc (module I5)
 
   let create2_ovc ik r x = (* use where values are introduced *)
@@ -3607,7 +3607,7 @@ module IntDomTupleImpl = struct
     let map f ?no_ov = function Some x -> Some (f ?no_ov x) | _ -> None  in
     let intv = map (r.f1_ovc (module I2)) b in
     let intv_set = map (r.f1_ovc (module I5)) e in
-    let no_ov = check_ov ik intv intv_set in
+    let no_ov = check_ov ~cast ik intv intv_set in
     let no_ov = no_ov || should_ignore_overflow ik in
     refine ik
       ( map (fun ?no_ov x -> r.f1_ovc ?no_ov (module I1) x |> fst) a
@@ -3617,10 +3617,10 @@ module IntDomTupleImpl = struct
       , BatOption.map fst intv_set )
 
   (* map2 with overflow check *)
-  let map2ovc ik r (xa, xb, xc, xd, xe) (ya, yb, yc, yd, ye) =
+  let map2ovc ?(cast=false) ik r (xa, xb, xc, xd, xe) (ya, yb, yc, yd, ye) =
     let intv = opt_map2 (r.f2_ovc (module I2)) xb yb in
     let intv_set = opt_map2 (r.f2_ovc (module I5)) xe ye in
-    let no_ov = check_ov ik intv intv_set in
+    let no_ov = check_ov ~cast ik intv intv_set in
     let no_ov = no_ov || should_ignore_overflow ik in
     refine ik
       ( opt_map2 (fun ?no_ov x y -> r.f2_ovc ?no_ov (module I1) x y |> fst) xa ya