Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] RE : The Capabilities of Frama-C

  • Subject: [Frama-c-discuss] RE : The Capabilities of Frama-C
  • From: Pascal.CUOQ at cea.fr (CUOQ Pascal)
  • Date: Sun, 12 Apr 2009 17:49:29 +0200
  • References: <49E1FBA4.4060000@gmail.com>
Hi, and thanks for your interest.

>1. What C/C++ standards are supported by the parser being used in 
>Frama-C? (C89, C99, C++ 2003, GNU Extensions, ...)

Frama-C handles most of C99 (as far as I remember, only
the complex type defined in C99 is not handled),
and most of GCC and MSVC extensions.
Work has been done on C++ support but is not available.
The reason is that supporting C++ is a huge amount of work
and that not all C++ constructs are handled yet.

>2. What algorithms are implemented for interval analysis? How precise is 
>the analysis? Are values of dynamic objects taken into consideration?

The value analysis is based on the theoretical framework
of Abstract Interpretation:
http://en.wikipedia.org/wiki/Abstract_interpretation

We find the analysis to be quite precise, and in particular
more precise than what you would get with any other open-source
static analyzer that we know of.
I am not sure I understand the question about
"values of dynamic objects", but if the question is whether
the analyzer can distinguish the different values successively
taken by a variable during the execution, the answer is "yes".

>3. Is there implemented any kind of points-to analysis? Which kind?

The values computed by the value analysis can be adresses
(for instance for the values of pointer variables),
so it directly translates into points-to information.
In the vocabulary that is usual for points-to analyses,
it is path-sensitive, context-sensitive and interprocedural.

>4. How structures and multi-dimensional arrays are supported in 
>implemented analysis types? Is the analysis element- and field-aware?

The value analysis is element-aware and field-aware
(of course for arrays this makes a difference only
when the expression used as an indice can be evaluated
with enough precision. There are a number of settings to
improve precision at the cost of more time and memory use).

In fact, casts between pointers to different structs,
and casts between pointers to structs and pointers to arrays,
are handled with precision too.

>5. Which generic types of analysis are implemented? 
>(Path-sensitive/insensitive, Context-sensitive/insensitive, 
>Inter-procedural/intra-procedural, ...)

CIL, the front-end on which Frama-C is based, provides
generic forward and backward generic dataflow analyses
that can be used for implementing path-sensitive or insensitive,
context-sensitive or insensitive, and inter- or intra-procedural
analyses. The value analysis and other analyses such
as the functional dependencies computation are
implemented using these generic analyses, and the simplest
of these analyses can be used as examples.

>6. Which companies/institutions/research groups/... has used Frama-C 
>framework successfully?

I would feel a little uncomfortable dropping names, so I will let
industrial and academic partners come forward
if they wish to (note that there are hints
about where Frama-C is in use in the archives of this 
very mailing-list).

>7. Has any tests been conducted on real applicability of Frama-C 
>framework? (For instance to analyzing or verifying any commercial or 
>opensource software) 

Again, confidentiality rules prevent us from having all the
details, not to mention giving them to you. We have heard about
projects of tens (or hundreds) of thousands lines of embedded
C code on which the value analysis was providing useful results
in hours (or days) of computations and hundreds of megabytes
(or gigabytes) of memory. Your mileage may vary, it very much
depends on the nature of the code you want to analyze.

A tutorial that will double as a
demonstration of the value analysis' capabilities on
"real" software should be available very soon.

Best regards,

Pascal