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] The Capabilities of Frama-C

  • Subject: [Frama-c-discuss] The Capabilities of Frama-C
  • From: vadim.tsesko at gmail.com (Vadim TSES'KO)
  • Date: Sun, 12 Apr 2009 18:33:08 +0400
Hi, everybody!

I represent a team of researchers and we are considering using Frama-C 
framework for building C/C++ static analysis tool.

I couldn't find any specific information about the capabilities of 
Frama-C and digging into the source code is rather time consuming.

Could you please answer some questions or redirect me to appropriate 
sources of information.

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

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

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

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

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

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

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

In my humble opinion, this information would be very useful on official 
website.

Thank you for your attention,

Vadim TSES'KO