--- layout: fc_discuss_archives title: Message 39 from Frama-C-discuss on May 2010 ---
I think MACRO is replaced by actual value at pre-processing stage. It is left as is in comment section and this is why when code is finally consumed by frama-c BUFFER_SIZE will be "BUFFER_SIZE" in comments and BUFFER_SIZE in code will be replaced by actual value, let's say "1024". This is at least how I think it to works. --- Alexei Polkhanov Cell: 1.604.719.2515 On Wed, May 12, 2010 at 03:00, < frama-c-discuss-request at lists.gforge.inria.fr> wrote: > Send Frama-c-discuss mailing list submissions to > frama-c-discuss at lists.gforge.inria.fr > > To subscribe or unsubscribe via the World Wide Web, visit > > http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss > or, via email, send a message with subject or body 'help' to > frama-c-discuss-request at lists.gforge.inria.fr > > You can reach the person managing the list at > frama-c-discuss-owner at lists.gforge.inria.fr > > When replying, please edit your Subject line so it is more specific > than "Re: Contents of Frama-c-discuss digest..." > > > Today's Topics: > > 1. Small function on buffer doesn't verify (Boris Hollas) > 2. Re: One-line comments used for multi-line annotations > (Boris Hollas) > > > ---------------------------------------------------------------------- > > Message: 1 > Date: Tue, 11 May 2010 17:21:40 +0200 > From: Boris Hollas <hollas at informatik.htw-dresden.de> > Subject: [Frama-c-discuss] Small function on buffer doesn't verify > To: frama-c-discuss <frama-c-discuss at lists.gforge.inria.fr> > Message-ID: <1273591300.4338.8.camel at iti27> > Content-Type: text/plain; charset="UTF-8" > > Jessie is unable to verify the following code for reasons that I don't > understand. I get "?" for postcondition, pointer dereferencing, > arithmetic overflow. Using #define instead of const doesn't work either > because it seems that Jessie doesn't read #defines. > > > const int BUFF_SIZE = 4; > > /*@ requires \valid(msg+(0..BUFF_SIZE)); > ensures msg[BUFF_SIZE] == '\0'; > */ > int setFoo(char* msg) { > msg[BUFF_SIZE] = '\0'; > msg[BUFF_SIZE-1] = '\0'; > return 0; > } > > > > > > ------------------------------ > > Message: 2 > Date: Tue, 11 May 2010 17:25:56 +0200 > From: Boris Hollas <hollas at informatik.htw-dresden.de> > Subject: Re: [Frama-c-discuss] One-line comments used for multi-line > annotations > To: Frama-C public discussion <frama-c-discuss at lists.gforge.inria.fr> > Message-ID: <1273591556.4338.11.camel at iti27> > Content-Type: text/plain; charset="UTF-8" > > I proposed a change request some months ago for this very > reason. //-style comments are frequently used in C, so this can confuse > users. > > On Mon, 2010-05-10 at 16:36 +0200, Yannick Moy wrote: > > I just realized that you cannot use one-line comments with the @ char > > for multi-line annotations. Was it the case previously, or has it > > always been like that? > > E.g. > > > > //@ predicate even (integer x) = > > //@ x % 2 == 0; > > > > is rejected by Frama-C. > > -- > > Yannick > > _______________________________________________ > > 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 > > > > > > ------------------------------ > > _______________________________________________ > 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 > > End of Frama-c-discuss Digest, Vol 24, Issue 9 > ********************************************** > -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20100512/ab65b696/attachment.htm>