diff --git a/Makefile.generating b/Makefile.generating index 4bb84658c1e3b8af259d9d5b07bdc79bc94b74da..063b2a11c935ee006b665873de86ae0995a70c8f 100644 --- a/Makefile.generating +++ b/Makefile.generating @@ -85,6 +85,7 @@ $(CONFIG_FILE): $(CONFIG_FILE).in VERSION share/Makefile.config Makefile.generat -e "s|@FRAMAC_DEFAULT_CPP@|$(FRAMAC_DEFAULT_CPP)|" \ -e "s|@FRAMAC_GNU_CPP@|$(FRAMAC_GNU_CPP)|" \ -e "s|@DEFAULT_CPP_KEEP_COMMENTS@|$(DEFAULT_CPP_KEEP_COMMENTS)|" \ + -e "s|@DEFAULT_CPP_SUPPORTED_ARCH_OPTS@|$(DEFAULT_CPP_SUPPORTED_ARCH_OPTS)|" \ -e "s|@STATIC_PLUGINS@|$(STATIC_PLUGINS)|" \ -e "s|@STATIC_GUI_PLUGINS@|$(STATIC_GUI_PLUGINS)|" \ -e "s|@COMPILATION_UNITS@|$(COMPILATION_UNITS)|" \ diff --git a/configure.in b/configure.in index cbdd6db773604566b92fa35ebbf73605cd6b77c8..5b1ec3eca26669e550393026973a1cf82e8c979c 100644 --- a/configure.in +++ b/configure.in @@ -528,6 +528,38 @@ AC_ARG_WITH( AC_MSG_RESULT(Default preprocessor is '$FRAMAC_DEFAULT_CPP'.) + +# Test if preprocessor supports options such as -m16/-m32/-m64 + +DEFAULT_CPP_SUPPORTED_ARCH_OPTS= + +rm -f conftest.i +CPPFLAGS="-m32" +AC_PREPROC_IFELSE( + [AC_LANG_SOURCE([/* Check if preprocessor supports option -m32 */])], + [if test -e conftest.i; then + DEFAULT_CPP_SUPPORTED_ARCH_OPTS+='\"-m32\"; '; + fi], []) + +rm -f conftest.i +CPPFLAGS="-m64" +AC_PREPROC_IFELSE( + [AC_LANG_SOURCE([/* Check if preprocessor supports option -m64 */])], + [if test -e conftest.i; then + DEFAULT_CPP_SUPPORTED_ARCH_OPTS+='\"-m64\"; '; + fi], []) + +rm -f conftest.i +CPPFLAGS="-m16" +AC_PREPROC_IFELSE( + [AC_LANG_SOURCE([/* Check if preprocessor supports option -m16 */])], + [if test -e conftest.i; then + DEFAULT_CPP_SUPPORTED_ARCH_OPTS+='\"-m16\"; '; + fi], []) + +AC_MSG_RESULT(Default preprocessor supported architecture-related options: $DEFAULT_CPP_SUPPORTED_ARCH_OPTS) + + ################# # Plugin wished # ################# @@ -954,6 +986,7 @@ AC_SUBST(CYCLES_PER_USEC) AC_SUBST(LOCAL_MACHDEP) AC_SUBST(datarootdir) AC_SUBST(FRAMAC_DEFAULT_CPP) +AC_SUBST(DEFAULT_CPP_SUPPORTED_ARCH_OPTS) AC_SUBST(FRAMAC_GNU_CPP) AC_SUBST(DEFAULT_CPP_KEEP_COMMENTS) AC_SUBST(CC) diff --git a/share/Makefile.config.in b/share/Makefile.config.in index e254ddc93d9e265b9f01007d1590030a914ee741..0f2a08ce440b5dfd3887f0eb13627db7c1be69ae 100644 --- a/share/Makefile.config.in +++ b/share/Makefile.config.in @@ -50,6 +50,7 @@ EMACS_DATADIR ?=$(DATADIR)/emacs/site-lisp FRAMAC_DEFAULT_CPP ?=@FRAMAC_DEFAULT_CPP@ FRAMAC_GNU_CPP ?=@FRAMAC_GNU_CPP@ DEFAULT_CPP_KEEP_COMMENTS?=@DEFAULT_CPP_KEEP_COMMENTS@ +DEFAULT_CPP_SUPPORTED_ARCH_OPTS?=@DEFAULT_CPP_SUPPORTED_ARCH_OPTS@ CC =@CC@ ############### diff --git a/src/kernel_internals/runtime/config.ml.in b/src/kernel_internals/runtime/config.ml.in index 9fa1d0a2938ef66f15924018d2ebc87d5197e014..a44de6874d79e78c43a3d49281c0de1d430341a5 100644 --- a/src/kernel_internals/runtime/config.ml.in +++ b/src/kernel_internals/runtime/config.ml.in @@ -58,6 +58,8 @@ let preprocessor = let preprocessor_is_gnu_like = try ignore (Sys.getenv "CPP"); false with Not_found -> @FRAMAC_GNU_CPP@ +let preprocessor_supported_arch_options = [@DEFAULT_CPP_SUPPORTED_ARCH_OPTS@] + let preprocessor_keep_comments = try (ignore (Sys.getenv "CPP"); true) with Not_found -> @DEFAULT_CPP_KEEP_COMMENTS@ diff --git a/src/kernel_internals/runtime/config.mli b/src/kernel_internals/runtime/config.mli index bff595458dcf74c735097ddb3ace295734f4f179..95a80251b1d252491cfd57dc95743cc29a2a5bba 100644 --- a/src/kernel_internals/runtime/config.mli +++ b/src/kernel_internals/runtime/config.mli @@ -81,6 +81,13 @@ val preprocessor_is_gnu_like: bool @since Sodium-20150201 *) +val preprocessor_supported_arch_options: string list + (** architecture-related options (e.g. -m32) known to be supported by + the default preprocessor. Used to match preprocessor commands to + selected machdeps. + @since Frama-C+dev + *) + val preprocessor_keep_comments: bool (** [true] if the default preprocessor selected during compilation is able to keep comments (hence ACSL annotations) in its output. diff --git a/src/kernel_internals/runtime/machdeps.ml b/src/kernel_internals/runtime/machdeps.ml index a77f65ef77b1090d2d58dc5a507f2daf676314cd..2af5207078362f34eceb04db8a61af5f37e79098 100644 --- a/src/kernel_internals/runtime/machdeps.ml +++ b/src/kernel_internals/runtime/machdeps.ml @@ -47,6 +47,7 @@ let x86_16 = { version = "x86 16 bits mode (gcc like compiler) with big or huge memory model"; compiler = "generic"; + cpp_arch_flags = ["-m16"]; sizeof_short = 2; sizeof_int = 2; sizeof_long = 4; @@ -86,6 +87,7 @@ let gcc_x86_16 = { x86_16 with compiler = "gcc" } let x86_32 = { version = "gcc 4.0.3 - X86-32bits mode"; compiler = "generic"; + cpp_arch_flags = ["-m32"]; sizeof_short = 2; sizeof_int = 4; sizeof_long = 4; @@ -123,6 +125,7 @@ let gcc_x86_32 = { x86_32 with compiler = "gcc" } let x86_64 = { version = "gcc 4.0.3 AMD64"; compiler = "generic"; + cpp_arch_flags = ["-m64"]; sizeof_short = 2; sizeof_int = 4; sizeof_long = 8; @@ -160,6 +163,7 @@ let gcc_x86_64 = { x86_64 with compiler = "gcc" } let ppc_32 = { version = "4.0.1 (Apple Computer, Inc. build 5367)"; compiler = "standard"; + cpp_arch_flags = ["-m32"]; sizeof_short = 2; sizeof_int = 4; sizeof_long = 4; @@ -195,6 +199,7 @@ let ppc_32 = { let msvc_x86_64 = { version = "MSVC - X86-64bits mode"; compiler = "msvc"; + cpp_arch_flags = ["-m64"]; sizeof_short = 2; sizeof_int = 4; sizeof_long = 4; diff --git a/src/kernel_services/ast_data/cil_types.mli b/src/kernel_services/ast_data/cil_types.mli index 331057aef902514fb62f45babc56561d86766519..27c1664773ee35eff2453c12bd244d5257686302 100644 --- a/src/kernel_services/ast_data/cil_types.mli +++ b/src/kernel_services/ast_data/cil_types.mli @@ -1765,6 +1765,8 @@ type mach = { __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 + the preprocessor (if supported) *) version: string; (* Information on this machdep *) } diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml index 05adaed0f2162e9d95d71f80ac1c0d86b81e3301..ac7fb7ceca4f060173fa2f1cfa9494e31a72cb94 100644 --- a/src/kernel_services/ast_queries/file.ml +++ b/src/kernel_services/ast_queries/file.ml @@ -439,6 +439,25 @@ let parse_cabs = function else add_if_gnu "-nostdinc" in let define_args = "__FRAMAC__" :: define_args in + (* Hypothesis: the preprocessor does support the arch-related + options tested when 'configure' was run. *) + let required_cpp_arch_args = (get_machdep ()).cpp_arch_flags in + let supported_cpp_arch_args, unsupported_cpp_arch_args = + List.partition (fun arg -> + List.mem arg Config.preprocessor_supported_arch_options) + required_cpp_arch_args + in + if unsupported_cpp_arch_args <> [] then + Kernel.warning ~once:true + "your preprocessor is not known to handle option(s) `%a', \ + considered necessary for machdep `%s'. To ensure compatibility \ + between your preprocessor and the machdep, consider using \ + -cpp-command with the appropriate flags. \ + Your preprocessor is known to support these flags: %a" + (Pretty_utils.pp_list ~sep:" " Format.pp_print_string) + unsupported_cpp_arch_args (Kernel.Machdep.get ()) + (Pretty_utils.pp_list ~sep:" " Format.pp_print_string) + Config.preprocessor_supported_arch_options; let extra_args = if Kernel.ReadAnnot.get () then if Kernel.PreprocessAnnot.is_set () then @@ -459,7 +478,7 @@ let parse_cabs = function in let supp_args = string_of_supp_args include_args define_args - (extra_args @ Kernel.CppExtraArgs.get ()) + (extra_args @ Kernel.CppExtraArgs.get () @ supported_cpp_arch_args) in if Kernel.is_debug_key_enabled dkey_pp then Kernel.feedback ~dkey:dkey_pp @@ -485,8 +504,14 @@ preprocessor command or use the option \"-cpp-command\"." cpp_command "trying to preprocess annotation with an unknown \ preprocessor."; true)) then begin + let pp_annot_supp_args = + Format.asprintf "-nostdinc %a" + (Pretty_utils.pp_list ~sep:" " Format.pp_print_string) + supported_cpp_arch_args + in let ppf' = - try Logic_preprocess.file ".c" (build_cpp_cmd cmdl "-nostdinc") ppf + try Logic_preprocess.file ".c" + (build_cpp_cmd cmdl pp_annot_supp_args) ppf with Sys_error _ as e -> safe_remove_file ppf; Kernel.abort "preprocessing of annotations failed (%s)" diff --git a/tests/misc/custom_machdep/custom_machdep.ml b/tests/misc/custom_machdep/custom_machdep.ml index 3b50162d8a88821d3d8d236cd758ac2030cf3bbb..da8ee8cf9ba794bdadaf45f50673cb83af71dca5 100644 --- a/tests/misc/custom_machdep/custom_machdep.ml +++ b/tests/misc/custom_machdep/custom_machdep.ml @@ -4,6 +4,7 @@ let mach = { version = "foo"; compiler = "bar"; + cpp_arch_flags = []; sizeof_short = 2; sizeof_int = 3; sizeof_long = 4; diff --git a/tests/syntax/machdep_char_unsigned.ml b/tests/syntax/machdep_char_unsigned.ml index e23ac489ab378de867d34a32753097261496d229..494492e8be26863ab7f54f10bae93d75753bbbef 100644 --- a/tests/syntax/machdep_char_unsigned.ml +++ b/tests/syntax/machdep_char_unsigned.ml @@ -4,6 +4,7 @@ open Cil_types let md = { version = ""; compiler = "gcc"; + cpp_arch_flags = ["-m32"]; sizeof_short = 2; sizeof_int = 2; sizeof_long = 4;