DIVINE segfaults when verifying a buggy program
Running ./divine verify try.c
on this program:
int *foo2(void)
{
int arr[100000024];
arr[10000094] = 13;
return arr + 10000094;
}
int *foo(void)
{
int arr[123];
return foo2();
}
int main(void) {
int *a = foo();
printf("%d\n", *a);
return 0;
}
Results in segmentation fault. Some more information from gdb: divine_gdb.txt.