Supported Language Features
|
Supported Language Features
|
CBMC supports the
following ANSI-C language features.
| Supported Language Features | Properties checked | |
|---|---|---|
| Basic Data Types | All standard scalar data types custom fixed-width integers, fixed-point numbers and floating-point numbers. |
|
| 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 Overflow for unsigned data types |
| Type casts | All type casts, including conversion between integer and floating-point types. | Overflow for signed data types Overflow for unsigned data types |
| Side effects | CBMC allows all compound operators |
|
| Function calls | The locality of
parameters and non-static local variables is preserved. CBMC supports ANSI-C prototypes and K&R-style functions. |
Unwinding bound for recursive functions by means of an unwinding assertion |
| Control flow statements |
goto, return, break,
continue, switch
(''fall-through'' is supported), while
|
|
| Non-Determinism | User-input is modeled by means of non-deterministic choice functions | |
| Assumptions and Assertions |
Standard ANSI-C expressions are allowed as assertions; in addition, Spec#-style quantifiers are supported. | 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 and anonymous union members | |
| 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''). |
CBMC supports the
following C++ language features.
| Supported Language Features | Properties checked | |
|---|---|---|
| Classes | methods, multiple and virtual inheritance, virtual methods, access control, constructors and destructors | |
| Dynamic object creation | with new and deletetemporary objects |
|
| Overloading | function overloading, operator overloading | |
| Templates | Templates with type and scalar arguments | |
| STL | std::map, std::list, std::vector | Correct use of iterators, non-emptiness preconditions |