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)

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)

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):
- Date
- Thread