implementation-defined aspects

[pmo]

In  the C standard (C90/C99), type int is by default signed. except for a bitfield where the sign  becomes  implementation defined. With gcc, a bitfield of type int is by default signed like other variables of type int but this can be changed with the option -funsigned-bitfiled. With some other compilators,  bitfield are, by default, unsigned. 

From this observation, I am wondering how to specify this kind of implementation-defined aspects to CBMC ?

Thanks  

[Martin Nyx Brain]

CBMC has a series of options for specifying the OS and architecture,
which then control these implementation defined aspects. By default it
will try to match the platform it is run on. The flags --arch and --os
are the key ones but there are also things like --16, --32, --64, --
LP64, etc. --little-endian, --big-endian and --unsigned-char which
over-ride the arch and OS setting.

util/config.cpp contains most of the code that handles this, if there
are specific architecture(s) that you want supported let us know and
send some test cases. For deeper "platform dependent behaviour" it ma
be possible to support it but we'd need a patch or a use-case.

HTH

Cheers,
- Martin