Skip to content

Commit 118a1b8

Browse files
committed
Trim trailing whitespace in BaseInvariant (PR #1623)
1 parent 8dd4762 commit 118a1b8

File tree

1 file changed

+8
-8
lines changed

1 file changed

+8
-8
lines changed

src/analyses/baseInvariant.ml

Lines changed: 8 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -395,13 +395,13 @@ struct
395395
| Le, Some false -> meet_bin (ID.starting ikind (Z.succ l2)) (ID.ending ikind (Z.pred u1))
396396
| _, _ -> a, b)
397397
| _ -> a, b)
398-
| BOr ->
399-
(* Be careful: inv_exp performs a meet on both arguments of the BOr / BXor. *)
398+
| BOr ->
399+
(* Be careful: inv_exp performs a meet on both arguments of the BOr / BXor. *)
400400
if PrecisionUtil.get_bitfield () then
401401
(* refinement based on the following idea: bit set to one in c and set to zero in b must be one in a and bit set to zero in c must be zero in a too (analogously for b) *)
402-
let ((az, ao), (bz, bo)) = BitfieldDomain.Bitfield.refine_bor (ID.to_bitfield ikind a) (ID.to_bitfield ikind b) (ID.to_bitfield ikind c) in
402+
let ((az, ao), (bz, bo)) = BitfieldDomain.Bitfield.refine_bor (ID.to_bitfield ikind a) (ID.to_bitfield ikind b) (ID.to_bitfield ikind c) in
403403
ID.meet a (ID.of_bitfield ikind (az, ao)), ID.meet b (ID.of_bitfield ikind (bz, bo))
404-
else
404+
else
405405
(if M.tracing then M.tracel "inv" "Unhandled operator %a" d_binop op;
406406
(* Be careful: inv_exp performs a meet on both arguments of the BOr / BXor. *)
407407
(a, b)
@@ -416,7 +416,7 @@ struct
416416
a, b
417417
| BAnd ->
418418
(* we only attempt to refine a here *)
419-
let b_int = ID.to_int b in
419+
let b_int = ID.to_int b in
420420
let a =
421421
match b_int with
422422
| Some x when Z.equal x Z.one ->
@@ -426,11 +426,11 @@ struct
426426
| None -> a)
427427
| _ -> a
428428
in
429-
if PrecisionUtil.get_bitfield () then
429+
if PrecisionUtil.get_bitfield () then
430430
(* refinement based on the following idea: bit set to zero in c and set to one in b must be zero in a and bit set to one in c must be one in a too (analogously for b) *)
431-
let ((az, ao), (bz, bo)) = BitfieldDomain.Bitfield.refine_band (ID.to_bitfield ikind a) (ID.to_bitfield ikind b) (ID.to_bitfield ikind c) in
431+
let ((az, ao), (bz, bo)) = BitfieldDomain.Bitfield.refine_band (ID.to_bitfield ikind a) (ID.to_bitfield ikind b) (ID.to_bitfield ikind c) in
432432
ID.meet a (ID.of_bitfield ikind (az, ao)), ID.meet b (ID.of_bitfield ikind (bz, bo))
433-
else if b_int = None then
433+
else if b_int = None then
434434
(if M.tracing then M.tracel "inv" "Unhandled operator %a" d_binop op;
435435
(a, b)
436436
)

0 commit comments

Comments
 (0)