Running goto-cc followed by cbmc with different values for --object-bits only causes a warning.

[thomasspriggs]

Running goto-cc followed by cbmc with different values for --object-bits only causes a warning. This should really be an error rather than a warning. This option was added to goto-cc as part of this PR - #5440 , in order to address issue - #5272
Example -

$ goto-cc --object-bits 6 ./temp_main.c -o ./temp_main.gb
$ goto-cc --object-bits 10 ./temp_func.c -o ./temp_func.gb
$ cbmc ./temp_func.gb ./temp_main.gb
CBMC version 5.12 (cbmc-5.12.4-9-gdae95d970-dirty) 64-bit x86_64 linux
Reading GOTO program from file
Reading: ./temp_func.gb
Reading GOTO program from file
Reading: ./temp_main.gb
file <built-in-additions> line 24: warning: conflicting initializers for variable "__CPROVER_max_malloc_size"
using old value in module temp_func file <built-in-additions> line 24
9007199254740992ul
ignoring new value in module temp_main file <built-in-additions> line 24
144115188075855872ul
Generating GOTO Program
Adding CPROVER library (x86_64)
file <built-in-additions> line 24: warning: conflicting initializers for variable "__CPROVER_max_malloc_size"
using old value in module temp_func file <built-in-additions> line 24
9007199254740992ul
ignoring new value in module <built-in-library> file <built-in-additions> line 24
36028797018963968ul
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking

[hannes-steffenhagen-diffblue]

I’m closing this issue because rather than printing a warning we should remove the --object-bits option from goto-cc.

[thomasspriggs]

So where is the ticket/issue for removing the --object-bits option from goto-cc? Are you certain that this kind of linker issue should only be a warning rather than an error?