--- layout: fc_discuss_archives title: Message 28 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 Coqcode



On Wed, Dec 2, 2009 at 2:20 PM, CUOQ Pascal <Pascal.CUOQ at cea.fr> wrote:
> 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.

Thanks. Pascal. I understand the architecture of Frama-c much better now.
I am installing Jessie from
http://frama-c.cea.fr/download/frama-c-Beryllium-20090902-why-2.21.tar.gz.
But I got a syntax error at line 604, file src/kernel/db.ml

(** Detection of the unused code of an application. *)
module Sparecode = struct
  let get =
    ref (fun ~select_annot:_  -> not_yet_implemented "Sparecode.run")
  let rm_unused_globals =
    ref (fun ?project:_ -> not_yet_implemented
"Sparecode.rm_unused_glob")   (*this is line 604*)
end

It seems that ocaml does not like an ignored :_ after an optional
function argument. But I think it is fine to
annotate an argument as 'unused' for an ~ argument.  I tried both
ocaml 3.10.2 and the latest
3.11.1, got the same errors. My linux is SEAS SuSE Linux 11.1, x86_64,
2.6.27.29-0.1-default. Do you
happen to know how I can fix this problem?

Best regards,
Jianzhou

>
> Best regards,
>
> Pascal
>
> _______________________________________________
> Frama-c-discuss mailing list
> Frama-c-discuss at lists.gforge.inria.fr
> http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss
>