diff --git a/regression/cbmc/Malloc23/test.desc b/regression/cbmc/Malloc23/test.desc index 9e34fa7f42..4bd6cbdc14 100644 --- a/regression/cbmc/Malloc23/test.desc +++ b/regression/cbmc/Malloc23/test.desc @@ -5,8 +5,8 @@ main.c ^SIGNAL=0$ pointer outside dynamic object bounds in \*p: FAILURE pointer outside dynamic object bounds in \*p: FAILURE -pointer outside dynamic object bounds in p2\[\(signed long int\)1\]: FAILURE -pointer outside dynamic object bounds in p2\[\(signed long int\)0\]: FAILURE +pointer outside dynamic object bounds in p2\[.*1\]: FAILURE +pointer outside dynamic object bounds in p2\[.*0\]: FAILURE \*\* 4 of 36 failed \(3 iterations\) -- ^warning: ignoring diff --git a/regression/cbmc/byte_update2/main.c b/regression/cbmc/byte_update2/main.c index 12493e4267..cee6e19ecc 100644 --- a/regression/cbmc/byte_update2/main.c +++ b/regression/cbmc/byte_update2/main.c @@ -6,7 +6,7 @@ int main(int argc, char** argv) { if(argc != 2) return 0; - unsigned long x[argc]; + unsigned long long x[argc]; x[0]=0x0102030405060708; x[1]=0x1112131415161718; diff --git a/regression/cbmc/byte_update3/main.c b/regression/cbmc/byte_update3/main.c index 6d9b3c293c..e20eb6588c 100644 --- a/regression/cbmc/byte_update3/main.c +++ b/regression/cbmc/byte_update3/main.c @@ -13,7 +13,7 @@ int main(int argc, char** argv) { x[3]=0x0708; x[4]=0x090a; - unsigned long* alias=(unsigned long*)(((char*)x)+0); + unsigned long long* alias=(unsigned long long*)(((char*)x)+0); *alias=0xf1f2f3f4f5f6f7f8; unsigned char* alias2=(unsigned char*)x; diff --git a/regression/cbmc/byte_update4/main.c b/regression/cbmc/byte_update4/main.c index 0285f3058f..2866b20a0f 100644 --- a/regression/cbmc/byte_update4/main.c +++ b/regression/cbmc/byte_update4/main.c @@ -18,7 +18,7 @@ int main(int argc, char** argv) { x[8]=0x09; x[9]=0x0a; - unsigned long* alias=(unsigned long*)(((char*)x)+1); + unsigned long long* alias=(unsigned long long*)(((char*)x)+1); *alias=0xf1f2f3f4f5f6f7f8; unsigned char* alias2=(unsigned char*)x; diff --git a/regression/cbmc/byte_update5/main.c b/regression/cbmc/byte_update5/main.c index e2f9da4def..fc698a2014 100644 --- a/regression/cbmc/byte_update5/main.c +++ b/regression/cbmc/byte_update5/main.c @@ -13,7 +13,7 @@ int main(int argc, char** argv) { x[3]=0x0708; x[4]=0x090a; - unsigned long* alias=(unsigned long*)(((char*)x)+1); + unsigned long long* alias=(unsigned long long*)(((char*)x)+1); *alias=0xf1f2f3f4f5f6f7f8; unsigned char* alias2=(unsigned char*)x; diff --git a/regression/cbmc/byte_update6/main.c b/regression/cbmc/byte_update6/main.c index cb92364572..d0e3680b83 100644 --- a/regression/cbmc/byte_update6/main.c +++ b/regression/cbmc/byte_update6/main.c @@ -6,7 +6,7 @@ int main(int argc, char** argv) { if(argc != 2) return 0; - unsigned long x[argc]; + unsigned long long x[argc]; x[0]=0x0102030405060708; x[1]=0x1112131415161718; diff --git a/regression/cbmc/byte_update7/main.c b/regression/cbmc/byte_update7/main.c index 599df60afd..35690acc90 100644 --- a/regression/cbmc/byte_update7/main.c +++ b/regression/cbmc/byte_update7/main.c @@ -6,7 +6,7 @@ int main(int argc, char** argv) { if(argc != 2) return 0; - unsigned long x[argc]; + unsigned long long x[argc]; x[0]=0x0102030405060708; x[1]=0x1112131415161718;