Skip to content

Commit fd0c611

Browse files
authored
Merge pull request #1742 from goblint/intdomain-top_typ
Remove `IntDomain.Size.top_typ`
2 parents 0598ab3 + 4bb4437 commit fd0c611

File tree

3 files changed

+2
-5
lines changed

3 files changed

+2
-5
lines changed

src/cdomain/value/cdomains/intDomain0.ml

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -233,7 +233,6 @@ module Size = struct (* size in bits as int, range as int64 *)
233233
open Cil
234234
let sign x = if Z.compare x Z.zero < 0 then `Signed else `Unsigned
235235

236-
let top_typ = TInt (ILongLong, [])
237236
let min_for x = intKindForValue x (sign x = `Unsigned)
238237
let bit = function (* bits needed for representation *)
239238
| IBool -> 1

src/cdomain/value/cdomains/intDomain_intf.ml

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -387,8 +387,6 @@ sig
387387

388388

389389
module Size : sig
390-
(** The biggest type we support for integers. *)
391-
val top_typ : Cil.typ
392390
val range : Cil.ikind -> Z.t * Z.t
393391
val is_cast_injective : from_type:Cil.typ -> to_type:Cil.typ -> bool
394392
val bits : Cil.ikind -> int * int

src/cdomain/value/cdomains/valueDomain.ml

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -702,7 +702,7 @@ struct
702702
| (x, Top) -> x
703703
| (Int x, Int y) -> Int (ID.meet x y)
704704
| (Float x, Float y) -> Float (FD.meet x y)
705-
| (Int _, Address _) -> meet x (cast (TInt(Cilfacade.ptr_ikind (),[])) y)
705+
| (Int _, Address _) -> meet x (cast !GoblintCil.upointType y)
706706
| (Address x, Int y) -> Address (AD.meet x (AD.of_int y))
707707
| (Address x, Address y) -> Address (AD.meet x y)
708708
| (Struct x, Struct y) -> Struct (Structs.meet x y)
@@ -727,7 +727,7 @@ struct
727727
match (x,y) with
728728
| (Int x, Int y) -> Int (ID.narrow x y)
729729
| (Float x, Float y) -> Float (FD.narrow x y)
730-
| (Int _, Address _) -> narrow x (cast IntDomain.Size.top_typ y)
730+
| (Int _, Address _) -> narrow x (cast !GoblintCil.upointType y)
731731
| (Address x, Int y) -> Address (AD.narrow x (AD.of_int y))
732732
| (Address x, Address y) -> Address (AD.narrow x y)
733733
| (Struct x, Struct y) -> Struct (Structs.narrow x y)

0 commit comments

Comments
 (0)