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] arbitrary buffers in analysis
- Subject: [Frama-c-discuss] arbitrary buffers in analysis
- From: pascal.cuoq at gmail.com (Pascal Cuoq)
- Date: Fri, 21 Aug 2015 20:40:44 +0200
- In-reply-to: <55D6D307.1080605@linux-france.org>
- References: <CAGSRWbgQaaaBnjhBWamzidNa4Q+rqwoeJY9NDir98jebQFzmfQ@mail.gmail.com> <55D587D9.2080300@linux-france.org> <CAGSRWbi3GaMAdSUZqiJj19FBzPxgfcscRNb+vAJTtMo9zOUJiw@mail.gmail.com> <55D6D307.1080605@linux-france.org>
Hello Tim and David, On Fri, Aug 21, 2015 at 9:28 AM, David MENTRE <dmentre at linux-france.org> wrote: > Hello Tim, > > Le 20/08/2015 18:58, Tim Newsham a écrit : > >> It doesn't seem that will work to verify all buffer >> sizes (for example, l=0xffffffffffffffff on 64-bit memory spaces). >> > > Yes. For such big values, you might have more success with Deductive > Verification, thus WP or Jessie plug-ins. But it is also a lot of more work > to prove, e.g., absence of Run Time Error. > > The main advantage of Frama-C is that you can combine both techniques, > i.e. Value Analysis and WP. One relatively efficient technique for combining them could be this: A/ Frama-C's value analysis supports memory blocks the size of which is not known precisely. Any access to such a block beyond the first byte causes an alarm to be emitted BUT the possibility that the memory access might be valid is also taken into account. One way to cause the creation of such a memory block by the analyzer was malloc(Frama_C_interval(1, 0x7fffffff)). Unfortunately this doesn't work any more with the open-source version because the built-in for malloc has been removed. However, you can still declare an extern array with an incomplete type, and this has some of the same effects. (Note: the support for extern arrays with an incomplete type could disappear too, because it singlehandedly causes a lot of special cases that need to be taken into account in a lot of places in the analyzer, and removing support for these variables would simply the analyzer a lot. Anyway, in the current version, this support appears to be available, so you can use this to get an idea of how the method works on small examples, bearing in mind that you might encounter bugs that, if you report them, might push the Frama-C developers to simply remove support for extern arrays with an incomplete type.) An example looks like this: extern char t[]; int main(void){ t[1] = 1; t[2] = 2; t[3] = 3; Frama_C_dump_each(); } Analyzed, this produces: $ frama-c -val t.c ... [value] Computing initial state t.c:1:[kernel] imprecise size for variable t t.c:1:[value] warning: during initialization of variable 't', size of type 'char []' cannot be computed (Size of array without number of elements.) ... t.c:4:[kernel] warning: out of bounds write. assert \valid(&t[1]); t.c:5:[kernel] warning: out of bounds write. assert \valid(&t[2]); t.c:6:[kernel] warning: out of bounds write. assert \valid(&t[3]); [value] DUMPING STATE of file t.c line 7 t[0] â [--..--] [1] â {1} [2] â {2} [3] â {3} [4..4294967295] â [--..--] __retres â UNINITIALIZED =END OF DUMP== Note how the analyzer did not assume that execution stopped when t[1] (and then t[2] and t[3]) were accessed, although it emitted an alarm for them. Because it had to take into account the possibility that these memory locations were valid, it considered the possibility that execution continued too (in this case the value at t[1] can only be 1). The values displayed at Frama_C_dump_each() are of course only for the executions that reach that point. Executions that have become stuck while accessing memory illegally are not shown there because they stopped earlier. So the analyzer guarantees that t[1] is 1 at that point. If this is not clear, contrast with the behavior of the analyzer on the same program where the array t is declared with a known size of 1 instead. B/ Use any other Frama-C plug-in to verify the assertions generated by the value analysis, including those about memory accesses that are caused by the value analysis' unusual behavior for the array t. The deductive plug-ins available for Frama-C may not completely handle all aspects of dynamic allocation yet, but for the usecase being discussed, I think that they already have pretty much all the features that are needed, that is, the ability to reason symbolically about a valid block of size n. I assume that the pre-condition \valid(&t[0 .. n-1]) would appear somewhere. -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150821/782a148b/attachment.html>
- References:
- [Frama-c-discuss] arbitrary buffers in analysis
- From: tim.newsham at gmail.com (Tim Newsham)
- [Frama-c-discuss] arbitrary buffers in analysis
- From: dmentre at linux-france.org (David MENTRE)
- [Frama-c-discuss] arbitrary buffers in analysis
- From: tim.newsham at gmail.com (Tim Newsham)
- [Frama-c-discuss] arbitrary buffers in analysis
- From: dmentre at linux-france.org (David MENTRE)
- [Frama-c-discuss] arbitrary buffers in analysis
- Prev by Date: [Frama-c-discuss] headers question
- Next by Date: [Frama-c-discuss] arbitrary buffers in analysis
- Previous by thread: [Frama-c-discuss] arbitrary buffers in analysis
- Next by thread: [Frama-c-discuss] arbitrary buffers in analysis
- Index(es):