[kernel] Parsing tests/basic/pointer_to_virtual_method.cpp (external front-end)
Now output intermediate result
/* Generated by Frama-C */
struct _frama_c_vmt_content {
   void (*method_ptr)() ;
   int shift_this ;
};
struct _frama_c_rtti_name_info_node;
struct _frama_c_vmt {
   struct _frama_c_vmt_content *table ;
   int table_size ;
   struct _frama_c_rtti_name_info_node *rtti_info ;
};
struct _frama_c_rtti_name_info_content {
   struct _frama_c_rtti_name_info_node *value ;
   int shift_object ;
   int shift_vmt ;
};
struct _frama_c_rtti_name_info_node {
   char const *name ;
   struct _frama_c_rtti_name_info_content *base_classes ;
   int number_of_base_classes ;
   struct _frama_c_vmt *pvmt ;
};
struct Foo;
struct Foo {
   struct _frama_c_vmt *pvmt ;
};
struct Bar;
struct Bar {
   struct Foo _frama_c__Z3Foo ;
};
static int g = 0;
void Foo::Ctor(struct Foo const *this);

void Foo::Dtor(struct Foo const *this);

struct _frama_c_vmt _frama_c_vmt_header;

struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;

struct _frama_c_vmt_content _frama_c_vmt[1];

/*@ requires \valid(this); */
void m(struct Foo *this, int i)
{
  g = i;
  return;
}

/*@ requires \valid_read(this); */
void Foo::Dtor(struct Foo const *this)
{
  *((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
  return;
}

/*@ requires \valid_read(this); */
void Foo::Ctor(struct Foo const *this)
{
  *((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
  return;
}

int _frama_c_find_dynamic_cast_aux(struct _frama_c_rtti_name_info_node *target_info,
                                   struct _frama_c_rtti_name_info_content *concrete_base,
                                   int number_of_bases,
                                   int found_shift_object,
                                   int found_shift_vmt, int last_shift_vmt,
                                   int *shift_object, int *distance)
{
  int result = 0;
  struct _frama_c_rtti_name_info_content *cursor = concrete_base;
  int is_over = 0;
  int base_index = 0;
  while (base_index < number_of_bases) {
    if (cursor->value == target_info) {
      if (*distance < 0) goto _LOR;
      else 
        if (*distance >= 1) {
          _LOR:
          {
            if (found_shift_vmt == cursor->shift_vmt) *distance = 0;
            else *distance = 1;
            *shift_object = found_shift_object - cursor->shift_object;
            result = 1;
          }
        }
    }
    else 
      if (cursor->shift_vmt <= found_shift_vmt) {
        int tmp_5;
        if (base_index < number_of_bases - 1) tmp_5 = (cursor + 1)->shift_vmt > found_shift_vmt;
        else {
          int tmp_4;
          if (last_shift_vmt == -1) tmp_4 = 1;
          else 
            if (found_shift_vmt < last_shift_vmt) tmp_4 = 1; else tmp_4 = 0;
          tmp_5 = tmp_4;
        }
        if (tmp_5) {
          int tmp_0;
          int tmp;
          int local_distance = 0;
          int local_shift_object = 0;
          if (base_index < number_of_bases - 1) tmp = (cursor + 1)->shift_vmt;
          else tmp = last_shift_vmt;
          ;
          ;
          ;
          ;
          ;
          tmp_0 = _frama_c_find_dynamic_cast_aux(target_info,
                                                 (cursor->value)->base_classes,
                                                 (cursor->value)->number_of_base_classes,
                                                 found_shift_object - cursor->shift_object,
                                                 found_shift_vmt - cursor->shift_vmt,
                                                 tmp,& local_shift_object,
                                                 & local_distance);
          int local_result = tmp_0;
          if (local_result != 0) 
            if (local_distance >= 0) 
              if (*distance < 0) goto _LOR_0;
              else 
                if (*distance >= local_distance) {
                  _LOR_0:
                  {
                    result = local_result;
                    *shift_object = local_shift_object - cursor->shift_object;
                    *distance = local_distance;
                  }
                }
          is_over = 1;
        }
        else goto _LAND;
      }
      else {
        _LAND: ;
        if (*distance < 0) goto _LOR_2;
        else 
          if (*distance >= 1) {
            _LOR_2:
            {
              int tmp_2;
              int tmp_1;
              int local_distance_0 = 0;
              int local_shift_object_0 = 0;
              if (base_index < number_of_bases + 1) tmp_1 = (cursor + 1)->shift_vmt;
              else tmp_1 = last_shift_vmt;
              ;
              ;
              ;
              ;
              ;
              tmp_2 = _frama_c_find_dynamic_cast_aux(target_info,
                                                     (cursor->value)->base_classes,
                                                     (cursor->value)->number_of_base_classes,
                                                     found_shift_object - cursor->shift_object,
                                                     found_shift_vmt - cursor->shift_vmt,
                                                     tmp_1,
                                                     & local_shift_object_0,
                                                     & local_distance_0);
              int local_result_0 = tmp_2;
              if (local_result_0 != 0) 
                if (local_distance_0 >= 0) 
                  if (*distance < 0) goto _LOR_1;
                  else {
                    int tmp_3;
                    if (is_over == 0) tmp_3 = local_distance_0;
                    else tmp_3 = local_distance_0 + 1;
                    ;
                    if (*distance > tmp_3) {
                      _LOR_1:
                      {
                        result = local_result_0;
                        *shift_object = local_shift_object_0 - cursor->shift_object;
                        *distance = local_distance_0 + 1;
                      }
                    }
                  }
            }
          }
      }
    cursor ++;
    base_index ++;
  }
  return result;
}

int _frama_c_find_dynamic_cast(struct _frama_c_rtti_name_info_node *declared_info,
                               struct _frama_c_vmt *declared_vmt,
                               struct _frama_c_rtti_name_info_node *target_info,
                               int *shift_object)
{
  int __retres;
  int shift_vmt;
  int elaborated_shift_target;
  struct _frama_c_rtti_name_info_content *cursor;
  int number_of_bases;
  int tmp_0;
  struct _frama_c_rtti_name_info_node *concrete_info =
    declared_vmt->rtti_info;
  int elaborated_shift_vmt = 0;
  int elaborated_shift_object = 0;
  int cursor_index = 0;
  int distance = -1;
  if (concrete_info->pvmt > declared_vmt) {
    __retres = 0;
    goto return_label;
  }
  else 
    if (declared_vmt > concrete_info->pvmt + declared_vmt->table_size) {
      __retres = 0;
      goto return_label;
    }
  shift_vmt = declared_vmt - concrete_info->pvmt;
  if (concrete_info == declared_info) {
    *shift_object = 0;
    __retres = target_info == declared_info;
    goto return_label;
  }
  if (target_info == concrete_info) elaborated_shift_target = 0;
  else elaborated_shift_target = -1;
  cursor = concrete_info->base_classes;
  number_of_bases = concrete_info->number_of_base_classes;
  while (1) {
    while (1) {
      if (cursor_index < number_of_bases) {
        if (! (elaborated_shift_vmt + cursor->shift_vmt < shift_vmt)) 
          break;
      }
      else break;
      {
        struct _frama_c_rtti_name_info_content *tmp;
        if (cursor_index < number_of_bases - 1) tmp = cursor + 1;
        else tmp = (struct _frama_c_rtti_name_info_content *)0;
        struct _frama_c_rtti_name_info_content *next_cursor = tmp;
        if (next_cursor != (struct _frama_c_rtti_name_info_content *)0) 
          if (elaborated_shift_vmt + next_cursor->shift_vmt <= shift_vmt) {
            cursor = next_cursor;
            cursor_index ++;
          }
          else break;
        else break;
      }
    }
    if (cursor_index < number_of_bases) {
      elaborated_shift_vmt += cursor->shift_vmt;
      elaborated_shift_object += cursor->shift_object;
      if (cursor->value == target_info) elaborated_shift_target = elaborated_shift_object;
      if (elaborated_shift_vmt == shift_vmt) 
        if (cursor->value == declared_info) {
          if (elaborated_shift_target >= 0) {
            *shift_object = elaborated_shift_target - elaborated_shift_object;
            __retres = 1;
            goto return_label;
          }
          break;
        }
      cursor = (cursor->value)->base_classes;
      number_of_bases = (cursor->value)->number_of_base_classes;
      cursor_index = 0;
    }
    if (! (cursor_index < number_of_bases)) break;
  }
  if (cursor_index >= number_of_bases) {
    __retres = 0;
    goto return_label;
  }
  tmp_0 = _frama_c_find_dynamic_cast_aux(target_info,
                                         concrete_info->base_classes,
                                         concrete_info->number_of_base_classes,
                                         elaborated_shift_object,shift_vmt,
                                         -1,shift_object,& distance);
  __retres = tmp_0;
  return_label: return __retres;
}

struct _frama_c_vmt_content _frama_c_vmt[1] =
  {{.method_ptr = (void (*)())(& m), .shift_this = 0}};
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "Foo",
   .base_classes = (struct _frama_c_rtti_name_info_content *)0,
   .number_of_base_classes = 0,
   .pvmt = & _frama_c_vmt_header};
struct _frama_c_vmt _frama_c_vmt_header =
  {.table = _frama_c_vmt,
   .table_size = 1,
   .rtti_info = & _frama_c_rtti_name_info};
void Bar::Ctor(struct Bar const *this);

void Bar::Dtor(struct Bar const *this);

struct _frama_c_vmt _frama_c_vmt_header;

struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;

struct _frama_c_rtti_name_info_content _frama_c_base_classes[1];

struct _frama_c_vmt_content _frama_c_vmt[1];

/*@ requires \valid(this); */
void m(struct Bar *this, int i)
{
  g = 2 * i;
  return;
}

/*@ requires \valid_read(this); */
void Bar::Dtor(struct Bar const *this)
{
  *((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
  Foo::Dtor(& this->_frama_c__Z3Foo);
  return;
}

/*@ requires \valid_read(this); */
void Bar::Ctor(struct Bar const *this)
{
  Foo::Ctor(& this->_frama_c__Z3Foo);
  *((struct _frama_c_vmt **)this) = & _frama_c_vmt_header;
  return;
}

struct _frama_c_vmt_content _frama_c_vmt[1] =
  {{.method_ptr = (void (*)())(& m), .shift_this = 0}};
struct _frama_c_rtti_name_info_content _frama_c_base_classes[1] =
  {{.value = & _frama_c_rtti_name_info,
    .shift_object = (char *)0 - (char *)(& ((struct Bar *)0)->_frama_c__Z3Foo),
    .shift_vmt = 0}};
struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
  {.name = "Bar",
   .base_classes = _frama_c_base_classes,
   .number_of_base_classes = 1,
   .pvmt = & _frama_c_vmt_header};
struct _frama_c_vmt _frama_c_vmt_header =
  {.table = _frama_c_vmt,
   .table_size = 1,
   .rtti_info = & _frama_c_rtti_name_info};
int main(void)
{
  void (*mptr)(struct Foo *, int ) = & m;
  struct Bar bar;
  Bar::Ctor(& bar);
  struct Foo *mbar = & bar._frama_c__Z3Foo;
  (*mptr)(mbar,42);
  Bar::Dtor((struct Bar const *)(& bar));
  return g;
}