Skip to content

Commit aeb2829

Browse files
committed
Remove roundabout conversion in SharedFunctions.CilOfApron.cil_exp_of_linexpr1_term
1 parent 1601a6f commit aeb2829

File tree

1 file changed

+7
-4
lines changed

1 file changed

+7
-4
lines changed

src/cdomains/apron/sharedFunctions.apron.ml

Lines changed: 7 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -302,12 +302,15 @@ struct
302302
| Some vinfo when IntDomain.Size.is_cast_injective ~from_type:vinfo.vtype ~to_type:(TInt(ILongLong,[])) ->
303303
let var = Cilfacade.mkCast ~e:(Lval(Var vinfo,NoOffset)) ~newt:longlong in
304304
let i = int_of_coeff_warn ~scalewith c in
305-
let flip, coeff = cil_exp_of_int i in
306-
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 *)
307-
flip, var
308-
else
305+
if Z.equal i Z.one then
306+
false, var
307+
else if Z.equal i Z.minus_one then
308+
true, var
309+
else (
310+
let flip, coeff = cil_exp_of_int i in
309311
let prod = BinOp(Mult, coeff, var, longlong) in
310312
flip, prod
313+
)
311314
| None ->
312315
M.warn ~category:Analyzer "Invariant Apron: cannot convert to cil var: %a" Var.pretty v;
313316
raise Unsupported_Linexpr1

0 commit comments

Comments
 (0)