Platform Dependent Verification

When verifying a program, particularly one written in C or C++, the correctness of the program may depend on specifics of the target platform. For example, there may be pointer arithmetic that assumes an integer takes up 4 bytes, operations on integers may over/underflow, and for bitwise arithmetic we also need to know how big to make the bit vectors. By default, VerCors will make no assumptions which are not guaranteed by the C standard.[^1] The C standard guarantees the following for the sizes of integer types [source]:

Type	Width in bits	Relation
char	exactly 8*	≤ sizeof(short int)
short int	at least 16	≤ sizeof(int)
int	at least 16	≤ sizeof(long int)

long int | at least 32 | ≤ sizeof(long long int)

long long int | at least 64 | -

Note

In VerCors we make the assumption that bytes are 8 bits, since the C standard guarantees that sizeof(char) is equal to 1 this implies that chars are 8 bits

If your code requires stronger guarantees than the C standard provides you will need to set a target using VerCors' --target flag. The target is specified as a target triple in the same syntax used by Clang. (we use Clang to determine the sizes) A reference for this format can be found at llvm.org. Currently we support four data models:

Type	LP32	ILP32	LLP64	LP64
char	8	8	8	8
short int	16	16	16	16
int	16	32	32	32
long int	32	32	32	64

long long int | 64 | 64 | 64 | 64 pointer | 32 | 32 | 64 | 64 Example Target Triple | ppc-lv2-unknown | i686-linux-unknown | x86_64-windows-unknown | x86_64-linux-unknown

Setting the target will cause unsigned integer operations to be guarded with a modulo operation to deal with over- and underflows. To check that signed integers do not over- or underflow (as this is implementation-defined behaviour in C) you can use the --check-integer-bounds flag. Without setting this flag such erroneous over- and underflows will be ignored even if a target is set. Using --check-integer-bounds will also add additional assumptions to function contracts and loop invariants; it cannot be used without setting the target with --target.

Additionally, setting the target may also influence the macros defined by the preprocessor.

[!Note] If you do not specify a target (or set --target unset) then Clang will use the current platform's target to determine which macros to set. In this case VerCors will make no assumptions about the integer size but if your code uses the macros defined by the preprocessor your verification may not be completely portable.