--- layout: fc_discuss_archives title: Message 28 from Frama-C-discuss on December 2009 ---
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 >