Predicate Abstaction using SAT

Supported ANSI-C Language Features

SATABS 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	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	`SATABS` allows all compound operators
Function calls	Supported by inlining. The locality of parameters and non-static local variables is preserved.	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 currently not supported
Pointers	Dereferencing	When a pointer is dereferenced, `SATABS` checks that the object pointed to is still alive. If the object is an array, the array bounds are checked.
	Pointer arithmetic
	Relational operators on pointers	`SATABS` checks that the two operands point to the same object.
	Pointer Type Casts	A memory model permits machine-specific pointer type casts.
	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. `SATABS` can check that all dynamically allocated memory is deallocated before exiting the program (''memory leaks'').
Concurrency	`pthread_create` and `pthread_mutex_*` are supported. `SATABS` searches all possible interleavings exhaustively. Together with Boppo, unbounded thread creation is permitted.