C Instrumentation Framework

The mistake is from here:

./drivers/acpi/battery.m0032.rep.gz == ZZZ: Exception: SymbolicStore.Value.Invalid_access("Attempt to access a non structure value as a structure: field0.field1  value: 1")

...
typedef unsigned long long acpi_integer;
typedef u32 acpi_object_type;
typedef u32 acpi_event_type;
typedef u32 acpi_event_status;
typedef u8 acpi_adr_space_type;
union acpi_object {
 acpi_object_type type;
 struct {
  acpi_object_type type;
  acpi_integer value;
 } integer;

 struct {
  acpi_object_type type;
  u32 length;
  char *pointer;
 } string;

 struct {
  acpi_object_type type;
  u32 length;
  u8 *pointer;
 } buffer;

 struct {
  acpi_object_type type;
  u32 count;
  union acpi_object *elements;
 } package;

 struct {
  acpi_object_type type;
  acpi_object_type actual_type;
  acpi_handle handle;
 } reference;

 struct {
  acpi_object_type type;
  u32 proc_id;
  acpi_io_address pblk_address;
  u32 pblk_length;
 } processor;

 struct {
  acpi_object_type type;
  u32 system_level;
  u32 resource_order;
 } power_resource;
};
...
static int extract_package(...)
{
...
union acpi_object *element;
...
...element->integer.value...
...
}
...
=====

In generated by llc (after LLVM):
=====
...
struct l_unnamed9 {
  unsigned int field0;
  unsigned int field1;
  unsigned long long field2;
  unsigned int field3;
};

struct l_struct_2E_acpi_object {
  struct l_unnamed9 field0;
};
...
struct l_struct_2E_device_dma_parameters {
  unsigned int field0;
  unsigned long long field1;
};
...
static unsigned int extract_package(...)
{
...
struct l_struct_2E_acpi_object *llvm_cbe_tmp__152;
unsigned long long llvm_cbe_tmp__153;
...
llvm_cbe_tmp__153 = *((&(((struct l_struct_2E_device_dma_parameters
*)((&llvm_cbe_tmp__152->field0))))->field1));
...
}
...

Generated variant is correct and it's taken by gcc good but it seems too complicated for CIL or BLAST to parse it correctly.

Don't know what to do at the moment.