Skip to content

Commit 00cceab

Browse files
committed
Extract SharedFunctions.CilOfApron.int_of_coeff_warn
1 parent 4df87a7 commit 00cceab

File tree

1 file changed

+18
-16
lines changed

1 file changed

+18
-16
lines changed

src/cdomains/apron/sharedFunctions.apron.ml

Lines changed: 18 additions & 16 deletions
Original file line numberDiff line numberDiff line change
@@ -273,26 +273,28 @@ struct
273273

274274
let longlong = TInt(ILongLong,[])
275275

276+
let int_of_coeff_warn ?scalewith ?round coeff =
277+
match int_of_coeff ?scalewith ?round coeff with
278+
| Some i -> i
279+
| None ->
280+
M.warn ~category:Analyzer "Invariant Apron: coefficient is not int: %a" Coeff.pretty coeff;
281+
raise Unsupported_Linexpr1
276282

277283
(** Returned boolean indicates whether returned expression should be negated. *)
278284
let coeff_to_const ~scalewith (c:Coeff.union_5) =
279-
match int_of_coeff ?scalewith c with
280-
| Some i ->
281-
let ci,truncation = truncateCilint ILongLong i in
282-
if truncation = NoTruncation then
283-
if Z.compare i Z.zero >= 0 then
284-
false, Const (CInt(i,ILongLong,None))
285-
else
286-
(* attempt to negate if that does not cause an overflow *)
287-
let cneg, truncation = truncateCilint ILongLong (Z.neg i) in
288-
if truncation = NoTruncation then
289-
true, Const (CInt((Z.neg i),ILongLong,None))
290-
else
291-
false, Const (CInt(i,ILongLong,None))
285+
let i = int_of_coeff_warn ?scalewith c in
286+
let ci,truncation = truncateCilint ILongLong i in
287+
if truncation = NoTruncation then
288+
if Z.compare i Z.zero >= 0 then
289+
false, Const (CInt(i,ILongLong,None))
292290
else
293-
raise Unsupported_Linexpr1
294-
| None ->
295-
M.warn ~category:Analyzer "Invariant Apron: coefficient is not int: %a" Coeff.pretty c;
291+
(* attempt to negate if that does not cause an overflow *)
292+
let cneg, truncation = truncateCilint ILongLong (Z.neg i) in
293+
if truncation = NoTruncation then
294+
true, Const (CInt((Z.neg i),ILongLong,None))
295+
else
296+
false, Const (CInt(i,ILongLong,None))
297+
else
296298
raise Unsupported_Linexpr1
297299

298300
(** Returned boolean indicates whether returned expression should be negated. *)

0 commit comments

Comments
 (0)