diff --git a/src/plugins/value/domains/cvalue/cvalue_init.ml b/src/plugins/value/domains/cvalue/cvalue_init.ml index 063a3ce6fe184d81897d5e9c5a70179699cd4c7c..d5d2316e82804cc3ec461d5d3a4ff2170c1692d9 100644 --- a/src/plugins/value/domains/cvalue/cvalue_init.ml +++ b/src/plugins/value/domains/cvalue/cvalue_init.ml @@ -98,7 +98,7 @@ let create_hidden_base ~libc ~valid ~hidden_var_name ~name_desc pointed_typ = let reject_empty_struct b offset typ = match Cil.unrollType typ with | TComp (ci, _, _) -> - if ci.cfields = Some [] && not (Cil.gccMode () || Cil.msvcMode ()) then + if ci.cfields = Some [] && not (Cil.acceptEmptyCompinfo ()) then Value_parameters.abort ~current:true "@[empty %ss@ are unsupported@ (type '%a',@ location %a%a)@ \ in C99 (only allowed as GCC/MSVC extension).@ Aborting.@]"