--- layout: fc_discuss_archives title: Message 2 from Frama-C-discuss on July 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] how to interpret ACSL annotations?



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