--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on July 2011 ---
Hello, Le 01/07/2011 11:12, ??? a ?crit : > It's powerful for analysis with ACSL annotations but I cannot find how > to interpret the ACSL annotations and in the development-guide only > a little information is given. So could you show me the way to deal with > ACSL annotations or show me a simple example? What do you mean by "interpret"? If you want to check the validity of an ACSL annotation, then the module Properties_status is up to you. If you want to handle them yourself in your plug-in, then I'm afraid that you have to do the job by yourself. That is what each plug-in which emits a property status (valid/invalid/unknown) does. For such plug-ins, it is even the biggest part of their job. Best regards, Julien Signoles -- Researcher-engineer CEA LIST, Software Safety Labs 91191 Gif-Sur-Yvette Cedex tel:(+33)1.69.08.71.82 fax:(+33)1.69.08.83.95 Julien.Signoles at cea.fr