diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml index 75eabeeadfde6fa728d4418ccfe7675c45314be2..24962b42cb16fa17057f41fc3fba8917cdb6bdfc 100644 --- a/src/kernel_internals/typing/cabs2cil.ml +++ b/src/kernel_internals/typing/cabs2cil.ml @@ -1346,20 +1346,14 @@ let canDropStatement (s: stmt) : bool = ignore (visitCilStmt vis s); !pRes -let allowed_machdep machdep = - Format.asprintf - "only allowed for %s machdeps;@ see option -machdep or@ \ - run '-machdep help' for the list of available machdeps" - machdep - let fail_if_incompatible_sizeof ~ensure_complete op typ = if Cil.isFunctionType typ && Cil.theMachine.theMachine.sizeof_fun < 0 then Kernel.error ~current:true "%s called on function %s" op - (allowed_machdep "GCC"); + (Cil.allowed_machdep "GCC"); let is_void = Cil.isVoidType typ in if is_void && Cil.theMachine.theMachine.sizeof_void < 0 then Kernel.error ~current:true "%s on void type %s" op - (allowed_machdep "GCC/MSVC"); + (Cil.allowed_machdep "GCC/MSVC"); if ensure_complete && not (Cil.isCompleteType typ) && not is_void then Kernel.error ~current:true "%s on incomplete type '%a'" op Cil_printer.pp_typ typ @@ -3359,7 +3353,7 @@ let rec _pp_preInit fmt = function let empty_preinit() = if Cil.gccMode () || Cil.msvcMode () then CompoundPre (ref (-1), ref [| |]) - else abort_context "empty initializers %s" (allowed_machdep "GCC/MSVC") + else abort_context "empty initializers %s" (Cil.allowed_machdep "GCC/MSVC") (* Set an initializer *) let rec setOneInit this o preinit = @@ -5212,7 +5206,7 @@ and doType (ghost:bool) isFuncArg not (Cil.gccMode () || Cil.msvcMode ()) then Kernel.error ~once:true ~current:true - "zero-length arrays %s" (allowed_machdep "GCC/MSVC"); + "zero-length arrays %s" (Cil.allowed_machdep "GCC/MSVC"); Some len' in let al' = doAttributes ghost al in @@ -5478,7 +5472,7 @@ and makeCompType ghost (isstruct: bool) Kernel.error ~source "field `%s' declared with a type containing a flexible array \ member %s." - n (allowed_machdep "GCC/MSVC") + n (Cil.allowed_machdep "GCC/MSVC") end else if not (Cil.isCompleteType ~allowZeroSizeArrays ftype) then begin @@ -5638,7 +5632,7 @@ and makeCompType ghost (isstruct: bool) Kernel.error ~current:true ~once:true "empty %ss %s" (if comp.cstruct then "struct" else "union") - (allowed_machdep "GCC/MSVC"); + (Cil.allowed_machdep "GCC/MSVC"); List.iter check flds; if comp.cfields <> None then begin let old_fields = Option.get comp.cfields in diff --git a/src/kernel_services/ast_queries/cil.ml b/src/kernel_services/ast_queries/cil.ml index 6c0fad4721f7abdca0b103532ecd9763713e4618..bb05b7899a0f6d831698fc06113d088bda812fc6 100644 --- a/src/kernel_services/ast_queries/cil.ml +++ b/src/kernel_services/ast_queries/cil.ml @@ -171,6 +171,12 @@ let set_acceptEmptyCompinfo () = acceptEmptyCompinfo := true let acceptEmptyCompinfo () = msvcMode () || gccMode () || !acceptEmptyCompinfo +let allowed_machdep machdep = + Format.asprintf + "only allowed for %s machdeps;@ see option -machdep or@ \ + run '-machdep help' for the list of available machdeps" + machdep + let theMachineProject = ref (createMachine ()) module Machine_datatype = diff --git a/src/kernel_services/ast_queries/cil.mli b/src/kernel_services/ast_queries/cil.mli index bb03f8fb2cdf84315404d8dd357e75203c500abb..32bd684f7f20b1382a140f9adf088d42bbf4d68a 100644 --- a/src/kernel_services/ast_queries/cil.mli +++ b/src/kernel_services/ast_queries/cil.mli @@ -118,6 +118,13 @@ val acceptEmptyCompinfo: unit -> bool @since 23.0-Vanadium *) +val allowed_machdep: string -> string +(** [allowed_machdep "machdep family"] provides a standard message for features + only allowed for a particular machdep. + + @since Frama-C+dev +*) + (* ************************************************************************* *) (** {2 Values for manipulating globals} *) (* ************************************************************************* *)