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 vs Ada/SPARK

Hello and welcome,

> I am not very familiar with either Frama-C or Ada/SPARK.
> I am wondering whether anyone in the list would be able
> to comment on how they compare against each other.
> It seems as though Frama-C has a stronger focus on mathematic
> proofs whereas SPARK is more like an static analyzer.

This is not going to be a definitive answer because I
am less familiar with SPARK than Frama-C.

I do not quite agree with this characterization of Frama-C,
unless by "static analyzer" you mean a tool to enforce 
coding rules, which indeed no provided Frama-C plug-in 
does (someone could still write their own plug-in to
enforce coding rules, and in fact some people have,
for their own needs), or a heuristic bug-finding tool,
something we have not focused on given the already
healthy existing microcosm of tools that do that for
the C language.

There is in principle nothing that prevents any static 
analysis applicable to C to be implemented as a plug-in,
although those we provide for now are the Value Analysis,
and plug-ins that exploit its results, with the limitations
this implies.

On the other hand, if I understand correctly what I have
been told by someone from Praxis, SPARK relies on
deductive techniques too.

So the bottom line is that they are very similar.
SPARK/Ada is an older, more mature framework,
and it defines its own subset of Ada
that it works with. Frama-C uses C, which
is not as well defined as Ada in the first place
(the standard is weak because it has to retrofit all the
existing compilers, so embedded developers often have to
rely on behaviors of their compiler that are not mandated
by the standard, and to make things worse some compiler
developers are actively trying to break these embedded
developers' programs). Frama-C does not define a common
subset of C, although each plug-in can of course refuse
to handle this or that difficult C construct. We will soon have
some very impressive demos of C programs with difficult
constructs being verified in a collaborative approach where
the participating plug-ins help each other navigate around
the analyzed program's difficulties.

Hope this helps,

Pascal