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] static arrays
- Subject: [Frama-c-discuss] static arrays
- From: pascal.cuoq at gmail.com (Pascal Cuoq)
- Date: Tue, 18 Aug 2015 04:53:15 +0200
- In-reply-to: <CAL+X0enWOro4KtpXUCBee4=-SG4LNYht8X=VgBad+tjWVsckKQ@mail.gmail.com>
- References: <CAL+X0enWOro4KtpXUCBee4=-SG4LNYht8X=VgBad+tjWVsckKQ@mail.gmail.com>
On Mon, Aug 17, 2015 at 9:57 PM, Junkil (David) Park < junkil.park at cis.upenn.edu> wrote: > What is the semantics of static arrays in nested curly braces? > The front-end moves them outside the block that limits their scope, renaming them as appropriate to avoid clashes, as you can see for yourself here: $ frama-c -print t.c ⦠[kernel] preprocessing with "gcc -C -E -I. t.c" /* Generated by Frama-C */ void foo(void); static int const a[2] = {4, 5}; void foo(void) { /*@ assert a[0] ⡠4; */ ; /*@ assert a[1] ⡠5; */ ; return; } int main(void); static int const b[2] = {9, 8}; int main(void) { int __retres; /*@ assert b[0] ⡠9; */ ; /*@ assert b[1] ⡠8; */ ; __retres = 0; return __retres; } So for function foo(), the reason the assertion a[0] == 4 is not proved is that this property is not the result of local reasoning (after normalization). Adding a pre-condition to foo() that a[0] == 4 would make proving the assertion local reasoning, and thus should allow WP to conclude (untested). If the caller of foo() is not main() but a function g(), you would need to make a[0]==4 a pre-condition of g() too. The function main() is the exception here. WP assumes that global variables have their initial values at the start of main() without needing to be told so (page 20 of http://frama-c.com/download/wp-manual-Sodium-20150201.pdf ). WP does not appear to take advantage of const qualifiers, according to your results. I will leave you the care of submitting that as a feature wish if you think that it is important. -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150818/e8f7c7ed/attachment.html>
- Follow-Ups:
- [Frama-c-discuss] static arrays
- From: boris at yakobowski.org (Boris Yakobowski)
- [Frama-c-discuss] static arrays
- References:
- [Frama-c-discuss] static arrays
- From: junkil.park at cis.upenn.edu (Junkil (David) Park)
- [Frama-c-discuss] static arrays
- Prev by Date: [Frama-c-discuss] static arrays
- Next by Date: [Frama-c-discuss] specification question
- Previous by thread: [Frama-c-discuss] static arrays
- Next by thread: [Frama-c-discuss] static arrays
- Index(es):