Closed
Description
In the partial order concurrency encoding cbmc currently assumes that stack memory is not shared. This seems to be a reasonable assumption, but some svcomp benchmarks make use of this:
sv-benchmarks/c/ldv-races/race-2_2-container_of_false-unreach-call.c
sv-benchmarks/c/ldv-races/race-2_3-container_of_false-unreach-call.c
sv-benchmarks/c/ldv-races/race-2_4-container_of_false-unreach-call.c
sv-benchmarks/c/ldv-races/race-2_5-container_of_false-unreach-call.c
sv-benchmarks/c/ldv-races/race-3_2-container_of-global_false-unreach-call.c
For a distilled example see regression/cbmc-concurrency/stack1 in #303.
Metadata
Metadata
Assignees
Labels
No labels