--- layout: fc_discuss_archives title: Message 26 from Frama-C-discuss on December 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] How to use ACSL in GUI and How to generate Coq code



Hi,

I was using ACSL in frama-c-gui. The features provided by GUI are
about slicing, value analysis, dependency analysis and other
static analysis options. I cannot find options for ACSL. The frama-c
cmd does not seem to have such options either. How can users know if
the specification written by ACSL is correct? Do we have a tutorial
about how to use ACSL with frama-c or  frama-c-gui?

The other question is about proof backend support. Frama-C includes
Caduceus http://why.lri.fr/caduceus/. Caduceus supports
different backend from automatic provers and proof assistents. For
example, it can generate Coq code to let users do interactive proof
for tricky properties. Does Frama-C also support this? How can users
generate Coq proofs from ACSL?

Thanks.
Jianzhou