CPAchecker does not handle anonymous unions or structs in designated initializers

• CPAchecker version: commit 95acb0b7
• Example programs:
  • Anonymous union

typedef struct union_in_struct_s {
  union {
    char a;
    short b;
  };
  int c;
} union_in_struct_t;

int main() {
  union_in_struct_t s = {.a = 1, .b = 2, .c = 3};
  __VERIFIER_assert(s.a == 1);
  return 0;
}

• Anonymous struct

typedef union struct_in_union_u {
  struct {
    char a;
    short b;
  };
  int c;
} struct_in_union_t;

int main() {
  struct_in_union_t u = {.a = 1, .b = 2, .c = 3};
  __VERIFIER_assert(u.a == 1);
  return 0;
}

• Command: ./bin/cpachecker --spec sv-comp-reachability --bmc <example>
• Expected behavior: CPAchecker detects the assertions in both programs are violated (a is 2 in the first example and 3 in the second)
• Actual behavior: parsing failure

Error: Parsing failed (line 28: Unrecognized C code (Initializer for field a but no field with this name exists in union struct_in_union_u): .a (line was originally struct_in_union_t u = {.a = 1, .b = 2, .c = 3};)) (CFACreator.createCFA, SEVERE)