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] Could I disable acsl/rte/wp annotation in value analysis? or treat all property to be valid in value analysis?
- Subject: [Frama-c-discuss] Could I disable acsl/rte/wp annotation in value analysis? or treat all property to be valid in value analysis?
- From: pascal.cuoq at gmail.com (Pascal Cuoq)
- Date: Sun, 8 Sep 2013 20:30:50 +0200
- In-reply-to: <CAA1cxug8Ld4FsxKVFT4VtmWEQbs8HPzYkZs5upVZO7c7byEQOg@mail.gmail.com>
- References: <CAA1cxug8Ld4FsxKVFT4VtmWEQbs8HPzYkZs5upVZO7c7byEQOg@mail.gmail.com>
On Sun, Sep 8, 2013 at 7:23 PM, David Yang <abiao.yang at gmail.com> wrote: > > the code below the line 5 is dead code. I understand that it is because > the default context-width is 2. So line 5 is out of bound memory access. > > But i want to analysis the function by not treat all code to be dead code > and continue the value analysis procedure. > This is not possible in Frama-C's value analysis. More precisely, there are no values worth continuing the execution with after an undefined behavior, such as an out-of-bounds memory access, because ?undefined behavior? means that anything is possible. This is discussed as one of the points in this article: https://www.dropbox.com/s/el2lidf5v71ogm6/p.pdf If you want the value analysis not to treat the code as dead code, tell it that variable A points to an array of size at least the value of variable size. There are several ways to do that. You may find that the best results are obtained with separate analyses for each size. -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20130908/d8043208/attachment.html>
- References:
- [Frama-c-discuss] Could I disable acsl/rte/wp annotation in value analysis? or treat all property to be valid in value analysis?
- From: abiao.yang at gmail.com (David Yang)
- [Frama-c-discuss] Could I disable acsl/rte/wp annotation in value analysis? or treat all property to be valid in value analysis?
- Prev by Date: [Frama-c-discuss] Could I disable acsl/rte/wp annotation in value analysis? or treat all property to be valid in value analysis?
- Next by Date: [Frama-c-discuss] WP: assigns needed to prove function contract?
- Previous by thread: [Frama-c-discuss] Could I disable acsl/rte/wp annotation in value analysis? or treat all property to be valid in value analysis?
- Next by thread: [Frama-c-discuss] Could I disable acsl/rte/wp annotation in value analysis? or treat all property to be valid in value analysis?
- Index(es):