Frama-C-discuss mailing list archives

yannick.moy at gmail.com (Yannick Moy) · Mon Oct 6 12:38:53 2008

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 <amdunn@gmail.com> 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
> Frama-c-discuss@lists.gforge.inria.fr
> 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

Frama-C-discuss mailing list archives

[Frama-c-discuss] Extra features in ACSL in Frama-C versus Caduceus?