diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml index 60437e0033f406a46706e8dc99c1fade04b6fe94..5afec74216f15b44be81acd7b1ec3afbae60a540 100644 --- a/src/kernel_internals/typing/cabs2cil.ml +++ b/src/kernel_internals/typing/cabs2cil.ml @@ -3210,7 +3210,10 @@ let rec collectInitializer | _ -> 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