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
- Subject: [Frama-c-discuss] Frama-C vs Ada/SPARK
- From: Pascal.CUOQ at cea.fr (CUOQ Pascal)
- Date: Wed, 11 Nov 2009 09:30:49 +0100
- References: <416260.32304.qm@web110610.mail.gq1.yahoo.com>
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
- Follow-Ups:
- [Frama-c-discuss] Frama-C vs Ada/SPARK
- From: yannick.moy at gmail.com (Yannick Moy)
- [Frama-c-discuss] Frama-C vs Ada/SPARK
- References:
- [Frama-c-discuss] Frama-C vs Ada/SPARK
- From: hxdg21 at yahoo.com (Aaron Rocha)
- [Frama-c-discuss] Frama-C vs Ada/SPARK
- Prev by Date: [Frama-c-discuss] Res: Feature or bug?
- Next by Date: [Frama-c-discuss] Newbie question
- Previous by thread: [Frama-c-discuss] Frama-C vs Ada/SPARK
- Next by thread: [Frama-c-discuss] Frama-C vs Ada/SPARK
- Index(es):