Skip to content

Commit f76ae66

Browse files
committed
Trim trailing whitespace in int domains (PR #1739)
1 parent 538b3e7 commit f76ae66

File tree

4 files changed

+8
-8
lines changed

4 files changed

+8
-8
lines changed

src/cdomain/value/cdomains/int/defExcDomain.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -470,7 +470,7 @@ struct
470470
| `Bot -> `Bot
471471

472472
let logand ik x y = norm ik (match x,y with
473-
| `Excluded (_, r), `Definite i
473+
| `Excluded (_, r), `Definite i
474474
| `Definite i, `Excluded (_, r) ->
475475
if Z.equal i Z.zero then
476476
`Definite Z.zero

src/cdomain/value/cdomains/int/intervalDomain.ml

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -244,7 +244,7 @@ struct
244244
| result when not (is_top_of ik result) && not (is_bot result) -> result
245245
| _ ->
246246
match i1, i2 with
247-
| Some (x1, x2), Some (y1, y2) ->
247+
| Some (x1, x2), Some (y1, y2) ->
248248
let is_nonneg x = Ints_t.compare x Ints_t.zero >= 0 in
249249
begin match is_nonneg x1, is_nonneg x2, is_nonneg y1, is_nonneg y2 with
250250
| true, _, true, _ ->
@@ -290,11 +290,11 @@ struct
290290
end
291291
| _ -> top_of ik
292292

293-
let logor ik i1 i2 =
293+
let logor ik i1 i2 =
294294
match bit (fun _ik -> Ints_t.logor) ik i1 i2 with
295295
| result when not (is_top_of ik result) && not (is_bot result) -> result
296296
| _ ->
297-
match i1, i2 with
297+
match i1, i2 with
298298
| Some (x1, x2), Some (y1, y2) ->
299299
let is_nonneg x = Ints_t.compare x Ints_t.zero >= 0 in
300300
begin match is_nonneg x1, is_nonneg x2, is_nonneg y1, is_nonneg y2 with
@@ -309,7 +309,7 @@ struct
309309
of_interval ik (lower, upper) |> fst
310310
end
311311
| _ -> top_of ik
312-
312+
313313
let bit1 f ik i1 f' =
314314
if is_bot i1 then
315315
bot_of ik
@@ -335,7 +335,7 @@ struct
335335
| Some x, Some y -> (try of_int ik (Ints_t.shift_right x (Ints_t.to_int y)) with Division_by_zero | Invalid_argument _ -> (top_of ik, {underflow=false; overflow=false}))
336336
| _, _->
337337
let is_nonneg x = Ints_t.compare x Ints_t.zero >= 0 in
338-
match i1, i2 with
338+
match i1, i2 with
339339
| Some (x1, x2), Some (y1,y2) when is_nonneg x1 && is_nonneg y1 ->
340340
of_interval ik (Ints_t.zero, Ints_t.div x2 (Ints_t.shift_left Ints_t.one (Ints_t.to_int y1)))
341341
| _ -> (top_of ik, {underflow=false; overflow=false})

src/cdomain/value/cdomains/int/intervalSetDomain.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -342,7 +342,7 @@ struct
342342
let (x1, x2), (y1, y2) = i1, i2 in
343343
let is_nonneg x = Ints_t.compare x Ints_t.zero >= 0 in
344344
match is_nonneg x1, is_nonneg x2, is_nonneg y1, is_nonneg y2 with
345-
| true, _, true, _ ->
345+
| true, _, true, _ ->
346346
of_interval ik (Ints_t.zero, Ints_t.min x2 y2) |> fst
347347
| _, false, _, false ->
348348
of_interval ik (min_val_bit_constrained @@ Ints_t.min x1 y1, Ints_t.zero) |> fst

src/cdomain/value/cdomains/valueDomain.ml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -979,7 +979,7 @@ struct
979979
do_eval_offset ask f x offs exp l o v t
980980

981981
let update_offset ?(blob_destructive=false) (ask: VDQ.t) (x:t) (offs:offs) (value:t) (exp:exp option) (v:lval) (t:typ): t =
982-
let rec do_update_offset ?(bitfield:int option=None) (ask:VDQ.t) (x:t) (offs:offs) (value:t) (exp:exp option) (l:lval option) (o:offset option) (v:lval) (t:typ):t =
982+
let rec do_update_offset ?(bitfield:int option=None) (ask:VDQ.t) (x:t) (offs:offs) (value:t) (exp:exp option) (l:lval option) (o:offset option) (v:lval) (t:typ):t =
983983
if M.tracing then M.traceli "update_offset" "do_update_offset %a %a (%a) %a" pretty x Offs.pretty offs (Pretty.docOpt (CilType.Exp.pretty ())) exp pretty value;
984984
let mu = function Blob (Blob (y, s', zeroinit), s, _) -> Blob (y, ID.join s s', zeroinit) | x -> x in
985985
let r =

0 commit comments

Comments
 (0)