diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml index abb0e06bdcd170a45fd0b8945af02f66dfa32c1c..2b0b61cf1781ef85b9a34defc8e405abc08675d2 100644 --- a/src/kernel_internals/typing/cabs2cil.ml +++ b/src/kernel_internals/typing/cabs2cil.ml @@ -4199,7 +4199,11 @@ let rec doSpecList loc ghost (suggestedAnonName: string) | [Cabs.Tunsigned; Cabs.Tshort] -> TInt(IUShort, []) | [Cabs.Tunsigned; Cabs.Tshort; Cabs.Tint] -> TInt(IUShort, []) - | [] -> TInt(IInt, []) + | [] -> + Kernel.warning ~current:true ~wkey:Kernel.wkey_implicit_int + "type specifier missing, defaults to 'int'; ISO C99 and later do not \ + support implicit int"; + TInt(IInt, []) | [Cabs.Tint] -> TInt(IInt, []) | [Cabs.Tsigned] -> TInt(IInt, []) | [Cabs.Tsigned; Cabs.Tint] -> TInt(IInt, []) diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml index 792ea61154286dd65b41f44ee1967eb682a259c1..03d0e1bec5084f4b8d47992c33939437bcb70913 100644 --- a/src/kernel_services/plugin_entry_points/kernel.ml +++ b/src/kernel_services/plugin_entry_points/kernel.ml @@ -204,6 +204,9 @@ let () = set_warn_status wkey_jcdb Log.Wonce let wkey_implicit_function_declaration = register_warn_category "typing:implicit-function-declaration" +let wkey_implicit_int = register_warn_category "typing:implicit-int" +let () = set_warn_status wkey_implicit_int Log.Werror + let wkey_no_proto = register_warn_category "typing:no-proto" let wkey_missing_spec = register_warn_category "annot:missing-spec" diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli index 33076ff8e300aa22381f31d9c7e4094044c52b9b..675cfd1021d2948a4c9c9031c0cac99e57e7e03d 100644 --- a/src/kernel_services/plugin_entry_points/kernel.mli +++ b/src/kernel_services/plugin_entry_points/kernel.mli @@ -174,6 +174,8 @@ val wkey_linker_weak: warn_category val wkey_implicit_conv_void_ptr: warn_category +val wkey_implicit_int: warn_category + val wkey_incompatible_types_call: warn_category val wkey_incompatible_pointer_types: warn_category