--- layout: fc_discuss_archives title: Message 39 from Frama-C-discuss on May 2010 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Small function on buffer doesn't verify



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>