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] Unable to work with large projects

  • Subject: [Frama-c-discuss] Unable to work with large projects
  • From: Pascal.CUOQ at cea.fr (CUOQ Pascal)
  • Date: Sun, 18 Oct 2009 21:18:58 +0200
  • References: <b15d09070910181203r3165209esea8412644fc6f17d@mail.gmail.com>
Hello Alexandre,

> maybe I was unlucky with the project I've chosen
> as it may have been carefully programmed/checked,
> since I only got "The name foobar is used for two
> distinct globals" messages.

It would be the first time ever someone finds Frama-C is not
giving enough feedback! This is almost as unlikely as the thought
of a large piece of C software on which man-years have not
already been spent exclusively ironing out bugs not having a
single one left to uncover.

In all likelihood the value analysis did not take place, for
whatever reason, but perhaps simply because you did not use the
-val option.

More about that: Frama-C is a framework where, in its current
state, various approaches to software *verification* are
implemented as plug-ins. This means that if you do not specify
one (or several) of them specifically, only the syntactic
analysis takes place, because there is no reason to assume you
want one more than the others. This would correspond well to the
warning you said you had, which should be detected at link-time
when compiling but isn't because object files do not carry types
(by the way, I urge you to take it seriously).
Frama-C detects the problem when doing its own source-level link.
Well, technically, the credit should go to the CIL parser that
we use a modified version of.

Note that *I* am assuming that you want the value analysis, and
not, say, deductive verification using the Jessie plug-in. That's
only because you do not seem very keen on manual intervention in
the analysis process.

Projects of a size comparable to yours have been analyzed
in Frama-C, by people who were trying to verify them
(i.e. establish beyond reasonable doubt the absence of bug for
some definition of "bug"). They may have had more motivation than
you, no offense intended -- when the intention is to verify
software, the alternative to formal methods as proposed in
Frama-C is to use tests and code reviews, and the consensus is
that you need a *lot* of these to get to the point where you are
sure there couldn't possibly be any bug left. Just look how many
bugs are left in software when "only" large quantities of them are
used.  Using tests and code reviews for verification works, but
you need insane amounts of them.

The value analysis does, as you will notice as soon as you do
launch it, emit a warning in every place it can not guarantee a
run-time error does not take place.  Other tools (bug-finding
tools) try only to warn about probable bugs. An example, that I
think I got from the talk linked below, is a program that checks
a pointer for NULL after it has already been dereferenced. If
this happens locally enough, a bug-finding tool will warn: if you
aren't sure that the pointer is not NULL, should you have
dereferenced it earlier?

http://video.google.com/videoplay?docid=-8150751070230264609#

The reasoning is that either the test to NULL is unnecessary or
there is a risk of dereferencing NULL, and in both cases the user
will be grateful to have the location where this is happening
pointed out to him.

Contrast this with the value analysis' behavior, which is not to
warn if it is able to infer *on its own* that the pointer is
valid, and to warn otherwise, independently of any test to NULL
that may appear in the program. Also, the value analysis will not
warn if the program compares an always valid pointer to NULL,
because this comparison does not introduce undefinedness in the
program. The value analysis is definitely not a style checker.

At this point you may be thinking "that's what I need, a
bug-finding, style-checking tool!". Findbugs in the video above
is for Java, but have a look at the tool clang. It's open-source
and although it does not do the same thing as Frama-C, we hear
good things about it.

On the other hand, if you think you are interested in software
verification, my advice would be to work your way up from small
to medium projects, instead of trying to get results on a large
one on your first try. If doesn't matter that the small projects
you start with do not have bugs. Verification is not about finding
bugs, it's about making sure that there aren't any.

> I was hopping to use it for dead code removal (but that plugin
> requires ACSL tags in the code)

I am not sure exactly what you mean. Slicing requires you
to specify what it is that you want to keep, but that's
minimal intervention. And it relies on the value analysis'
results, which require all functions to be available or specified
in ACSL (including library functions, down to a modelization
in C or ACSL of system calls). How else could it infer reliably
that the value of a pointer is not NULL?

> and also to spot potencial bad
> programming cases, like race conditions and the likes.

The verification of concurrent code is a whole other mess, where
other techniques make sense. All distributed plug-ins for
Frama-C are for sequential code. We have undistributed
prototype plug-ins for infering things about concurrent code.

Pascal

PS: If I had a blog, this would be its first post.