--- layout: fc_discuss_archives title: Message 7 from Frama-C-discuss on August 2015 ---
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>