goto-cc isn't aware of cbmc's --object-bits setting

[karkhaz]

This seems to be a CBMC bug introduced by PR 5210.

The issue exhibits when running the s2n proof for stuffer_resize_if_empty. The command is:

cbmc --verbosity 4  --bounds-check --div-by-zero-check --float-overflow-check --nan-check --pointer-check --pointer-overflow-check --signed-overflow-check --undefined-shift-check --unsigned-overflow-check --unwind 1 --unwinding-assertions  --object-bits 6 --trace /Users/karkhaz/code/s2n/tests/cbmc/proofs/s2n_stuffer_resize_if_empty/gotos/s2n_stuffer_resize_if_empty_harness.goto 2>&1 | tee  logs/cbmc.log; if [ ${PIPESTATUS[0]} -ne 10 ]; then exit ${PIPESTATUS[0]}; fi

which emits this warning:

file <built-in-additions> line 24: warning: conflicting initializers for variable "__CPROVER_max_malloc_size"
using old value in module abort_override_assert_false file <built-in-additions> line 24
8388608ul
ignoring new value in module <built-in-library> file <built-in-additions> line 24
33554432ul

The problem is that we're running CBMC with --object-bits 6, which sets max_malloc_size to 8399608ul (0x800 000). However, when goto-cc built one of the files, it had set max_malloc_size to 33554432ul (0x2 000 000), which is what it would be if object-bits were 8. We can confirm this by running CBMC with --object-bits 10, in which case we see the opposite problem:

file <built-in-additions> line 24: warning: conflicting initializers for variable "__CPROVER_max_malloc_size"
using old value in module abort_override_assert_false file <built-in-additions> line 24
8388608ul
ignoring new value in module <built-in-library> file <built-in-additions> line 24
2097152ul

I will next try to reduce this to a minimal example.

[hannes-steffenhagen-diffblue]

This is internally tracked as ADA-568

[thomasspriggs]

This issue can now be avoided by passing --object-bits to goto-cc. This was done in this PR - #5440