Skip to content

CBMC stops analysis with "pointer handling for concurrency is unsound" error with Address Assignment. #8714

@dc-nagai

Description

@dc-nagai

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?

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions