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

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
>