Skip to content

fc estimate difficulty

Jump to bottom
Andre Maroneze edited this page Apr 12, 2022 · 2 revisions

fc-estimate-difficulty: a tool for estimating the difficulty of analyzing some source code with Frama-C

This page provides binaries for the command-line tool fc-estimate-difficulty. Run it as:

./fc-estimate-difficulty [paths]

Where paths is one or several files or directories containing C code.

The tool will evaluate the code (heuristically) and try to identify features that could complicate an analysis with Frama-C, such as:

  • inclusion of non-POSIX headers (e.g. third-party libraries such as X11, OpenSSH, etc);
  • presence of recursion (for plug-ins such as Eva);
  • unsupported or hard-to-analyze standard library functions and headers (e.g. complex.h, setjmp);
  • non-portable features such as inline assembly (asm(...));
  • dynamic memory allocation (e.g. calls to malloc, realloc, free);
  • C library functions for which the Frama-C standard library does not yet provide ACSL specifications.

This tool is targeted towards users who have not yet installed Frama-C, but would like to obtain a quick (despite imprecise) estimation of whether their code base is likely to be easily analyzed by Frama-C. The tool outputs a series of warnings (whenever a "hard" feature is found) and a score at the end, which summarizes how many "difficulties" were found. An "ideal" analysis should obtain 0 in all categories.

Note that the estimation is, above all, an estimation: analyses can be simple even when several difficulties were detected, and vice-versa.

Already included in Frama-C, via frama-c-script estimate-difficulty

If you already have Frama-C installed, this tool is redundant: you can simply fun frama-c-script estimate-difficulty <paths> to obtain the same result. This tool is distributed in this form simply to help those who do not have Frama-C installed.

How it works

In order to make this tool easy to use (no installation required), it is almost entirely written in Python and compiled to an executable, thanks to PyInstaller. It also embeds a few C/C++-based extra tools, such as scc and astyle, which help improve precision of the heuristics.

This tool does not parse the source code; instead, it uses some simple regex-based heuristics to obtain a rough estimate of the code's callgraph, and then matches (likely) function names to those defined in POSIX.

In particular, the tool does not preprocess the code, which makes it prone to reporting issues that may be specific to a few architectures or configurations.

Download for Linux, macOS, Windows

There are three binaries available:

  • Linux: 64-bit statically linked binary; no dependencies required
  • macOS: 64-bit mach-O binary (compiled on a Intel Mac, but can run on M1 Macs)
  • Windows : 64-bit command-line executable (to be run on Command Prompt or PowerShell)

The source code is available in the public Frama-C development repository, inside the share/analysis-scripts directory.

Clone this wiki locally