--- layout: fc_discuss_archives title: Message 47 from Frama-C-discuss on June 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama-C



Hello,

the "Frama" in the name "Frama-C" comes from "framework", and is a
reference to the modular architecture, with analysis plug-ins
organized around a common kernel and exchanging information with each
other about the analyzed program.

You can get an idea what the architecture will look like when it is
completed from what is in the current version, but it is not finished
yet. Examples of what is already there are:

- when you use Frama-C's slicer, various preliminary analyses that are
necessary are automatically launched in the right order so that it
just works.

- the value analysis, that emits alarms and accepts user annotations
as part of its work, emits alarms in ACSL and accepts user annotations
in ACSL so that it is possible to check the validity of these alarms
or assumptions with another verification plug-in based on ACSL, such
as Jessie.

Pascal