Skip to content

Commit 1601a6f

Browse files
committed
Extract SharedFunctions.CilOfApron.cil_exp_of_int
1 parent 871a783 commit 1601a6f

File tree

1 file changed

+4
-4
lines changed

1 file changed

+4
-4
lines changed

src/cdomains/apron/sharedFunctions.apron.ml

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -281,8 +281,7 @@ struct
281281
raise Unsupported_Linexpr1
282282

283283
(** Returned boolean indicates whether returned expression should be negated. *)
284-
let coeff_to_const ~scalewith (c:Coeff.union_5) =
285-
let i = int_of_coeff_warn ~scalewith c in
284+
let cil_exp_of_int i =
286285
let ci,truncation = truncateCilint ILongLong i in
287286
if truncation = NoTruncation then
288287
if Z.compare i Z.zero >= 0 then
@@ -302,7 +301,8 @@ struct
302301
match V.to_cil_varinfo v with
303302
| Some vinfo when IntDomain.Size.is_cast_injective ~from_type:vinfo.vtype ~to_type:(TInt(ILongLong,[])) ->
304303
let var = Cilfacade.mkCast ~e:(Lval(Var vinfo,NoOffset)) ~newt:longlong in
305-
let flip, coeff = coeff_to_const ~scalewith c in
304+
let i = int_of_coeff_warn ~scalewith c in
305+
let flip, coeff = cil_exp_of_int i in
306306
if Z.equal (Option.get (Cil.getInteger coeff)) Z.one then (* Option.get should succeed by construction *) (* TODO: check (scaled!) coeff directly instead of extracting from exp *)
307307
flip, var
308308
else
@@ -322,7 +322,7 @@ struct
322322
if Coeff.is_zero c then
323323
ref []
324324
else
325-
ref [coeff_to_const ~scalewith c]
325+
ref [cil_exp_of_int (int_of_coeff_warn ~scalewith c)]
326326
in
327327
let append_summand (c:Coeff.union_5) v =
328328
if not (Coeff.is_zero c) then

0 commit comments

Comments
 (0)