Skip to content
This repository was archived by the owner on Oct 3, 2021. It is now read-only.

Commit 9166aa3

Browse files
Added a few more type casts to avoid overflow in llvm IR
Can be reverted with same reason as the previous commit.
1 parent 0794c45 commit 9166aa3

File tree

2 files changed

+11
-5
lines changed

2 files changed

+11
-5
lines changed

c/nla-digbench/bresenham-ll.c

Lines changed: 9 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -20,28 +20,32 @@ void __VERIFIER_assert(int cond) {
2020

2121
int main() {
2222
int X, Y;
23-
long long x, y, v;
23+
long long x, y, v, xy, yx;
2424
X = __VERIFIER_nondet_int();
2525
Y = __VERIFIER_nondet_int();
2626
v = ((long long) 2 * Y) - X; // cast required to avoid int overflow
2727
y = 0;
2828
x = 0;
2929

3030
while (1) {
31-
__VERIFIER_assert( 2*Y*x - 2*X*y - X + (long long) 2*Y - v == 0);
31+
yx = (long long) Y*x;
32+
xy = (long long) X*y;
33+
__VERIFIER_assert( 2*yx - 2*xy - X + (long long) 2*Y - v == 0);
3234
if (!(x <= X))
3335
break;
3436
// out[x] = y
3537

3638
if (v < 0) {
37-
v = v + 2 * Y;
39+
v = v + (long long) 2 * Y;
3840
} else {
39-
v = v + 2 * (Y - X);
41+
v = v + 2 * ((long long) Y - X);
4042
y++;
4143
}
4244
x++;
4345
}
44-
__VERIFIER_assert(2*Y*x - 2*x*y - X + (long long) 2*Y - v + 2*y == 0);
46+
xy = (long long) x*y;
47+
yx = (long long) Y*x;
48+
__VERIFIER_assert(2*yx - 2*xy - X + (long long) 2*Y - v + 2*y == 0);
4549

4650
return 0;
4751
}

c/nla-digbench/egcd2-ll.c

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -33,6 +33,8 @@ int main() {
3333
k = 0;
3434
xy = (long long) x * y;
3535
yy = (long long) y * y;
36+
assume_abort_if_not(xy < 2147483647);
37+
assume_abort_if_not(yy < 2147483647);
3638

3739
while (1) {
3840
if (!(b != 0))

0 commit comments

Comments
 (0)