diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml index 4ad7be278ca025c73500ba4d94526d29584247e8..5afec74216f15b44be81acd7b1ec3afbae60a540 100644 --- a/src/kernel_internals/typing/cabs2cil.ml +++ b/src/kernel_internals/typing/cabs2cil.ml @@ -3193,23 +3193,31 @@ let rec collectInitializer Cil_datatype.Typ.pretty thistype !pMaxIdx; (* Find the field to initialize *) let rec findField (idx: int) = function - | [] -> Kernel.fatal ~current:true "collectInitializer: union" + | [] -> + (* This code should only be reachable with GCC/MSVC machdeps *) + if Machine.(gccMode () || msvcMode ()) then + [], reads + else + Kernel.fatal ~current:true "collectInitializer: union" | _ :: rest when idx < !pMaxIdx && !pArray.(idx) = NoInitPre -> findField (idx + 1) rest | f :: _ when idx = !pMaxIdx -> let init, reads = collectFieldInitializer reads !pArray.(idx) f ~parenttype:thistype in - (Field(f, NoOffset), init), reads + [ (Field(f, NoOffset), init) ], reads | _ -> abort_context "Can initialize only one field for union" in - if Machine.msvcMode () && !pMaxIdx != 0 then + (* CompoundPre is initialized with pMaxId = -1 for empty compound init + (cf. empty_preinit), so we need to check if it is greater than 0 + instead of different. *) + if Machine.msvcMode () && !pMaxIdx > 0 then Kernel.warning ~current:true "On MSVC we can initialize only the first field of a union"; let init, reads = findField 0 (Option.value ~default:[] comp.cfields) in - CompoundInit (thistype, [ init ]), thistype, reads + CompoundInit (thistype, init), thistype, reads | _ -> Kernel.fatal ~current:true "collectInitializer" diff --git a/src/kernel_services/ast_printing/cil_printer.ml b/src/kernel_services/ast_printing/cil_printer.ml index a229b8c21798ecd925c7171ad3392143198958a8..88f336d80aca5c4a494a12f0a44b862e7736f564 100644 --- a/src/kernel_services/ast_printing/cil_printer.ml +++ b/src/kernel_services/ast_printing/cil_printer.ml @@ -911,7 +911,7 @@ class cil_printer () = object (self) | _ -> Kernel.fatal "Trying to print malformed initializer" in if not (Cil.isArrayType t) then - Pretty_utils.pp_list ~pre:"{@[<hv>" ~sep:",@ " ~suf:"@]}" + Pretty_utils.pp_list ~pre:"{@[<hv>" ~sep:",@ " ~suf:"@]}" ~empty:"{}" designated_init fmt initl else begin let print_index prev_index (designator,init as di) = diff --git a/tests/syntax/empty_union.i b/tests/syntax/empty_union.i new file mode 100644 index 0000000000000000000000000000000000000000..4b656499b0144d7b86bbbad3b9cce0e47f024d67 --- /dev/null +++ b/tests/syntax/empty_union.i @@ -0,0 +1,9 @@ +/* run.config* + STDOPT: +"-machdep gcc_x86_32 -print -ocode @PTEST_NAME@_reparse.c -then @PTEST_NAME@_reparse.c -ocode=''" + STDOPT: +"-machdep msvc_x86_64 -print -ocode @PTEST_NAME@_reparse.c -then @PTEST_NAME@_reparse.c -ocode=''" + EXIT: 1 + STDOPT: + */ + +// based on GCC's 'torture' test suite +union empty {} eu = {}; diff --git a/tests/syntax/oracle/empty_union.0.res.oracle b/tests/syntax/oracle/empty_union.0.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..7d386369f1419cdca1541c94233289478a007fec --- /dev/null +++ b/tests/syntax/oracle/empty_union.0.res.oracle @@ -0,0 +1,8 @@ +[kernel] Parsing empty_union.i (no preprocessing) +[kernel] Parsing empty_union_reparse.c (with preprocessing) +/* Generated by Frama-C */ +union empty { + +}; +union empty eu = {}; + diff --git a/tests/syntax/oracle/empty_union.1.res.oracle b/tests/syntax/oracle/empty_union.1.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..7d386369f1419cdca1541c94233289478a007fec --- /dev/null +++ b/tests/syntax/oracle/empty_union.1.res.oracle @@ -0,0 +1,8 @@ +[kernel] Parsing empty_union.i (no preprocessing) +[kernel] Parsing empty_union_reparse.c (with preprocessing) +/* Generated by Frama-C */ +union empty { + +}; +union empty eu = {}; + diff --git a/tests/syntax/oracle/empty_union.2.res.oracle b/tests/syntax/oracle/empty_union.2.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..c1a338cee3f48e25e391e113fa8142235dbb2f85 --- /dev/null +++ b/tests/syntax/oracle/empty_union.2.res.oracle @@ -0,0 +1,10 @@ +[kernel] Parsing empty_union.i (no preprocessing) +[kernel] empty_union.i:9: User Error: + empty unions only allowed for GCC/MSVC machdeps; see option -machdep or run 'frama-c -machdep help' for the list of available machdeps +[kernel] empty_union.i:9: User Error: + empty initializers only allowed for GCC/MSVC machdeps; see option -machdep or run 'frama-c -machdep help' for the list of available machdeps + 7 + 8 // based on GCC's 'torture' test suite + 9 union empty {} eu = {}; + ^^ +[kernel] Frama-C aborted: invalid user input.