I encountered an issue where CBMC outputs an error and stops analysis when performing pointer operations.
When I run CBMC (versions 6.7.1 and 5.9.5) on the following sample code:
static unsigned char *testptr;
void func(void) {
unsigned char u1data = 0;
testptr = &u1data;
}
CBMC command:
・cbmc --unwind 1 --flush --partial-loops --object-bits 8 --conversion-check --unsigned-overflow-check --trace --xml-ui xxx.goto
・cbmc --unwind 1 --flush --partial-loops --object-bits 8 --cover location --xml-ui xxx.goto
CBMC outputs the following error message and terminates the analysis:
pointer handling for concurrency is unsound
Is it possible to improve CBMC so that the analysis does not stop in this case?
Alternatively, is there any option or workaround to force CBMC to continue the analysis despite this warning?