diff --git a/convert.ml b/convert.ml
index 6196db1ecd893c5de49de38232de2db8ad61a28c..6a3c47a58ee58fcc1bc0c4913c4a163f38afb761 100644
--- a/convert.ml
+++ b/convert.ml
@@ -570,6 +570,25 @@ let preserved_returned_object aux e =
List.map transf aux
| _ -> aux
+let convert_class_name env name tc =
+ if Convert_env.is_extern_c_aggregate env name tc then name.decl_name
+ else
+ let s, t = Convert_env.typedef_normalize env name tc in
+ Mangling.mangle s t None
+
+let qual_vmt_content_name = Cxx_utils.empty_qual "_frama_c_vmt_content"
+let qual_vmt_name = Cxx_utils.empty_qual "_frama_c_vmt"
+
+let mk_vmt_content_type env =
+ let name, tc =
+ Convert_env.typedef_normalize env qual_vmt_content_name TStandard
+ in
+ Tstruct (convert_class_name env name tc, None, [])
+
+let mk_vmt_type env =
+ let name, tc = Convert_env.typedef_normalize env qual_vmt_name TStandard in
+ Tstruct (convert_class_name env name tc, None, [])
+
let rec convert_base_type env spec decl typ does_remove_virtual =
match typ with
| Void -> env, (spec_type Tvoid :: spec, decl)
@@ -610,12 +629,7 @@ let rec convert_base_type env spec decl typ does_remove_virtual =
in
env, (spec_type (Tenum(name,None,[]))::spec, decl)
| Struct (s,t) ->
- let name =
- if Convert_env.is_extern_c_aggregate env s t then s.decl_name
- else
- let s, t = Convert_env.typedef_normalize env s t in
- Mangling.mangle s t None
- in
+ let name = convert_class_name env s t in
env, (spec_type (Tstruct (name, None, [])) :: spec, decl)
| Union (s,t) ->
let name =
@@ -837,9 +851,7 @@ and convert_expr_node ?(drop_temp=false) env aux e does_remove_virtual =
Cxx_utils.(
plain_obj_ptr (unqual_type (Struct (derived_name,td))))
in
- let derived_name, td =
- Convert_env.typedef_normalize env derived_name td
- in
+ let name = convert_class_name env derived_name td in
let init =
if not is_reference then e else mk_expr env (UNARY(ADDROF, e))
in
@@ -847,9 +859,7 @@ and convert_expr_node ?(drop_temp=false) env aux e does_remove_virtual =
add_local_aux_def aux
(DECDEF(
None,
- ([SpecType
- (Tstruct
- (Mangling.mangle derived_name td None, None, []))],
+ ([SpecType (Tstruct (name,None,[]))],
[(var_name, PTR([], JUSTBASE),[], e.expr_loc),
SINGLE_INIT(init)]), e.expr_loc))
in
@@ -860,19 +870,14 @@ and convert_expr_node ?(drop_temp=false) env aux e does_remove_virtual =
if (noeffect) then access, aux, env
else begin
let table_access = virtual_var_name () in
- let qual_vmt_content_name = Cxx_utils.empty_qual "_frama_c_vmt_content" in
let env =
Convert_env.add_local_var env table_access
Cxx_utils.(
plain_obj_ptr (
unqual_type (Struct (qual_vmt_content_name, TStandard))))
in
- let qual_vmt_content_name, _ =
- Convert_env.typedef_normalize env qual_vmt_content_name TStandard
- in
let tmp_decl = DECDEF( None,
- ([SpecType (Tstruct (Mangling.mangle
- qual_vmt_content_name TStandard None, None, []))],
+ ([SpecType (mk_vmt_content_type env)],
[(table_access,PTR( [], JUSTBASE),[],access.expr_loc),
SINGLE_INIT (access)]),
access.expr_loc)
@@ -1006,10 +1011,11 @@ and convert_expr_node ?(drop_temp=false) env aux e does_remove_virtual =
env (rt,decl JUSTBASE)
(mk_addrof env (mk_expr env (MEMBEROF(e, cname)))))
| RPKVirtualBasePointer(base_index, origin_type, noeffect) ->
- let derived_name, td =
+ let derived_name,td =
Convert_env.get_class_name_from_pointer
env origin_type.plain_type
in
+ let cderived_name= convert_class_name env derived_name td in
let var_name = shift_ptr_var_name () in
let env =
Convert_env.add_local_var
@@ -1020,26 +1026,16 @@ and convert_expr_node ?(drop_temp=false) env aux e does_remove_virtual =
let def =
DECDEF(
None,
- ([SpecType
- (Tstruct
- (Mangling.mangle derived_name td None, None, []))],
+ ([SpecType (Tstruct (cderived_name,None,[]))],
[(var_name, PTR([], JUSTBASE),[], e.expr_loc),
SINGLE_INIT(e)]), e.expr_loc)
in
let aux = add_local_aux_def aux def in
- let qual_vmt_name = Cxx_utils.empty_qual "_frama_c_vmt" in
let this_access, aux, env =
create_this_access e origin_type aux env false noeffect
in
- let qual_vmt_name, _ =
- Convert_env.typedef_normalize env qual_vmt_name TStandard
- in
let vmt_type =
- [SpecType
- (Tstruct
- (Mangling.mangle qual_vmt_name
- TStandard None, None, []))],
- PTR ([], PTR ([], JUSTBASE))
+ [SpecType (mk_vmt_type env)], PTR ([], PTR ([], JUSTBASE))
in
let table_access_def =
mk_expr env
@@ -1075,16 +1071,8 @@ and convert_expr_node ?(drop_temp=false) env aux e does_remove_virtual =
create_this_access e origin_type aux env
true (* is_reference *) false (* noeffect *)
in
- let qual_vmt_name = Cxx_utils.empty_qual "_frama_c_vmt" in
- let qual_vmt_name,_ =
- Convert_env.typedef_normalize env qual_vmt_name TStandard
- in
let vmt_type =
- [SpecType
- (Tstruct
- (Mangling.mangle
- qual_vmt_name TStandard None, None, []))],
- PTR ([], PTR ([], JUSTBASE))
+ [SpecType (mk_vmt_type env)], PTR ([], PTR ([], JUSTBASE))
in
let table_access_def =
mk_expr env
@@ -1374,7 +1362,6 @@ and convert_expr_node ?(drop_temp=false) env aux e does_remove_virtual =
let qual_vmt_content_name =
Cxx_utils.empty_qual "_frama_c_vmt_content"
in
- let qual_vmt_name = Cxx_utils.empty_qual "_frama_c_vmt" in
let env =
Convert_env.add_local_var
env var_name
@@ -1401,24 +1388,8 @@ and convert_expr_node ?(drop_temp=false) env aux e does_remove_virtual =
([SpecType Tchar], PTR ([], JUSTBASE))
(List.fold_left shift_expr this shiftPvmt))
in
- let qual_vmt_content_name, _ =
- Convert_env.typedef_normalize env qual_vmt_content_name TStandard
- in
- let qual_vmt_name, _ =
- Convert_env.typedef_normalize env qual_vmt_name TStandard
- in
- let vmt_content_base_type =
- [SpecType
- (Tstruct
- (Mangling.mangle qual_vmt_content_name TStandard None,
- None, []))]
- in
- let vmt_base_type =
- [SpecType
- (Tstruct
- (Mangling.mangle qual_vmt_name TStandard None,
- None, []))]
- in
+ let vmt_content_base_type = [SpecType (mk_vmt_content_type env)] in
+ let vmt_base_type = [SpecType (mk_vmt_type env)] in
let vmt_access =
mk_expr env
(UNARY
@@ -1470,6 +1441,7 @@ and convert_expr_node ?(drop_temp=false) env aux e does_remove_virtual =
let class_name, tc =
Convert_env.typedef_normalize env class_name tc
in
+ let cclass_name = convert_class_name env class_name tc in
env, add_local_aux_def aux tmp_decl,
CALL(
mk_expr env
@@ -1485,9 +1457,7 @@ and convert_expr_node ?(drop_temp=false) env aux e does_remove_virtual =
env
(MEMBEROFPTR (mk_var env var_name, "method_ptr"))))),
(mk_cast env
- ([SpecType
- (Tstruct
- (Mangling.mangle class_name tc None, None, []))],
+ ([SpecType (Tstruct (cclass_name, None, []))],
PTR ([], JUSTBASE))
(mk_expr env
(BINARY
@@ -2597,10 +2567,7 @@ let bare_or_derived_type env most_derived n =
let make_class_decl env name tkind kind inherits fields body has_virtual =
let n, t = Convert_env.typedef_normalize env name tkind in
- let class_name =
- if Convert_env.is_extern_c env then n.decl_name
- else Mangling.mangle n t None
- in
+ let class_name = convert_class_name env name tkind in
let loc = Convert_env.get_loc env in
let create_class_type base tb =
{ qualifier = []; plain_type = (Struct (base,tb)) }
@@ -2639,14 +2606,11 @@ let make_class_decl env name tkind kind inherits fields body has_virtual =
let n, t = Convert_env.typedef_normalize env base tb in
let n' =
if Class.has_virtual_base_class (base,tb) then bare_qname n else n
- in (FIELD
- ([SpecType
- (Tstruct
- (Mangling.mangle n' t None,
- None, []))],
- [(create_base_field_name env n t,
- JUSTBASE, [], loc),
- None]),
+ in
+ let cname = convert_class_name env n' t in
+ (FIELD
+ ([SpecType (Tstruct (cname, None, []))],
+ [(create_base_field_name env n t, JUSTBASE, [], loc), None]),
(create_class_type base tb))
::result)
[] virtual_base_classes
@@ -2675,14 +2639,11 @@ let make_class_decl env name tkind kind inherits fields body has_virtual =
then bare_qname n
else n
in
+ let cname = convert_class_name env n' t in
has_virtual,
(FIELD
- ([SpecType
- (Tstruct
- (Mangling.mangle n' t None,
- None, []))],
- [(create_base_field_name env n t,
- JUSTBASE, [], loc),
+ ([SpecType (Tstruct (cname, None, []))],
+ [(create_base_field_name env n t, JUSTBASE, [], loc),
None]),
(create_class_type
inherits.base inherits.templated_kind))
@@ -2716,7 +2677,7 @@ let make_class_decl env name tkind kind inherits fields body has_virtual =
(List.fold_left create_field ([],[])
(List.append fields inherited_fields))
in
- let bare = bare_qname name in
+ let bare = bare_qname n in
let env = Convert_env.add_aggregate env bare CClass tkind false in
Some bcfields,
Convert_env.add_struct env (bare,tkind) bfields_typ
@@ -2732,7 +2693,8 @@ let make_class_decl env name tkind kind inherits fields body has_virtual =
match bare_fields, kind with
| None, _ | Some _, CUnion -> None
| Some fields, (CClass | CStruct) ->
- Some (Tstruct (Mangling.mangle (bare_qname n) t None, Some fields,[]))
+ let bare_name = convert_class_name new_env (bare_qname n) t in
+ Some (Tstruct (bare_name, Some fields,[]))
in
let bare_class_decl = match bare_type_decl with
| None -> None
diff --git a/tests/class/extern_c_class.cpp b/tests/class/extern_c_class.cpp
index 4af141d8c3daa5144f4c31b05ba9a1f4bb19e94d..14aa138321062005f75db113977d452c1d4d4760 100644
--- a/tests/class/extern_c_class.cpp
+++ b/tests/class/extern_c_class.cpp
@@ -1,6 +1,7 @@
extern "C"{
class C {
- void set(int* t) { *t = get_x(); }
+ void set(int* t) { *t = get_x(); foo(); }
int get_x() { return 0; }
+ virtual void foo();
};
}
diff --git a/tests/class/oracle/extern_c_class.res.oracle b/tests/class/oracle/extern_c_class.res.oracle
index ba5027bb2f3823f38afce26d80dafa0b75ca5a7f..900abea7d405005a2a08a4af3b4e6bd23aae9488 100644
--- a/tests/class/oracle/extern_c_class.res.oracle
+++ b/tests/class/oracle/extern_c_class.res.oracle
@@ -1,9 +1,37 @@
[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);
@@ -12,9 +40,240 @@ 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;