--- layout: fc_discuss_archives title: Message 109 from Frama-C-discuss on March 2009 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Frama-C: #define not taken into account intoannotations



Hello David,

Very good, it works! 
Thank you so much for that hint!

Cheers,
Dillon
 
 

> -----Message d'origine-----
> De : David DELMAS [mailto:david.delmas at airbus.com] 
> Envoy? : mardi 31 mars 2009 10:55
> ? : dillon.pariente at dassault-aviation.fr; Frama-C public discussion
> Objet : Re: [Frama-c-discuss] Frama-C: #define not taken into 
> account intoannotations
> 
> Hi Dillon,
> 
> Le mardi 31 mars 2009 ? 10:36 +0200, Pariente Dillon a ?crit :
> > //===== f.h
> > #define vx 0.0
> >  
> > //===== f.c file
> > #include "f.h"
> > float main(float v) { /*@ assert v<=vx ; */ return v; }
> 
> in this case, can't you just use "frama-c -pp-annot f.c -print" :
> 
> float main(float v )
> {
> 
>   {/*@ assert (v ? 0.0);
> 
>    */
>    ;
>   return (v);}
> 
> }
> 
> 
> The information in this e-mail is confidential. The contents 
> may not be disclosed or used by anyone other then the 
> addressee. Access to this e-mail by anyone else is unauthorised.
> If you are not the intended recipient, please notify Airbus 
> immediately and delete this e-mail.
> Airbus cannot accept any responsibility for the accuracy or 
> completeness of this e-mail as it has been sent over public 
> networks. If you have any concerns over the content of this 
> message or its Accuracy or Integrity, please contact Airbus 
> immediately.
> All outgoing e-mails from Airbus are checked using regularly 
> updated virus scanning software but you should take whatever 
> measures you deem to be appropriate to ensure that this 
> message and any attachments are virus free.
> 
>