FLATA-C is static-analysis front-end, implemented as a plugin, that aims at extracting 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 or .
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 public license.
Download and Installation
Prerequisites:
- Download and install 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
Contributors
- Florent Garnier
