Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • Subject: [Frama-c-discuss] Small function on buffer doesn't verify
  • From: apolkhanov at gmail.com (Alexei Polkhanov)
  • Date: Wed, 12 May 2010 09:33:27 -0700
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>