Linux Driver Verification » BLAST

Current development version of CIL (bc1cb8e676e71c0adabe04da5d760d2c85f24268) behaves correctly at least on the following tests:

struct flex
{
  int a;
  int b[];
};
struct flex fa = {1, {1}};
struct flex fb = {2, {2, 2}};
struct S
{
  int field;
  int arr[];
};
struct S var1 = { .field = 0, .arr = { [0] = 1 } };
struct S var2 = { .field = 0, .arr = { 1, [3] = 2 } };

is translated into

struct flex fa  =    {1, {1}};
struct flex fb  =    {2, {2, 2}};
struct S var1  =    {0, {1}};
struct S var2  =    {0, {1, 0, 0, 2}};