Clean up Z_mlgmpidl usages

goblint · Nov 21, 2024 · aeb2376 · aeb2376
1 parent 065f990
commit aeb2376
Show file tree

Hide file tree

Showing 4 changed files with 6 additions and 4 deletions.
diff --git a/src/cdomains/apron/apronDomain.apron.ml b/src/cdomains/apron/apronDomain.apron.ml
@@ -19,7 +19,7 @@ module M = Messages
 
 let widening_thresholds_apron = ResettableLazy.from_fun (fun () ->
     let t = if GobConfig.get_string "ana.apron.threshold_widening_constants" = "comparisons" then WideningThresholds.octagon_thresholds () else WideningThresholds.thresholds_incl_mul2 () in
-    let r = List.map (fun x -> Apron.Scalar.of_mpqf @@ Mpqf.of_mpz @@ Z_mlgmpidl.mpz_of_z x) t in
+    let r = List.map Scalar.of_z t in
     Array.of_list r
   )
 

diff --git a/src/cdomains/apron/gobApron.apron.ml b/src/cdomains/apron/gobApron.apron.ml
@@ -12,6 +12,8 @@ struct
       let pp = pp
     end
     )
+
+  let of_z z = of_mpqf (Mpqf.of_mpz (Z_mlgmpidl.mpz_of_z z))
 end
 
 module Coeff =

diff --git a/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml b/src/cdomains/apron/linearTwoVarEqualityDomain.apron.ml
@@ -790,7 +790,7 @@ struct
     let of_coeff xi coeffs o =
       let typ = (Option.get @@ V.to_cil_varinfo xi).vtype in
       let ikind = Cilfacade.get_ikind typ in
-      let cst = Coeff.s_of_mpqf @@ Mpqf.of_mpz (Z_mlgmpidl.mpz_of_z @@ IntDomain.Size.cast ikind o) in
+      let cst = Coeff.s_of_z (IntDomain.Size.cast ikind o) in
       let lincons = Lincons1.make (Linexpr1.make t.env) Lincons1.EQ in
       Lincons1.set_list lincons coeffs (Some cst);
       lincons

diff --git a/src/cdomains/apron/sharedFunctions.apron.ml b/src/cdomains/apron/sharedFunctions.apron.ml
@@ -133,7 +133,7 @@ struct
           else
             failwith "texpr1_expr_of_cil_exp: globals must be replaced with temporary locals"
         | Const (CInt (i, _, _)) ->
-          Cst (Coeff.s_of_mpqf (Mpqf.of_mpz (Z_mlgmpidl.mpz_of_z i)))
+          Cst (Coeff.s_of_z i)
         | exp ->
           match Cilfacade.get_ikind_exp exp with
           | ik ->
@@ -175,7 +175,7 @@ struct
                     (* convert response to a constant *)
                     let const = IntDomain.IntDomTuple.to_int @@ IntDomain.IntDomTuple.cast_to t_ik res in
                     match const with
-                    | Some c -> Cst (Coeff.s_of_mpqf (Mpqf.of_mpz (Z_mlgmpidl.mpz_of_z c))) (* Got a constant value -> use it straight away *)
+                    | Some c -> Cst (Coeff.s_of_z c) (* Got a constant value -> use it straight away *)
                     (* I gotten top, we can not guarantee injectivity *)
                     | None -> if IntDomain.IntDomTuple.is_top_of t_ik res then raise (Unsupported_CilExp (Cast_not_injective t))
                       else ( (* Got a ranged value different from top, so let's check bounds manually *)
-Original file line number
+Diff line change
@@ Expand Up / @@ -12,6 +12,8 @@ struct @@
           let pp = pp
         end
         )
+      let of_z z = of_mpqf (Mpqf.of_mpz (Z_mlgmpidl.mpz_of_z z))
     end
     module Coeff =
@@ Expand Down @@