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: dmentre at linux-france.org (David MENTRE)
- Date: Fri, 21 Aug 2015 09:28:07 +0200
- In-reply-to: <CAGSRWbi3GaMAdSUZqiJj19FBzPxgfcscRNb+vAJTtMo9zOUJiw@mail.gmail.com>
- References: <CAGSRWbgQaaaBnjhBWamzidNa4Q+rqwoeJY9NDir98jebQFzmfQ@mail.gmail.com> <55D587D9.2080300@linux-france.org> <CAGSRWbi3GaMAdSUZqiJj19FBzPxgfcscRNb+vAJTtMo9zOUJiw@mail.gmail.com>
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. Best regards, david
- Follow-Ups:
- [Frama-c-discuss] arbitrary buffers in analysis
- From: pascal.cuoq at gmail.com (Pascal Cuoq)
- [Frama-c-discuss] arbitrary buffers in analysis
- 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
- Prev by Date: [Frama-c-discuss] my first frama verification
- Next by Date: [Frama-c-discuss] my first frama verification
- Previous by thread: [Frama-c-discuss] arbitrary buffers in analysis
- Next by thread: [Frama-c-discuss] arbitrary buffers in analysis
- Index(es):