Skip to content

Commit 3176a21

Browse files
committed
Add test cases for division of a large number
1 parent 6d5af0b commit 3176a21

File tree

2 files changed

+41
-0
lines changed

2 files changed

+41
-0
lines changed
Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
//PARAM: --enable ana.int.interval --disable ana.int.def_exc
2+
#include <assert.h>
3+
4+
int main(){
5+
// 2^33
6+
long long x = 8589934592l;
7+
// 2^31 - 1
8+
long long y = 2147483647;
9+
10+
long long z = x/y;
11+
12+
if(z == 4){
13+
// Should be reachable
14+
assert(1);
15+
}
16+
17+
assert(z > 2); //UNKNOWN
18+
}
Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
//PARAM: --enable ana.int.interval --enable ana.int.def_exc
2+
#include <assert.h>
3+
4+
int main(){
5+
int top;
6+
// 2^33
7+
long long x = 8589934592l;
8+
// 2^31 - 1
9+
long long y = 2147483647;
10+
11+
if(top) {
12+
x = x - 1;
13+
}
14+
15+
long long z = x/y;
16+
17+
if(z == 4){
18+
// Should be reachable
19+
assert(1);
20+
}
21+
22+
assert(z > 2); //UNKNOWN
23+
}

0 commit comments

Comments
 (0)