diff --git a/Makefile.generating b/Makefile.generating
index 4495a37a663d9e7b39f2f11c3aa0af09e2739471..2e1c0c6c5dfc5b3bdb9ca7fc003397c3255386d3 100644
--- a/Makefile.generating
+++ b/Makefile.generating
@@ -116,7 +116,6 @@ $(MACHDEP_PATH)/local_machdep.ml: \
$(ECHO) "}" >>$@
$(ECHO) \
"let gccHas__builtin_va_list = $(HAVE_BUILTIN_VA_LIST)" >>$@
- $(ECHO) "let __thread_is_keyword = $(THREAD_IS_KEYWORD)" >>$@
$(ECHO) \
"$@ generated. You may have this file merged into Frama-C by developers."
$(CHMOD_RO) $@
diff --git a/config.h.in b/config.h.in
index 50555d91ca212376c50d24b65acc856529d1887b..73665676f86fe0110fc5cb25369a8f6e820916a8 100644
--- a/config.h.in
+++ b/config.h.in
@@ -52,6 +52,4 @@
#undef HAVE_BUILTIN_VA_LIST
-#undef THREAD_IS_KEYWORD
-
#undef UNDERSCORE_NAME
diff --git a/configure.in b/configure.in
index 271ec0976f4a495721593b61955409e015f5e5c7..284e9f5cea3280ba307aa6962ea4ad07f207f5ca 100644
--- a/configure.in
+++ b/configure.in
@@ -518,15 +518,6 @@ if test "$HAVE_BUILTIN_VA_LIST" = "true" ;then
AC_DEFINE_UNQUOTED(HAVE_BUILTIN_VA_LIST, 1)
fi
-AC_MSG_CHECKING([if __thread is a keyword])
-AC_COMPILE_IFELSE([AC_LANG_SOURCE([int main(int __thread) { return 0; }])],
- THREAD_IS_KEYWORD=false,
- THREAD_IS_KEYWORD=true)
-AC_MSG_RESULT($THREAD_IS_KEYWORD)
-if test "$THREAD_IS_KEYWORD" = "true" ;then
- AC_DEFINE_UNQUOTED(THREAD_IS_KEYWORD, 1)
-fi
-
# Does gcc add underscores to identifiers to make assembly labels?
# (I think MSVC always does)
AC_MSG_CHECKING([if gcc adds underscores to assembly labels.])
@@ -1001,7 +992,6 @@ AC_SUBST(HAVE_STDLIB_H)
AC_SUBST(HAVE_WCHAR_H)
AC_SUBST(HAVE_PTRDIFF_H)
AC_SUBST(HAVE_BUILTIN_VA_LIST)
-AC_SUBST(THREAD_IS_KEYWORD)
AC_SUBST(UNDERSCORE_NAME)
AC_SUBST(CYCLES_PER_USEC)
AC_SUBST(LOCAL_MACHDEP)
diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex
index 459e80d888a46cb31fd9c2fbb05cf238377adce0..637f4624afb5b34f9af6979fcc083ff52fe96f50 100644
--- a/doc/developer/advance.tex
+++ b/doc/developer/advance.tex
@@ -3399,7 +3399,6 @@ let my_machine =
little_endian = true;
underscore_name = false ;
has__builtin_va_list = true;
- __thread_is_keyword = true;
}
let () = File.new_machdep "my_machine" my_machine
diff --git a/share/Makefile.config.in b/share/Makefile.config.in
index 89352cdc64fde2da3fc8af58ec9bedf9b2c45c0f..5b485c09b90a8ca699170b6a3e6f649d48946a9a 100644
--- a/share/Makefile.config.in
+++ b/share/Makefile.config.in
@@ -149,7 +149,6 @@ EXE ?=@EXE@
# Required by Cil
UNDERSCORE_NAME ?=@UNDERSCORE_NAME@
HAVE_BUILTIN_VA_LIST ?=@HAVE_BUILTIN_VA_LIST@
-THREAD_IS_KEYWORD ?=@THREAD_IS_KEYWORD@
# test directories for ptests configuration
# Non-plugin test directories containing some ML files to compile
diff --git a/share/machdep.c b/share/machdep.c
index 43caa42a4518daa1c158a031c1103d6c9d26ceb3..cd0035e3314d8bf929f5a2902bb0299b65a4a4d1 100644
--- a/share/machdep.c
+++ b/share/machdep.c
@@ -343,15 +343,6 @@ int main() {
#endif
}
- // __thread_is_keyword
- {
-#ifdef THREAD_IS_KEYWORD
- printf("\t __thread_is_keyword = true;\n");
-#else
- printf("\t __thread_is_keyword = false;\n");
-#endif
- }
-
// underscore_name
{
#ifdef UNDERSCORE_NAME
diff --git a/src/kernel_internals/runtime/machdeps.ml b/src/kernel_internals/runtime/machdeps.ml
index 6372ee264983ad85ec8bfa40d2d8b453c181cdc8..3c9da30d57534a6e73ebe343faebe911a21929a6 100644
--- a/src/kernel_internals/runtime/machdeps.ml
+++ b/src/kernel_internals/runtime/machdeps.ml
@@ -79,7 +79,6 @@ let x86_16 = {
little_endian = true;
underscore_name = true ;
has__builtin_va_list = true;
- __thread_is_keyword = true;
}
let gcc_x86_16 = { x86_16 with
@@ -120,7 +119,6 @@ let x86_32 = {
little_endian = true;
underscore_name = false ;
has__builtin_va_list = true;
- __thread_is_keyword = true;
}
let gcc_x86_32 = { x86_32 with
@@ -161,7 +159,6 @@ let x86_64 = {
little_endian = true;
underscore_name = false ;
has__builtin_va_list = true;
- __thread_is_keyword = true;
}
let gcc_x86_64 = { x86_64 with
@@ -202,7 +199,6 @@ let ppc_32 = {
little_endian = false;
underscore_name = false ;
has__builtin_va_list = true;
- __thread_is_keyword = true;
}
let msvc_x86_64 = {
@@ -240,5 +236,4 @@ let msvc_x86_64 = {
little_endian = true;
underscore_name = false ;
has__builtin_va_list = false;
- __thread_is_keyword = false;
}
diff --git a/src/kernel_services/ast_data/cil_types.mli b/src/kernel_services/ast_data/cil_types.mli
index 9ad9fdb7a7684514813a0b79fee5116fcd7ab814..386affd6ea5a7f05d26205a6500e33fda3bfe00d 100644
--- a/src/kernel_services/ast_data/cil_types.mli
+++ b/src/kernel_services/ast_data/cil_types.mli
@@ -1912,7 +1912,6 @@ type mach = {
little_endian: bool; (* whether the machine is little endian *)
alignof_aligned: int (* Alignment of a type with aligned attribute *);
has__builtin_va_list: bool (* Whether [__builtin_va_list] is a known type *);
- __thread_is_keyword: bool (* Whether [__thread] is a keyword *);
compiler: string; (* Compiler being used. Currently recognized names
are 'gcc', 'msvc' and 'generic'. *)
cpp_arch_flags: string list; (* Architecture-specific flags to be given to
diff --git a/src/kernel_services/ast_printing/cil_types_debug.ml b/src/kernel_services/ast_printing/cil_types_debug.ml
index 0b4be0a9ac93ec2a8d93fb8a07047eaf2ff7a62e..bf24ded49429a4dc0425d3d22e954df4c4835082 100644
--- a/src/kernel_services/ast_printing/cil_types_debug.ml
+++ b/src/kernel_services/ast_printing/cil_types_debug.ml
@@ -1058,7 +1058,7 @@ let pp_mach fmt mach =
alignof_ptr=%a;alignof_float=%a;alignof_double=%a;alignof_longdouble=%a;\
alignof_str=%a;alignof_fun=%a;char_is_unsigned=%a;underscore_name=%a;\
const_string_literals=%a;little_endian=%a;alignof_aligned=%a;\
- has__builtin_va_list=%a;__thread_is_keyword=%a;compiler=%a;\
+ has__builtin_va_list=%a;compiler=%a;\
cpp_arch_flags=%a;version=%a}"
pp_int mach.sizeof_short
pp_int mach.sizeof_int
@@ -1089,7 +1089,6 @@ let pp_mach fmt mach =
pp_bool mach.little_endian
pp_int mach.alignof_aligned
pp_bool mach.has__builtin_va_list
- pp_bool mach.__thread_is_keyword
pp_string mach.compiler
(pp_list pp_string) mach.cpp_arch_flags
pp_string mach.version
diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml
index a1635dcd9dfa7ffa5f361137529f12c97e9eabb2..8d061af580a6862e260bb5932843ae6629f7e09e 100644
--- a/src/kernel_services/ast_queries/file.ml
+++ b/src/kernel_services/ast_queries/file.ml
@@ -296,8 +296,6 @@ let print_machdep fmt (m : Cil_types.mach) =
(if m.underscore_name then "have" else "have no") ;
Format.fprintf fmt " compiler %s builtin __va_list@\n"
(if m.has__builtin_va_list then "has" else "has not") ;
- Format.fprintf fmt " compiler %s __head as a keyword@\n"
- (if m.__thread_is_keyword then "uses" else "does not use") ;
end
module DatatypeMachdep = Datatype.Make_with_collections(struct
diff --git a/tests/misc/custom_machdep/custom_machdep.ml b/tests/misc/custom_machdep/custom_machdep.ml
index da8ee8cf9ba794bdadaf45f50673cb83af71dca5..8942b2b793acec940637c3194d331047d15762dd 100644
--- a/tests/misc/custom_machdep/custom_machdep.ml
+++ b/tests/misc/custom_machdep/custom_machdep.ml
@@ -34,7 +34,6 @@ let mach =
little_endian = true;
underscore_name = false ;
has__builtin_va_list = true;
- __thread_is_keyword = true;
}
let mach2 = { mach with compiler = "baz" }
diff --git a/tests/misc/oracle/print_machdep.res.oracle b/tests/misc/oracle/print_machdep.res.oracle
index 598e0004a0994ab05684b08dbc8412a5f4b96979..4902716c8fc08e7971dd7cee455314ab41f65599 100644
--- a/tests/misc/oracle/print_machdep.res.oracle
+++ b/tests/misc/oracle/print_machdep.res.oracle
@@ -17,4 +17,3 @@ Machine: gcc 4.0.3 - X86-32bits mode
strings are const chars
assembly names have no leading '_'
compiler has builtin __va_list
- compiler uses __head as a keyword
diff --git a/tests/syntax/machdep_char_unsigned.ml b/tests/syntax/machdep_char_unsigned.ml
index 494492e8be26863ab7f54f10bae93d75753bbbef..296683fbd7b36ade780bc74482aff8e5d99758f9 100644
--- a/tests/syntax/machdep_char_unsigned.ml
+++ b/tests/syntax/machdep_char_unsigned.ml
@@ -34,7 +34,6 @@ let md = {
wchar_t = "int";
ptrdiff_t = "int";
has__builtin_va_list = true;
- __thread_is_keyword = false;
}
let () =