From 7f8bf59b75b3a418123b4c5bef5af82144cccfde Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Fri, 20 Sep 2024 09:26:29 +0200
Subject: [PATCH] [kernel] Add a warn error for implicit int like clang and gcc
---
src/kernel_internals/typing/cabs2cil.ml | 6 +++++-
src/kernel_services/plugin_entry_points/kernel.ml | 3 +++
src/kernel_services/plugin_entry_points/kernel.mli | 2 ++
3 files changed, 10 insertions(+), 1 deletion(-)
diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml
index abb0e06bdc..2b0b61cf17 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 792ea61154..03d0e1bec5 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 33076ff8e3..675cfd1021 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
--
GitLab