Skip to content

Commit e2a74e7

Browse files
committed
Fix 01-cpa/60-def_exc-int128
1 parent 1452a93 commit e2a74e7

File tree

2 files changed

+2
-2
lines changed

2 files changed

+2
-2
lines changed

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -81,7 +81,7 @@ struct
8181
let name () = "def_exc"
8282

8383

84-
let top_range = R.of_interval range_ikind (-99L, 99L) (* Since there is no top ikind we use a range that includes both ILongLong [-63,63] and IULongLong [0,64]. Only needed for intermediate range computation on longs. Correct range is set by cast. *)
84+
let top_range = R.of_interval range_ikind (-999L, 999L) (* Since there is no top ikind we use a range that includes both IInt128 [-127,127] and IUInt128 [0,128]. Only needed for intermediate range computation on longs. Correct range is set by cast. *)
8585
let top_overflow () = `Excluded (S.empty (), top_range)
8686
let bot () = `Bot
8787
let top_of ik = `Excluded (S.empty (), size ik)

tests/regression/01-cpa/60-def_exc-int128.c

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,6 @@ __int128 int128max = ((__int128) LLONG_MAX) << 64 | ULLONG_MAX;
77
int main() {
88
__int128 x, y, z;
99
z = x + y;
10-
__goblint_check(z < int128max); // TODO UNKNOWN!
10+
__goblint_check(z < int128max); // UNKNOWN!
1111
return 0;
1212
}

0 commit comments

Comments
 (0)