Skip to content

Commit 1452a93

Browse files
committed
Add test to reveal def_exc unsoundness for __int128
1 parent 1ce9de0 commit 1452a93

File tree

1 file changed

+12
-0
lines changed

1 file changed

+12
-0
lines changed
Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
#include <goblint.h>
2+
#include <limits.h>
3+
4+
// There are no 128bit integer literals...
5+
__int128 int128max = ((__int128) LLONG_MAX) << 64 | ULLONG_MAX;
6+
7+
int main() {
8+
__int128 x, y, z;
9+
z = x + y;
10+
__goblint_check(z < int128max); // TODO UNKNOWN!
11+
return 0;
12+
}

0 commit comments

Comments
 (0)