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