diff --git a/convert.ml b/convert.ml
index 50c629a28e5a7c4391ee0f43d88be6b72bc1fc72..bb27c1ca713f2fe49ef98a8a6aaadff040403e7d 100644
--- a/convert.ml
+++ b/convert.ml
@@ -673,8 +673,8 @@ let rec convert_base_type env spec decl typ does_remove_virtual =
let attrs = List.map cv_to_attr spec in
env,
(rt,
- (fun d ->
- rt_decl
+ (fun d ->
+ rt_decl
(PROTO (decl (protect_ptr_type attrs d), args,[],variadic))))
| LVReference (PFunctionPointer s)
| RVReference (PFunctionPointer s) ->
@@ -684,7 +684,7 @@ let rec convert_base_type env spec decl typ does_remove_virtual =
let attrs= List.map cv_to_attr spec in
env,
(rt,
- (fun d ->
+ (fun d ->
rt_decl (PROTO (decl (protect_ptr_type attrs d),args,[],variadic))))
| Pointer(PStandardMethodPointer _)
| LVReference (PStandardMethodPointer _)
@@ -2146,21 +2146,21 @@ and convert_init_statement env init does_remove_virtual =
let env = Convert_env.add_local_var env id_name typ.plain_type in
match init_val with
| None ->
- let init = (id_name, decl JUSTBASE,[],loc),NO_INIT in
- (env, aux, init::l, def, base)
+ let init = (id_name, decl JUSTBASE,[],loc),NO_INIT in
+ (env, aux, init::l, def, base)
| Some init ->
let var = Local { prequalification = []; decl_name = id_name } in
let env,aux',init, def' =
convert_initializer env typ var init does_remove_virtual
in
- let def = match def' with
- | None -> def
- | Some stmt -> stmt::def
- in
- let init = (id_name, decl JUSTBASE,attrs,loc),init in
- env, merge_aux aux' aux, init::l, def, base)
- init_declarator_list
- (env, empty_aux, [], [], None)
+ let def = match def' with
+ | None -> def
+ | Some stmt -> stmt::def
+ in
+ let init = (id_name, decl JUSTBASE,attrs,loc),init in
+ env, merge_aux aux' aux, init::l, def, base)
+ init_declarator_list
+ (env, empty_aux, [], [], None)
in
let l = List.rev l in
if l = [] then
diff --git a/tests/class/oracle/extern_c_class.res.oracle b/tests/class/oracle/extern_c_class.res.oracle
index 900abea7d405005a2a08a4af3b4e6bd23aae9488..030abfe4fd636a387e5f87847cfee2d2935dee93 100644
--- a/tests/class/oracle/extern_c_class.res.oracle
+++ b/tests/class/oracle/extern_c_class.res.oracle
@@ -1,37 +1,8 @@
[kernel] Parsing extern_c_class.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 C;
struct C {
- struct _frama_c_vmt *pvmt ;
};
-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];
-
void set(struct C *this, int *t);
int get_x(struct C *this);
@@ -40,240 +11,9 @@ int get_x(struct C *this);
void set(struct C *this, int *t)
{
*t = get_x(this);
- struct _frama_c_vmt_content *__virtual_tmp_0 =
- (*((struct _frama_c_vmt **)this))->table + 0;
- (*((void (*)(struct C *))__virtual_tmp_0->method_ptr))((struct C *)(
- (char *)this - __virtual_tmp_0->shift_this));
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;
-}
-
-void foo(struct C *this);
-
-struct _frama_c_vmt_content _frama_c_vmt[1] =
- {{.method_ptr = (void (*)())(& foo), .shift_this = 0}};
-struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
- {.name = "C",
- .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};
int get_x(struct C *this)
{
int __retres;