Skip to content

Commit 078d7f5

Browse files
committed
C2PO tests: avoid undefined behavior (signed overflow) in one test case.
1 parent 1eb6153 commit 078d7f5

File tree

1 file changed

+4
-2
lines changed

1 file changed

+4
-2
lines changed

tests/regression/84-c2po/16-loops.c

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33
#include <goblint.h>
44
#include <stdlib.h>
55

6-
void main(void) {
6+
int main(void) {
77
long y;
88
long i;
99
long *x = malloc(sizeof(long) * 300);
@@ -15,7 +15,7 @@ void main(void) {
1515
y = *x;
1616
z = -1 + x;
1717

18-
while (top) {
18+
while (top > 0) {
1919
z = (long *)malloc(sizeof(long));
2020
x++;
2121
z = -1 + x;
@@ -25,4 +25,6 @@ void main(void) {
2525

2626
__goblint_check(z == -1 + x);
2727
__goblint_check(y == *x2); // UNKNOWN!
28+
29+
return 0;
2830
}

0 commit comments

Comments
 (0)