From c353e3caf3ea32c66bc2436b7b1996e6899b2b6f Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Wed, 28 Feb 2024 20:16:12 +0100
Subject: [PATCH] [conversion] C++ classes can live inside extern "C" context
---
convert.ml | 65 +++-----------------
framaCIRGen_src/Clang_utils.cpp | 6 +-
tests/class/oracle/extern_c_class.res.oracle | 25 ++++++++
3 files changed, 34 insertions(+), 62 deletions(-)
diff --git a/convert.ml b/convert.ml
index cc94061e..6196db1e 100644
--- a/convert.ml
+++ b/convert.ml
@@ -2597,7 +2597,10 @@ 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 = Mangling.mangle n t None in
+ let class_name =
+ if Convert_env.is_extern_c env then n.decl_name
+ else Mangling.mangle n t None
+ in
let loc = Convert_env.get_loc env in
let create_class_type base tb =
{ qualifier = []; plain_type = (Struct (base,tb)) }
@@ -3629,9 +3632,10 @@ and convert_class_component (env, implicits, types, fields, others) meth =
:: others))
| CCompound(loc,name,kind,inherits,body,tkind,has_virtual) ->
let new_env = Convert_env.set_loc env loc in
+ let is_extern_c = Convert_env.is_extern_c env in
let qualified_name = Convert_env.qualify new_env name in
let new_env =
- make_class_env new_env (Declaration name) kind tkind false
+ make_class_env new_env (Declaration name) kind tkind is_extern_c
in
let new_env,new_implicits,subtypes,subfields,subothers =
match body with
@@ -3743,7 +3747,8 @@ and convert_class_component (env, implicits, types, fields, others) meth =
and convert_class env name tkind kind inherits body has_virtual =
let qualified_name = make_qualified_name env name in
- let this_env = make_class_env env name kind tkind false in
+ let is_extern_c = Convert_env.is_extern_c env in
+ let this_env = make_class_env env name kind tkind is_extern_c in
let new_env, implicits, types, fields, others =
match body with
| None -> this_env, [], [], [], []
@@ -3775,60 +3780,6 @@ and convert_class env name tkind kind inherits body has_virtual =
List.fold_right add_glob my_implicits |>
Convert_env.reset_current_class
-let rec convert_pod_field (cfields, typs, env) field =
- match field with
- | CFieldDecl(loc, name, typ, bf_info,is_mutable) ->
- let env = Convert_env.set_loc env loc in
- let cloc = Cil_datatype.Location.of_lexing_loc loc in
- let env, (base,decl) = convert_specifiers env typ false in
- let base =
- if is_mutable then
- SpecAttr (add_attr env Cil.frama_c_mutable []) :: base
- else base
- in
- let bf_length = Option.map (convert_bitfield_info env) bf_info in
- FIELD(base, [(name,decl JUSTBASE,[],cloc),bf_length])::cfields,
- (name, typ) :: typs, env
- | CCompound(_, name, kind, _, body, tn, _) ->
- let dname = Declaration name in
- let env = convert_pod env dname kind tn body in
- cfields, typs, env
- | _ ->
- Convert_env.fatal env "Unknown declaration in extern C structure definition"
-
-and convert_pod env name kind tn body =
- let loc = Convert_env.get_loc env in
- let name =
- match name with
- | Declaration name -> name
- | Implementation name -> name.decl_name
- in
- let env =
- Convert_env.add_aggregate env (Cxx_utils.empty_qual name) kind tn true
- in
- let fields, env =
- match body with
- | None -> None, env
- | Some body ->
- let fields, typs, env =
- List.fold_left convert_pod_field ([], [], env) body
- in
- Some (List.rev fields),
- Convert_env.add_struct
- env (Cxx_utils.empty_qual name,tn) (List.rev typs)
- in
- let type_decl =
- match kind with
- | CClass | CStruct -> Tstruct (name, fields, [])
- | CUnion -> Tunion(name, fields,[])
- in
- Convert_env.add_c_global
- env (ONLYTYPEDEF ([SpecType type_decl], loc))
-
-let convert_class env name tkind kind inherits body has_virtual =
- if Convert_env.is_extern_c env then convert_pod env name kind tkind body
- else convert_class env name tkind kind inherits body has_virtual
-
let make_global_cons_init env name init =
let loc = Convert_env.get_loc env in
FUNDEF(None,([SpecType Tvoid; SpecAttr("__constructor__",[])],
diff --git a/framaCIRGen_src/Clang_utils.cpp b/framaCIRGen_src/Clang_utils.cpp
index b671d4ba..0f5b2837 100644
--- a/framaCIRGen_src/Clang_utils.cpp
+++ b/framaCIRGen_src/Clang_utils.cpp
@@ -1692,11 +1692,7 @@ Clang_utils::makePlainType(
tkind templateParameters = NULL;
const char* dec_name = get_aggregate_name(record, &templateParameters);
const clang::DeclContext* ctx = record->getDeclContext();
- qualified_name name;
- if (!isExternCContext(ctx))
- name = makeQualifiedName(ctx,dec_name,record);
- else
- name = qualified_name_cons(NULL, dec_name);
+ qualified_name name = makeQualifiedName(ctx,dec_name,record);
switch (tagKind) {
case clang::TTK_Struct:
case clang::TTK_Class:
diff --git a/tests/class/oracle/extern_c_class.res.oracle b/tests/class/oracle/extern_c_class.res.oracle
index e69de29b..ba5027bb 100644
--- a/tests/class/oracle/extern_c_class.res.oracle
+++ b/tests/class/oracle/extern_c_class.res.oracle
@@ -0,0 +1,25 @@
+[kernel] Parsing extern_c_class.cpp (external front-end)
+Now output intermediate result
+/* Generated by Frama-C */
+struct C {
+
+};
+void set(struct C *this, int *t);
+
+int get_x(struct C *this);
+
+/*@ requires \valid(this); */
+void set(struct C *this, int *t)
+{
+ *t = get_x(this);
+ return;
+}
+
+int get_x(struct C *this)
+{
+ int __retres;
+ __retres = 0;
+ return __retres;
+}
+
+
--
GitLab