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] Extra features in ACSL in Frama-C versus Caduceus?
- Subject: [Frama-c-discuss] Extra features in ACSL in Frama-C versus Caduceus?
- From: yannick.moy at gmail.com (Yannick Moy)
- Date: Mon Oct 6 12:38:53 2008
- In-reply-to: <firstname.lastname@example.org>
- References: <email@example.com>
Hi, Sorry we did not answer to this message before. I'm rephrasing the questions below and I provide short answers, please anybody, feel free to complete: 1) What is the difference between Caduceus annotation language and ACSL? ACSL is strongly inspired from Caduceus annotation language, which is itself strongly inspired from JML. ACSL is meant to be independent from a specific tool, technique or memory model, while Caduceus annotation language is strongly tied to deductive verification and the component-as-array memory model (aka Burstall-Bornat memory model), where pointer casts and unions are not allowed. ACSL only relies on what the C standard guarantees, and its aim is to allow expressing any safety property (not progress properties) on a C program. E.g., it is possible to have casts in ACSL annotations, sets of terms, sets expressed in comprehension notation, etc. 2) What is the difference between Frama-C and Caduceus? Frama-C is a platform that allows many techniques to be applied to analyse a C program. We are increasingly combining analyses (plugins), so that in the end you should be able to prove many properties by abstract interpretation, slice the program for the remaining properties and prove them by deductive verification inside Why, all automatically. Frama-C aims at supporting all of C, which it does already, while plugins have their own limitations. The Jessie plugin is the one that translates C programs into an intermediate language inside the Why platform, so that Frama-C can be used to perform deductive verification in the same way as Caduceus. We just started to support casts and unions for experiments, but we have not released this part yet. It should be the case ultimately that constructs not supported in Caduceus are supported in this Jessie plugin. Of course, we strongly encourage all users of Caduceus to switch to Frama-C, which should consist mostly in adding semicolons at the end of every clause in annotations ... Cheers, Yannick On Wed, Sep 17, 2008 at 2:36 PM, Alan Dunn <firstname.lastname@example.org> wrote: > I'm relatively new to using Frama-C and Caduceus, so I was wondering > if someone could explain what extra capabilities ACSL has that > Caduceus's specification language does not? Was the main idea of ACSL > that slight improvements could be made to Caduceus's specification > language since the entire Frama-C framework was being introduced at > that point anyway, or was there some other additional goal in the ACSL > specification language design? (Furthermore, is the goal with ACSL to > eventually add a number of features that Caduceus does not have? It's > difficult to glean the answer to these questions from the > documentation.) > > - Alan > > _______________________________________________ > Frama-c-discuss mailing list > Framaemail@example.com > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > -- Yannick -------------- next part -------------- An HTML attachment was scrubbed... URL: http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20081006/ae94f3ce/attachment.htm
- Next by Date: [Frama-c-discuss] Compiling the gui with gtkSourceView 2.0
- Next by thread: [Frama-c-discuss] Compiling the gui with gtkSourceView 2.0