diff --git a/src/kernel_internals/typing/cabs2cil.ml b/src/kernel_internals/typing/cabs2cil.ml index de0e67072492daa5af65815d4cff643da90a7455..2b0157f69b5bb35fd22301b642da63030e968430 100644 --- a/src/kernel_internals/typing/cabs2cil.ml +++ b/src/kernel_internals/typing/cabs2cil.ml @@ -4812,6 +4812,14 @@ and makeVarInfoCabs we do it afterwards *) bt (A.PARENTYPE(attrs, ndt, a)) in (*Format.printf "Got yp:%a->%a(%a)@." d_type bt d_type vtype d_attrlist nattr;*) + if hasAttribute "thread" nattr then begin + let wkey = Kernel.wkey_inconsistent_specifier in + let source = fst ldecl in + if isFunctionType vtype then + Kernel.warning ~wkey ~source "only objects can be thread-local" + else if not isglobal && (sto = NoStorage || sto = Register) then + Kernel.warning ~wkey ~source "a local object cannot be thread-local"; + end; if not isgenerated && ghost then begin if hasAttribute "ghost" (Cil.typeAttrs vtype) then Kernel.warning @@ -9125,6 +9133,11 @@ and doDecl local_env (isglobal: bool) : A.definition -> chunk = function let ftyp, funattr = doType local_env.is_ghost false (AttrName false) bt (A.PARENTYPE(attrs, dt, a)) in + if hasAttribute "thread" funattr then begin + let wkey = Kernel.wkey_inconsistent_specifier in + let source = fst funloc in + Kernel.warning ~wkey ~source "only objects can be thread-local" + end; (* Format.printf "Attrs are %a@." d_attrlist funattr; *) Cil.update_var_type !currentFunctionFDEC.svar ftyp; !currentFunctionFDEC.svar.vattr <- funattr; diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml index 1590e44022fb7b4c9423c25c5137d9f268c5ea17..b04db28560cb2e38bb2fd136496910bc62468cb7 100644 --- a/src/kernel_services/plugin_entry_points/kernel.ml +++ b/src/kernel_services/plugin_entry_points/kernel.ml @@ -156,6 +156,9 @@ let wkey_incompatible_types_call = let wkey_incompatible_pointer_types = register_warn_category "typing:incompatible-pointer-types" +let wkey_inconsistent_specifier = + register_warn_category "typing:inconsistent-specifier" + let wkey_int_conversion = register_warn_category "typing:int-conversion" diff --git a/src/kernel_services/plugin_entry_points/kernel.mli b/src/kernel_services/plugin_entry_points/kernel.mli index d39ea5ecc84ccf582c169925714bb6f935de2049..c9dae9c7fd2a8eb422b6976f2bce1c8bf15cf982 100644 --- a/src/kernel_services/plugin_entry_points/kernel.mli +++ b/src/kernel_services/plugin_entry_points/kernel.mli @@ -153,6 +153,8 @@ val wkey_incompatible_types_call: warn_category val wkey_incompatible_pointer_types: warn_category +val wkey_inconsistent_specifier: warn_category + val wkey_int_conversion: warn_category val wkey_cert_exp_46: warn_category diff --git a/tests/syntax/oracle/thread.res.oracle b/tests/syntax/oracle/thread.res.oracle index 8d43c550e321296cff6ae5af57f6241b748fd96f..057e0bcc95de15188f4e85ddaa6cb038c86be9b7 100644 --- a/tests/syntax/oracle/thread.res.oracle +++ b/tests/syntax/oracle/thread.res.oracle @@ -1,13 +1,33 @@ [kernel] Parsing tests/syntax/thread.i (no preprocessing) +[kernel:typing:inconsistent-specifier] tests/syntax/thread.i:10: Warning: + only objects can be thread-local +[kernel:typing:inconsistent-specifier] tests/syntax/thread.i:12: Warning: + only objects can be thread-local +[kernel:typing:inconsistent-specifier] tests/syntax/thread.i:15: Warning: + a local object cannot be thread-local +[kernel:typing:inconsistent-specifier] tests/syntax/thread.i:17: Warning: + a local object cannot be thread-local /* Generated by Frama-C */ __thread int a; static __thread int b; extern __thread int c; _Thread_local int d; + _Thread_local int bad(void); +int bad(void) +{ + int __retres; + __retres = 0; + return __retres; +} + +int main(void); + int main(void) { int __retres; + _Thread_local int e = 1; + register _Thread_local int g = 1; a = 0; b = 0; c = 0; diff --git a/tests/syntax/thread.i b/tests/syntax/thread.i index 209b26f890d3076ac0a21216a81f48964b3be06a..9cbb150145707a58775d960f1efada95ef0b9d1c 100644 --- a/tests/syntax/thread.i +++ b/tests/syntax/thread.i @@ -7,7 +7,14 @@ static __thread int b; extern __thread int c; _Thread_local int d; +_Thread_local int bad() { return 0; } // KO + +_Thread_local int bad_also(void); // KO + int main() { + _Thread_local int e = 1; // KO: e is neither extern nor static + static _Thread_local int f = 0; // OK + register _Thread_local int g = 1; // KO a = 0; b = 0; c = 0;