@@ -79,35 +79,37 @@ struct
79
79
let to_int x = Option. bind x (IArith. to_int)
80
80
let of_interval ?(suppress_ovwarn =false ) ik (x ,y ) = norm ~suppress_ovwarn ik @@ Some (x,y)
81
81
82
- let of_bitfield ik x =
83
- let min ik (z ,o ) =
84
- let signBit = Ints_t. shift_left Ints_t. one ((Size. bit ik) - 1 ) in
82
+ let of_bitfield ik x =
83
+ let min ik (z ,o ) =
84
+ let signBit = Ints_t. shift_left Ints_t. one ((Size. bit ik) - 1 ) in
85
85
let signMask = Ints_t. lognot (Ints_t. of_bigint (snd (Size. range ik))) in
86
86
let isNegative = Ints_t. logand signBit o <> Ints_t. zero in
87
- if GoblintCil. isSigned ik && isNegative then
87
+ if GoblintCil. isSigned ik && isNegative then
88
88
Ints_t. logor signMask (Ints_t. lognot z)
89
- else
89
+ else
90
90
Ints_t. lognot z
91
- in let max ik (z ,o ) =
92
- let signBit = Ints_t. shift_left Ints_t. one ((Size. bit ik) - 1 ) in
93
- let signMask = Ints_t. of_bigint (snd (Size. range ik)) in
94
- let isPositive = Ints_t. logand signBit z <> Ints_t. zero in
95
- if GoblintCil. isSigned ik && isPositive
96
- then Ints_t. logand signMask o
97
- else
98
- o
99
- in fst (norm ik (Some (min ik x, max ik x)))
91
+ in
92
+ let max ik (z ,o ) =
93
+ let signBit = Ints_t. shift_left Ints_t. one ((Size. bit ik) - 1 ) in
94
+ let signMask = Ints_t. of_bigint (snd (Size. range ik)) in
95
+ let isPositive = Ints_t. logand signBit z <> Ints_t. zero in
96
+ if GoblintCil. isSigned ik && isPositive then
97
+ Ints_t. logand signMask o
98
+ else
99
+ o
100
+ in
101
+ fst (norm ik (Some (min ik x, max ik x)))
100
102
101
103
let of_int ik (x : int_t ) = of_interval ik (x,x)
102
104
let zero = Some IArith. zero
103
105
let one = Some IArith. one
104
106
let top_bool = Some IArith. top_bool
105
107
106
- let to_bitfield ik z =
107
- match z with
108
- | None -> (Ints_t. lognot Ints_t. zero, Ints_t. lognot Ints_t. zero)
108
+ let to_bitfield ik z =
109
+ match z with
110
+ | None -> (Ints_t. lognot Ints_t. zero, Ints_t. lognot Ints_t. zero)
109
111
| Some (x ,y ) ->
110
- let (z,o) = fst(BitfieldDomain.Bitfield. of_interval ik (Ints_t. to_bigint x, Ints_t. to_bigint y)) in
112
+ let (z,o) = fst(BitfieldDomain.Bitfield. of_interval ik (Ints_t. to_bigint x, Ints_t. to_bigint y)) in
111
113
(Ints_t. of_bigint z, Ints_t. of_bigint o)
112
114
113
115
let of_bool _ik = function true -> one | false -> zero
@@ -407,8 +409,8 @@ struct
407
409
if M. tracing then M. trace " refine" " int_refine_with_congruence %a %a -> %a" pretty x pretty y pretty refn;
408
410
refn
409
411
410
- let refine_with_bitfield ik a b =
411
- let interv = of_bitfield ik b in
412
+ let refine_with_bitfield ik a b =
413
+ let interv = of_bitfield ik b in
412
414
meet ik a interv
413
415
414
416
let refine_with_interval ik a b = meet ik a b
0 commit comments