From 77981cdafa6dc5e632c5ca3fe3f238c06eb7c36c Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@m4x.org>
Date: Fri, 13 Mar 2020 11:16:36 +0100
Subject: [PATCH] [conversion] handle clang's ImplicitValueInitExpr

---
 ClangVisitor.cpp                   |  3 +++
 convert.ml                         | 27 +++++++++++++++++++++++++++
 intermediate_format.ast            |  1 +
 tests/basic/oracle/init.res.oracle | 15 +++++++++++++++
 4 files changed, 46 insertions(+)

diff --git a/ClangVisitor.cpp b/ClangVisitor.cpp
index 73c4e65..4192305 100644
--- a/ClangVisitor.cpp
+++ b/ClangVisitor.cpp
@@ -530,6 +530,9 @@ FramacVisitor::makeInitExpr(
       init_expr_Array_init(
         qualified_name_dup(idx), makeLocExpression(init,shouldDelay));
   };
+  if (clang::ImplicitValueInitExpr::classof(init)) {
+    return init_expr_Implicit_init();
+  }
   //TODO: there are other initializer classes.
   //Need to check whether they are used in the elaborated AST.
   // plain expression
diff --git a/convert.ml b/convert.ml
index 87b2355..ff576e3 100644
--- a/convert.ml
+++ b/convert.ml
@@ -1928,6 +1928,32 @@ and convert_initializer env typ var init_exp does_remove_virtual =
         -> Fclang_datatype.Qualified_name.equal (v1,TStandard) (v2,TStandard)
       | _ -> false
   in
+  (* default 0-initialization. *)
+  let rec mk_default_init typ =
+    match typ.plain_type with
+    | Int _ | Enum _ | Pointer _ -> SINGLE_INIT(mk_zero env)
+    | Float _ -> SINGLE_INIT (mk_expr env (CONSTANT(CONST_FLOAT "0.")))
+
+    | LVReference _ | RVReference _ ->
+      Convert_env.fatal env "Unsupported: default initialization of reference"
+    | Lambda _ -> (* could probably be directly assert false *)
+      Convert_env.fatal env
+        "Unsupported: default initialization of lambda object"
+
+    (* initialize at least one element. *)
+   | Array typ ->
+      COMPOUND_INIT [ NEXT_INIT, mk_default_init typ.subtype ]
+    | Struct (s,ts) | Union (s,ts) ->
+      (match Convert_env.get_struct env (s,ts) with
+       | [] -> NO_INIT
+       | (field, typ) :: _ ->
+         COMPOUND_INIT
+           [ INFIELD_INIT(field,NEXT_INIT), mk_default_init typ ])
+
+    | Named (ty,_) when Cxx_utils.is_builtin_qual_type ty -> NO_INIT
+    | Named(ty,_) -> mk_default_init (Convert_env.get_typedef env ty)
+    | Void -> assert false
+  in
   let rec aux_init env typ var = function
     | Single_init init ->
       (match init.econtent with
@@ -1946,6 +1972,7 @@ and convert_initializer env typ var init_exp does_remove_virtual =
           let env, aux, def = convert_full_expr env init does_remove_virtual in
           let def = convert_ref env typ.plain_type def in
           env, aux, SINGLE_INIT def, None)
+    | Implicit_init -> env, [], mk_default_init typ, None
     | Compound_init l ->
       let typed_l = find_type_list env typ.plain_type l in
       let env, aux, init =
diff --git a/intermediate_format.ast b/intermediate_format.ast
index 2bc3f70..fbfeb6a 100644
--- a/intermediate_format.ast
+++ b/intermediate_format.ast
@@ -351,6 +351,7 @@ type case_statement =
    where we still want to know which field initialized. *)
 type init_expr =
   | Single_init { definition: expression; }
+  | Implicit_init { } (* implicit initialization *)
   | Compound_init { init_elts: init_expr list; }
   | Union_init { field: string; field_type: qual_type; definition: init_expr; }
   (* initialization of an array of objects. expression is parameterized by
diff --git a/tests/basic/oracle/init.res.oracle b/tests/basic/oracle/init.res.oracle
index 4ada1c4..31566ce 100644
--- a/tests/basic/oracle/init.res.oracle
+++ b/tests/basic/oracle/init.res.oracle
@@ -26,6 +26,11 @@ struct A {
    int *a ;
    int b ;
 };
+typedef char myArray[10];
+struct myStruct {
+   myArray a ;
+};
+typedef struct myStruct myStruct;
 struct _frama_c_vmt _frama_c_vmt_header;
 struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info;
 
@@ -35,6 +40,16 @@ struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
    .base_classes = (struct _frama_c_rtti_name_info_content *)0,
    .number_of_base_classes = 0,
    .pvmt = (struct _frama_c_vmt *)0};
+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];
+struct _frama_c_rtti_name_info_node _frama_c_rtti_name_info =
+  {.name = "myStruct",
+   .base_classes = (struct _frama_c_rtti_name_info_content *)0,
+   .number_of_base_classes = 0,
+   .pvmt = (struct _frama_c_vmt *)0};
+myStruct s = {.a = {(char)0}};
 int main(void)
 {
   int x = 0;
-- 
GitLab