--- layout: fc_discuss_archives title: Message 109 from Frama-C-discuss on March 2009 ---
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. > >