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


FLATA-C is distributed freely, under LGPL public license.

 Download and Installation


  • 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 >


Attached documents

Flata-c front en plugin

17 September 2012
info document : TGZ
7.1 MiB

This archive contains the frama-c plugin source that allows to extract numerical transition system based models of C-language programs.