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] How to use ACSL in GUI and How to generate Coqcode

Hello,

> 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.

ACSL is not a plug-in, it is the common language of all
Frama-C plug-ins that try to provide assistance in verifying
functional properties. You did not say which plug-in you
were trying to use.

For non-Jessie plug-ins (that would be the value analysis
at the moment, with all its limitations when it come to the
verification of functional properties):

It is possible to put in ACSL assertions in the GUI by selecting a
statement, right-click and selecting one of the "add assert..."
actions in the contextual menu.

The display of ACSL properties' status in the GUI is one of the
features that you can expect in the next Frama-C release,
whenever that is.

For Jessie:

Jessie has its own user interface. The GUI that opens when you
follow the tutorial is Gwhy. It does not allow to manipulate
ACSL properties. The way to use it is to observe, think, and
then go modify the ACSL annotations (say, add a loop invariant)
in the analyzed files using your favorite text editor.

> The frama-c
> cmd does not seem to have such options either. How can users know if
> the specification written by ACSL is correct? 

For Jessie: because Gwhy says all proof obligations have been discharged.

For the value analysis in the current version: because the
generated logs never say that a property has "status unknown" or
"false".

For the value analysis in the next version: by looking at the summary in
the GUI.

> Do we have a tutorial
> about how to use ACSL with frama-c or  frama-c-gui?

There is a tutorial for Jessie:
http://frama-c.cea.fr/jessie_tutorial_index.html

The value analysis' tutorial does not emphasize the interpretation
of ACSL properties, which are not the primary goal of this plug-in.

> 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.

I am not sure "include" is the right word. You could say Frama-C
"includes" Why, considering the traffic on this list today,
and even that would not be completely accurate.

> For example, it can generate Coq code to let users do interactive proof
> for tricky properties. Does Frama-C also support this? 

Yes. The technically accurate statement is that Frama-C can
integrate the external Jessie plug-in, Jessie interfaces with Why,
and Why *is* the multi-prover back-end that allows Caduceus
to target different provers. Jessie can do the same thing
Caduceus did, because it also uses Why.

> How can users
> generate Coq proofs from ACSL?

Figure 1.1 in Jessie's tutorial, and section 1.1 around it, should begin to
answer your question.

Best regards,

Pascal