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] Is there any method not to initalize all global variables while doing value analysis?

  • Subject: [Frama-c-discuss] Is there any method not to initalize all global variables while doing value analysis?
  • From: pascal.cuoq at gmail.com (Pascal Cuoq)
  • Date: Wed, 31 Oct 2012 11:49:05 +0100
  • In-reply-to: <004301cdb733$def25150$9cd6f3f0$@gmail.com>
  • References: <004301cdb733$def25150$9cd6f3f0$@gmail.com>
On Wed, Oct 31, 2012 at 7:49 AM, Ben <abiao.yang at gmail.com> wrote:
> Which industrial embedded C code has been successfully applied?

The experiments that have been published are ?Fan-C, a Frama-C
plug-in for data flow verification?, ?Formal Verification of Industrial C Code
using Frama-C: a Case Study? and ?Formal Verification of Software
Important to Safety Using the Frama-C Tool Suite?.

> Is there any large open source codebases have been analysis by using
> frama-c?

The Sidan people have analyzed (at least a significant part of) OpenSSH:
http://www.rennes.supelec.fr/ren/rd/cidre/tools/sidan/pubs.html

I am afraid that the most comprehensive source of information is
Jonathan-Christofer Demay's thesis, in French.

> Maybe I should first use CIL (C
> Intermediate Language) to merge all vim source codes into a single file.
> Then, use frama-c to analysis that merged file.
> At that situation, I have no need to set that '-main' option for each
> function and do value analysis only once.

You can pass several files on the commandline:
frama-c file1.c file2.c ...

The more files, the more globals, so the longer it will take to create the
initial state, but you should be able to analyze at least groups of functions
together by picking meaningful entry points and letting the callees
be analyzed with the values coming from their callers.

> But when I use the command line:
> 'frama-c -value-help'
> It shows that:
> "...
> -slevel <n>  use <n> as number of path to explore in parallel
> ..."
> This makes me misunderstanding and wrongly using this option.

I see. In the next release, it will read:

-slevel <n>         superpose up to <n> states when unrolling control flow.
                    The larger n, the more precise and expensive the analysis
                    (defaults to 0)

I hope this will be clearer. Thanks for the feedback.

> > > Is there any method to ignore those errors like "length of array size
> > > is zero" and continue to do value analysis?
> >
> > The C99 standard says:
> >
> > 6.7.5.2 Array declarators
> > Constraints
> >
> > 1. [...] If the expression is a constant expression, it shall have a value
> greater
> > than zero.
> >
>
> Thank you. Maybe the linux-kernel version which I analyzed is out of date.

Yes, in a way.
Zero length arrays are a pre-C99 GCC extension. This extension is essentially
made obsolete by C99's ?incomplete types?. I suppose that the Linux kernel would
be marginally cleaner with the standard C99 feature instead of a GCC extension,
but the Linux maintainers have declared they were not interested in not relying
on GCC extensions (they are fine targeting other compilers as long as these
compilers have all the same extensions as GCC, like Clang).

> I would like to know if there is anybody have succeed analyzing Linux-kernel
> by using your group's tool frama-c before?

This would be very difficult. It would take a couple of man-years to do make a
significant dent into the problem. I would suggest targeting a well-delimited
part, such as a particular self-contained module or a filesystem. Even so,
there will be a lot of work.

Pascal