Description
After having a look at src/util/config.cpp and playing around with the options a little bit, it seems that the best way to set the target architecture for CBMC is with --arch and to never use --32, --64, --LP64 etc. because --arch sets not only the appropriate type widths but more than that.
For example, if I run cbmc --32 on a 64-bit Linux it will output Adding CPROVER library (x86_64) which seems undesired if I want to verify a 32-bit program. With --arch i386 it outputs Adding CPROVER library (i386).
Is this understanding correct?
If yes, I suggest to clarify this in the documentation. When looking at the output of --help or at the man page, there is not only no discussion of the difference between --arch i386 and --32, the latter also comes first and is thus most likely picked up by users (--arch is explained only several lines below between less relevant options). Options like --32 should be marked as not recommended.
If my understanding is incorrect, it might also be nice to explain in the documentation that there is no difference, and fix the misleading log output.
Additionally, in the source code the options --16/--32/--64 seem to be identical to --LP32/--ILP32/--(L)LP64 and thus do set widths of all relevant types. However, the help output claims that the former only sets widths of ints in contrast to the latter, which also set widths of pointers. So here the documentation should also be fixed.
CBMC version: 5.12
Operating system: Linux x86_64