CBMC: Supported Language Features

Supported Language Features

CBMC supports the following ANSI-C language features. A more detailed description with examples is available in the manual.

Supported Language Features		Properties checked
Basic Data Types	All scalar data types `float` and `double` using fixed-point arithmetic. The bit-width can be adjusted using a command line option.
Integer Operators	All integer operators, including division and bit-wise operators Only the basic floating-point operators are supported.	Division by zero Overflow for signed data types
Type casts	All type casts, including conversion between integer and floating-point types	Overflow for signed data types
Side effects	`CBMC` allows all compound operators	Side effects are checked not to affect variables that are evaluated elsewhere, and thus, that the ordering of evaluation does not affect the result.
Function calls	Supported by inlining. The locality of parameters and non-static local variables is preserved. CBMC supports ANSI-C prototyles and K&R style functions.	Unwinding bound for recursive functions Functions with a non-void return type must return a value by means of the `return` statement.
Control flow statements	`goto`, `return`, `break`, `continue`, `switch` (''fall-through'' is supported)
Non-Determinism	User-input is modeled by means of non-deterministic choice functions
Assumptions and Assertions	Only standard ANSI-C expressions are allowed as assertions.	Assertions are verified to be true for all possible non-deterministic choices given that any assumption executed prior to the assertion is true.
Arrays	Multi-dimensional arrays and dynamically-sized arrays are supported	Lower and upper bound of arrays, even for arrays with dynamic size
Structures	Arbitrary, nested structure types; may be recursive by means of pointers; incomplete arrays as last element of structure are allowed
Unions	Support for named unions, anonymous union members are supported	`CBMC` checks that unions are not used for type conversion, i.e., that the member used for reading is the same as used for writing last time.
Pointers	Dereferencing	When a pointer is dereferenced, `CBMC` checks that the object pointed to is still alive and of compatible type. If the object is an array, the array bounds are checked.
	Pointer arithmetic
	Relational operators on pointers	`CBMC` checks that the two operands point to the same object.
	Pointer Type Casts	Upon dereferencing, the type of the object and the expression are checked to be compatible. Byte-wise access to numerical data is supported.
	Pointers to Functions	The offset within the object is checked to be zero
Dynamic Memory	`malloc` and `free` are supported. The argument of malloc may be a nondeterministically chosen, arbitrarily large value.	Upon dereferencing, the object pointed to must still be alive. The pointer passed to `free` is checked to point to an object that is still alive. `CBMC` can check that all dynamically allocated memory is deallocated before exiting the program (''memory leaks'').