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.
- Prev by Date: [Frama-c-discuss] using jessie to verify float problem
- Next by Date: [Frama-c-discuss] using jessie to verify float problem
- Previous by thread: [Frama-c-discuss] Unable to work with large projects
- Next by thread: [Frama-c-discuss] dead code after an assertion unknown status
- Index(es):