bug in concurrency encoding for arrays and structs

[peterschrammel]

regression tests coming...

[tautschnig]

So what is the bug here - all of the tests are marked "CORE", none is "KNOWNBUG"?

[peterschrammel]

regression/cbmc-concurrency/struct_and_array1 was labelled KNOWNBUG -- I assume that this one is related. One can add another test that dynamically allocates the shared chunk of memory -- doesn't work either.

Side remark: There are currently 150 regression tests marked as KNOWNBUG in the test suite. Maybe we should go through them and dump them all into the issue tracker so that they get eventually resolved. Currently, it is unclear why they are marked as KNOWNBUG (maybe just to silence them, maybe they have been resolved, maybe they are obsolete) or whether anyone is doing something about resolving them.

[kroening]

On the side remark: A systematic approach to the 150 KNOWNBUGs would be super! Please do!

[peterschrammel]

I put it on my list.

[tautschnig]

I do volunteer to sort out the ones in ansi-c. In fact I've just submitted the first PR #131 on those.

[tautschnig]

The ansi-c ones are done as #131, #132, #133, #134.

[peterschrammel]

Also see #184