FLATA-C is static-analysis front-end, implemented as a FRAMA-C plugin, that aims at extracting Numerical Transition System models from C programs with low-level pointer updates such as e.g.: allocation, deletion, pointer arithmetic, etc. The generated NTS models can be used with off-the-shelf verifiers such as FLATA or ELDARICA.
We target the following types of errors in the C code:
- null or dangling pointer dereferencing
- unaligned memory accesses
- memory leaks
- double free
- out-of-bound memory accesses
Distribution
FLATA-C is distributed freely, under LGPL public license.
Download and Installation
Prerequisites:
- Download and install Frama-C version nitrogen first
- Download the flata-c tar archive, unpack it and read the instructions detailes on the README file.
FLATA-C is invoked as follows: frama-c -flatac < file_name.c >
Contributors
- Radu Iosif
- Florent Garnier
