Extract SharedFunctions.int_of_coeff

Author: sim642

src/cdomains/apron/gobApron.apron.ml

@@ -19,6 +19,14 @@ module Coeff =
 struct
   include Coeff
 
+  let pp = print
+  include Printable.SimpleFormat (
+    struct
+      type nonrec t = t
+      let pp = pp
+    end
+    )
+
   let s_of_z z = Coeff.s_of_mpqf (Mpqf.of_mpz (Z_mlgmpidl.mpz_of_z z))
 end
 

src/cdomains/apron/sharedFunctions.apron.ml

@@ -41,6 +41,10 @@ let int_of_scalar ?(scalewith=Z.one) ?round (scalar: Scalar.t) =
     | _ ->
       failwith ("int_of_scalar: unsupported: " ^ Scalar.show scalar)
 
+let int_of_coeff ?scalewith ?round (coeff: Coeff.union_5) =
+  match coeff with
+  | Scalar scalar -> int_of_scalar ?scalewith ?round scalar
+  | Interval _ -> None
 
 module type ConvertArg =
 sig
@@ -272,27 +276,24 @@ struct
 
   (** Returned boolean indicates whether returned expression should be negated. *)
   let coeff_to_const ~scalewith (c:Coeff.union_5) =
-    match c with
-    | Scalar c ->
-      (match int_of_scalar ?scalewith c with
-       | Some i ->
-         let ci,truncation = truncateCilint ILongLong i in
-         if truncation = NoTruncation then
-           if Z.compare i Z.zero >= 0 then
-             false, Const (CInt(i,ILongLong,None))
-           else
-             (* attempt to negate if that does not cause an overflow *)
-             let cneg, truncation = truncateCilint ILongLong (Z.neg i) in
-             if truncation = NoTruncation then
-               true, Const (CInt((Z.neg i),ILongLong,None))
-             else
-               false, Const (CInt(i,ILongLong,None))
-         else
-           raise Unsupported_Linexpr1
-       | None ->
-         M.warn ~category:Analyzer "Invariant Apron: coefficient is not int: %a" Scalar.pretty c;
-         raise Unsupported_Linexpr1)
-    | _ -> raise Unsupported_Linexpr1
+    match int_of_coeff ?scalewith c with
+    | Some i ->
+      let ci,truncation = truncateCilint ILongLong i in
+      if truncation = NoTruncation then
+        if Z.compare i Z.zero >= 0 then
+          false, Const (CInt(i,ILongLong,None))
+        else
+          (* attempt to negate if that does not cause an overflow *)
+          let cneg, truncation = truncateCilint ILongLong (Z.neg i) in
+          if truncation = NoTruncation then
+            true, Const (CInt((Z.neg i),ILongLong,None))
+          else
+            false, Const (CInt(i,ILongLong,None))
+      else
+        raise Unsupported_Linexpr1
+    | None ->
+      M.warn ~category:Analyzer "Invariant Apron: coefficient is not int: %a" Coeff.pretty c;
+      raise Unsupported_Linexpr1
 
   (** Returned boolean indicates whether returned expression should be negated. *)
   let cil_exp_of_linexpr1_term ~scalewith (c: Coeff.t) v =