From e13579fc16685fd41c076842eb98509c69b7ef69 Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Tue, 26 May 2020 11:12:33 +0200
Subject: [PATCH] [Kernel] remove __thread_is_keyword from machdep
---
Makefile.generating | 1 -
config.h.in | 2 --
configure.in | 10 ----------
doc/developer/advance.tex | 1 -
share/Makefile.config.in | 1 -
share/machdep.c | 9 ---------
src/kernel_internals/runtime/machdeps.ml | 5 -----
src/kernel_services/ast_data/cil_types.mli | 1 -
src/kernel_services/ast_printing/cil_types_debug.ml | 3 +--
src/kernel_services/ast_queries/file.ml | 2 --
tests/misc/custom_machdep/custom_machdep.ml | 1 -
tests/misc/oracle/print_machdep.res.oracle | 1 -
tests/syntax/machdep_char_unsigned.ml | 1 -
13 files changed, 1 insertion(+), 37 deletions(-)
diff --git a/Makefile.generating b/Makefile.generating
index 4495a37a663..2e1c0c6c5df 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 50555d91ca2..73665676f86 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 271ec0976f4..284e9f5cea3 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 459e80d888a..637f4624afb 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 89352cdc64f..5b485c09b90 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 43caa42a451..cd0035e3314 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 6372ee26498..3c9da30d575 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 9ad9fdb7a76..386affd6ea5 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 0b4be0a9ac9..bf24ded4942 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 a1635dcd9df..8d061af580a 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 da8ee8cf9ba..8942b2b793a 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 598e0004a09..4902716c8fc 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 494492e8be2..296683fbd7b 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 () =
--
GitLab