Skip to content

Commit

Permalink
Fix indentation in various non-legacy code
Browse files Browse the repository at this point in the history
  • Loading branch information
sim642 committed Feb 14, 2024
1 parent 7c545fc commit c3e2cc8
Show file tree
Hide file tree
Showing 5 changed files with 281 additions and 281 deletions.
28 changes: 14 additions & 14 deletions src/cdomain/value/cdomains/intDomain.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1898,21 +1898,21 @@ struct
let cast_to ?torg ?no_ov ik = function
| `Excluded (s,r) ->
let r' = size ik in
if R.leq r r' then (* upcast -> no change *)
`Excluded (s, r)
else if ik = IBool then (* downcast to bool *)
if S.mem Z.zero s then
`Definite Z.one
else
`Excluded (S.empty(), r')
if R.leq r r' then (* upcast -> no change *)
`Excluded (s, r)
else if ik = IBool then (* downcast to bool *)
if S.mem Z.zero s then
`Definite Z.one
else
(* downcast: may overflow *)
(* let s' = S.map (Size.cast ik) s in *)
(* We want to filter out all i in s' where (t)x with x in r could be i. *)
(* Since this is hard to compute, we just keep all i in s' which overflowed, since those are safe - all i which did not overflow may now be possible due to overflow of r. *)
(* S.diff s' s, r' *)
(* The above is needed for test 21/03, but not sound! See example https://github.com/goblint/analyzer/pull/95#discussion_r483023140 *)
`Excluded (S.empty (), r')
`Excluded (S.empty(), r')
else
(* downcast: may overflow *)
(* let s' = S.map (Size.cast ik) s in *)
(* We want to filter out all i in s' where (t)x with x in r could be i. *)
(* Since this is hard to compute, we just keep all i in s' which overflowed, since those are safe - all i which did not overflow may now be possible due to overflow of r. *)
(* S.diff s' s, r' *)
(* The above is needed for test 21/03, but not sound! See example https://github.com/goblint/analyzer/pull/95#discussion_r483023140 *)
`Excluded (S.empty (), r')
| `Definite x -> `Definite (Size.cast ik x)
| `Bot -> `Bot

Expand Down
2 changes: 1 addition & 1 deletion src/cdomain/value/cdomains/intDomain.mli
Original file line number Diff line number Diff line change
Expand Up @@ -232,7 +232,7 @@ sig
val invariant: Cil.exp -> t -> Invariant.t
end
(** Interface of IntDomain implementations that do not take ikinds for arithmetic operations yet.
TODO: Should be ported to S in the future. *)
TODO: Should be ported to S in the future. *)

module type S =
sig
Expand Down
Loading

0 comments on commit c3e2cc8

Please sign in to comment.