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] Tutorial for using Frama C

  • Subject: [Frama-c-discuss] Tutorial for using Frama C
  • From: pascal.cuoq at gmail.com (Pascal Cuoq)
  • Date: Fri, 27 May 2011 13:05:50 +0200
  • In-reply-to: <BANLkTik9n_kjjwk7UV3G=y7q8z+Rp6P1kg@mail.gmail.com>
  • References: <BANLkTikQxrAwXjMUKgF-v4x=0ZG3TUZr6Q@mail.gmail.com> <BANLkTik9n_kjjwk7UV3G=y7q8z+Rp6P1kg@mail.gmail.com>
Hello,

it appears that the frama-c-discuss at lists.gforge.inria.fr which should have been
the recipient for your e-mail was expanded into a list of e-mail addresses of
subscribers. This seems undesirable, and we should probably take steps so
that it doesn't happen again. If you did something special to get
this result, please explain what you did in a private message
to Benjamin.Monate at cea.fr.

On Fri, May 27, 2011 at 12:23 PM, krishnateja kesineni
<tejakesineni at gmail.com> wrote:

> Somehow, we are not able to get the Software to recognize simple errors like
> double free . use after free , buffer overflow

I should explain that Frama-C's value analysis was designed initially to
be useful for the verification of critical, low-level embedded code.
It does not focus on giving a meaning to standard functions because
these standard functions are not used in this kind of code.
Functions malloc() and free() are only supported in an experimental
fashion.

There are different modelizations of malloc() provided. None is perfect;
this is why there are so many of them.

For buffer overflows in malloc'ed blocks, you can use the
FRAMA_C_MALLOC_INDIVIDUAL modelization:

#define FRAMA_C_MALLOC_INDIVIDUAL

#include "share/malloc.c"

main()
{
  /* out of bounds */
  int *p = malloc(3 * sizeof(int));
  p[4] = 3;
}

frama-c -val test_m.c
...
test_m.c:9:[kernel] warning: out of bounds write. assert \valid(p+4);

In this log message, "assert" indicates a dangerous construct in the
source code. The analyzer cannot guarantee that p+4 is valid at this
line, and (p+4) SHOULD be valid. In fact, the analyzer is sure that
p+4 is not valid, because it says that the executions ends here with
this error.

The file malloc.c that is included in the test file's first line is
the file provided in direction share/ of the soure distribution. This
file may have been installed in /usr/share/frama-c for instance if you
are using a Linux distribution package. If you compiled yourself on
Unix, it is in /usr/local/share/frama-c.

Pascal