diff --git a/ClangVisitor.cpp b/ClangVisitor.cpp index 73c4e655d8a3a5742bab9e6d5a2e3ef2a35ef359..4192305f01feeb9914e9664d7238c65c3a439b61 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 87b23551258835df60bdb85b9fd9b9d4d5b471cd..ff576e38ff36c6ef074c64b55fb1c11b9824139f 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 2bc3f70d0d64b59c22f634e4c127368aa79ae461..fbfeb6abae86ecb4450f5512ff5eb5e4c1b5cb69 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 4ada1c4b4f8ca8974c9b2eb56417a1faa34fd7da..31566ce055cb4131e2f53fca19588644acc9e591 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;