--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on August 2015 ---
Hi, In the code below, the assertions in the main function are verified by Frama-C/WP (Sodium-20150201), but the assertions in the foo function are not. Can anyone please explain why? What is the semantics of static arrays in nested curly braces? void foo() { { static const int a[2] = { 4, 5 }; //@assert a[0] == 4; //@assert a[1] == 5; } } int main() { { static const int b[2] = { 9, 8 }; //@assert b[0] == 9; //@assert b[1] == 8; } return 0; } -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20150817/0dff8154/attachment.html>