Trace production with JSON UI segfaults

[smowton]

This happens in the test-gen-support branch when trying to simplify an index-expression with a pointer-offset expression in the index operand. The cause is a misunderstanding of pointer_offset_exprt here (https://github.com/diffblue/cbmc/blob/test-gen-support/src/goto-programs/json_goto_trace.cpp#L26)-- the transformation simply discarding pointer_offset_exprt(constant) is not correct. Fix coming up.

[smowton]

Fix:
#1066
https://github.com/diffblue/test-gen/pull/617

[carlburgess]

@smowton Is there anything for QA to do here ?

[smowton]

Hmm, I can't immediately find the originally failing test case for this. Perhaps @mgudemann has one?

[carlburgess]

@smowton @mgudemann How do we reproduce the conditions that caused this bug ? Is there an existing test case for this ?

[smowton]

Looks like the test case is added here: https://github.com/diffblue/cbmc/pull/1066/files

[carlburgess]

Fixed

[carlburgess]

@smowton @jgwilson42 I do not have the ability to close this

[jgwilson42]

@sara-db please could you close this?