--- layout: fc_discuss_archives title: Message 6 from Frama-C-discuss on August 2015 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] static arrays



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>