diff --git a/Changelog b/Changelog index 20f4f6bdef5a3eb46e105237bc74831958f8148e..892d650d80158cde698d85e81a976e8c6e8c85c9 100644 --- a/Changelog +++ b/Changelog @@ -18,6 +18,8 @@ Open Source Release <next-release> ############################################################################### +-! Kernel [2025-02-04] Undefine some predefined GCC macros, to minimize + parsing errors due to unsupported compiler extensions. o! Kernel [2025-01-31] Use a record to represent `Cil_types.typ` with two fields `tnode` and `tattr` for its `typ_node` and `attributes`. - Ivette [2025-01-23] New sidebar listing functions and global variables diff --git a/doc/userman/user-sources.tex b/doc/userman/user-sources.tex index 78536cb5ac2052e404ab9fe57bafaf0422fb0442..f938c1e83c1cbe4f66096e4103079111b6be507b 100644 --- a/doc/userman/user-sources.tex +++ b/doc/userman/user-sources.tex @@ -576,9 +576,10 @@ By default, \FramaC's preprocessing will include the headers of its own standard library, instead of those installed in the user's machine. This avoids issues with non-portable, compiler-specific features. Option \optiondef{-}{frama-c-stdlib} (set by default) -adds \verb+-I$(frama-c-config -print-share-path)/libc+ to the preprocessor command, as well as -GCC-specific option \texttt{-nostdinc}. If the latter is not recognized by -your preprocessor, +adds \verb+-I$(frama-c-config -print-share-path)/libc+ to the preprocessor +command, as well as some GCC-specific options, including (but not limited to) +\texttt{-dD}, \texttt{-nostdinc}, \texttt{-undef}, and some \texttt{-Wno-*} +options. If any of these if not accepted by your preprocessor, \optionuse{-}{no-cpp-frama-c-compliant} can be given to \FramaC (see section~\ref{sec:preprocessing}). diff --git a/src/kernel_internals/runtime/machdep.ml b/src/kernel_internals/runtime/machdep.ml index 08f75663020ed65e68eb4001d6b54b5bdf9c2fae..6bfdcb6d6c0dff8ea3630aa2bcf1f18526f6cd68 100644 --- a/src/kernel_internals/runtime/machdep.ml +++ b/src/kernel_internals/runtime/machdep.ml @@ -301,9 +301,12 @@ let gen_define_macro fmt macro def = else gen_define_string fmt macro def let gen_define_custom_macros fmt censored key_values = + let is_same_macro m1 m2 = + Extlib.strip_underscore m1 = Extlib.strip_underscore m2 + in List.iter (fun (k,v) -> - if not (Datatype.String.Set.mem (Extlib.strip_underscore k) censored) + if not (Datatype.String.Set.exists (is_same_macro k) censored) then begin gen_undef fmt k; gen_define_macro fmt k v @@ -613,7 +616,7 @@ let gen_all_defines fmt ?(censored_macros=Datatype.String.Set.empty) mach = Format.fprintf fmt "#endif // __FC_MACHDEP@\n" let generate_machdep_header ?censored_macros mach = - let debug = Kernel.(is_debug_key_enabled dkey_pp) in + let debug = Kernel.(is_debug_key_enabled dkey_pp_keep_temp_files) in let temp = Extlib.temp_dir_cleanup_at_exit ~debug "__fc_machdep" in let file = Filepath.Normalized.concat temp "__fc_machdep.h" in let chan = open_out (file:>string) in diff --git a/src/kernel_services/ast_queries/file.ml b/src/kernel_services/ast_queries/file.ml index c663a3524be9a06e90368079348babefd3c96916..a4b373292a0d60c7edd9b9109bf0f3ac2a16a81d 100644 --- a/src/kernel_services/ast_queries/file.ml +++ b/src/kernel_services/ast_queries/file.ml @@ -330,10 +330,21 @@ let get_machdep () = | Error (`Msg s) -> Kernel.abort "Error during machdep parsing: %s" s +(* Macros that are defined by gcc even in presence of -undef. + Specifically use -U on the command line to silence them. +*) +let unsupported_libc_macros = + [ + "__STDC_IEC_559_COMPLEX__"; + "__STDC_IEC_60559_COMPLEX__"; + "__STDC_ISO_10646__"; + "__STDC_UTF16__"; + "__STDC_UTF32__"; + ] let unsupported_float_type_macros acc name = List.fold_left - (fun acc s -> Datatype.String.Set.add (name ^ "_" ^ s) acc) + (fun acc s -> Datatype.String.Set.add ("__" ^ name ^ "_" ^ s ^ "__") acc) acc [ "DECIMAL_DIG"; "DENORM_MIN"; "DIG"; "HAS_DENORM"; "HAS_INFINITY"; "HAS_QUIET_NAN"; "IS_IEC_60559"; "MANT_DIG"; @@ -348,7 +359,10 @@ let unsupported_float_types = [ "BFLT16"; "FLT16"; "FLT128"; "LDBL"; ] let known_bad_macros = - Datatype.String.Set.add_seq (List.to_seq ["SIZEOF_INT128"; "SSE" ]) + Datatype.String.Set.add_seq + (List.to_seq + (["__GCC_IEC_559_COMPLEX"; "__SIZEOF_INT128__"; "__SSE__"; "__SSE2__" ] + @ unsupported_libc_macros)) unsupported_float_types let print_machdep_header () = @@ -505,6 +519,10 @@ let build_cpp_cmd = function if Kernel.FramaCStdLib.get() then add_if_gnu "-nostdinc" else [] in + let no_builtin_macros = + if Kernel.FramaCStdLib.get () then add_if_gnu "-undef" + else [] + in let output_defines_arg = let open Kernel in match ReadAnnot.get (), PreprocessAnnot.is_set (), PreprocessAnnot.get () with @@ -513,17 +531,22 @@ let build_cpp_cmd = function | true, false, _ -> add_if_gnu "-dD" | _, _, _ -> [] in - let gnu_implicit_args = output_defines_arg @ nostdinc_arg in - let string_of_supp_args extra includes defines = - Format.asprintf "%s%s%s" + let gnu_implicit_args = + output_defines_arg @ nostdinc_arg @ no_builtin_macros + in + let string_of_supp_args extra includes undef defines = + Format.asprintf "%s%s%s%s" (concat_strs ~pre:"-I" ~sep:" -I" includes) + (concat_strs ~pre:" -U" ~sep:" -U" undef) (concat_strs ~pre:" -D" ~sep:" -D" defines) (concat_strs ~pre:" " ~sep:" " extra) in let supp_args = string_of_supp_args (gnu_implicit_args @ machdep_no_warn @ clang_no_warn @ extra_args) - fc_include_args fc_define_args + fc_include_args + unsupported_libc_macros + fc_define_args in let cpp_command = replace_in_cpp_cmd cmdl supp_args (f:>string) (ppf:>string) diff --git a/tests/misc/pragma-pack-utils.h b/tests/misc/pragma-pack-utils.h index 25eb46802e58b831cf7aee0aa576fca0e4a82156..c0aaa11f60fa123cc9fae10bad0863a4fcc6bf7d 100644 --- a/tests/misc/pragma-pack-utils.h +++ b/tests/misc/pragma-pack-utils.h @@ -9,13 +9,11 @@ // Some versions of MSVC do not accept the '%z' modifier, but GCC emits warnings // without it, so use this macro to print it in both compilers. -// Note that __GNUC__ is defined in our machdep MSVC, but not in the actual -// MSVC compiler itself. -#ifdef __GNUC__ +#if defined(__GNUC__) || defined(__FRAMAC__) // GCC uses %zu for size_t, and allows unicode # define ZU "%zu" # define IN "∈" -#else +#else // actual MSVC compilation // MSVC uses %u for size_t, and does not allow unicode # define ZU "%u" # define IN "IN" diff --git a/tests/misc/pragma-pack.c b/tests/misc/pragma-pack.c index 4534d32c430d1c7bcaf4157ac811eab8d96fafb2..c0f25a35af0d4c11fe79584fc1c3b7705a9025de 100644 --- a/tests/misc/pragma-pack.c +++ b/tests/misc/pragma-pack.c @@ -31,7 +31,7 @@ // test functions are declared here to minimize shifting oracles in case of changes void tests1(void); void tests2(void); -#ifdef __GNUC__ +#if defined(__GNUC__) || defined(__FRAMAC__) // This main function is not used when testing MSVC on Visual C++; // instead, _tmain (defined at the end) is used int main() { @@ -340,7 +340,7 @@ typedef struct { } barcode_bmp_t; #pragma pack(pop) -#ifndef __GNUC__ +#if !defined(__GNUC__) && !defined(__FRAMAC__) // For MSVC testing on Visual C++ int _tmain(int argc, _TCHAR* argv[]) { tests1(); diff --git a/tests/spec/oracle/preprocess_string.res.oracle b/tests/spec/oracle/preprocess_string.res.oracle index ea37c11725bdad4a629e92e33d92c26f9703b091..a63a3bf75a03cfe040c57ae45e7fe9cb54f49d52 100644 --- a/tests/spec/oracle/preprocess_string.res.oracle +++ b/tests/spec/oracle/preprocess_string.res.oracle @@ -1,4 +1,5 @@ [kernel] Warning: your preprocessor is not known to handle option `-nostdinc'. If preprocessing fails because of it, please add -no-cpp-frama-c-compliant option to Frama-C's command-line. If you do not want to see this warning again, explicitly use option -cpp-frama-c-compliant. +[kernel] Warning: your preprocessor is not known to handle option `-undef'. If preprocessing fails because of it, please add -no-cpp-frama-c-compliant option to Frama-C's command-line. If you do not want to see this warning again, explicitly use option -cpp-frama-c-compliant. [kernel] Parsing preprocess_string.c (with preprocessing) /* Generated by Frama-C */ /*@ ensures *("/*" + 0) ≡ '/'; */ diff --git a/tests/syntax/censored_macros.c b/tests/syntax/censored_macros.c new file mode 100644 index 0000000000000000000000000000000000000000..d56fa08a68f62bd1427d93dd994d3c61701059a0 --- /dev/null +++ b/tests/syntax/censored_macros.c @@ -0,0 +1,5 @@ +#ifdef __SIZEOF_INT128__ +#error SHOULD BE BLACKLISTED +#endif + +int main () { } diff --git a/tests/syntax/cpp-command.t/run.t b/tests/syntax/cpp-command.t/run.t index 0acf9e13b4d9f599d025623e75916f0a8ba8efbf..d662536dea83ff20e9ad2283faa9355f0482d8b6 100644 --- a/tests/syntax/cpp-command.t/run.t +++ b/tests/syntax/cpp-command.t/run.t @@ -3,11 +3,11 @@ $ frama-c -check -no-autoload-plugins cpp-command.c -machdep x86_32 -cpp-frama-c-compliant -cpp-command "echo [\$(basename '%1') \$(basename '%1') \$(basename '%i') \$(basename '%input')] ['%2' '%2' '%o' '%output'] ['%args']" | python3 filter.py [kernel] Parsing cpp-command.c (with preprocessing) - [cpp-command.c cpp-command.c cpp-command.c cpp-command.c] [<TMPDIR/PP>.i <TMPDIR/PP>.i <TMPDIR/PP>.i <TMPDIR/PP>.i] [-I<TMP_MACHDEP> -I$FRAMAC_SHARE/libc -D__FRAMAC__ -dD -nostdinc] + [cpp-command.c cpp-command.c cpp-command.c cpp-command.c] [<TMPDIR/PP>.i <TMPDIR/PP>.i <TMPDIR/PP>.i <TMPDIR/PP>.i] [-I<TMP_MACHDEP> -I$FRAMAC_SHARE/libc -U__STDC_IEC_559_COMPLEX__ -U__STDC_IEC_60559_COMPLEX__ -U__STDC_ISO_10646__ -U__STDC_UTF16__ -U__STDC_UTF32__ -D__FRAMAC__ -dD -nostdinc -undef] $ frama-c -check -no-autoload-plugins cpp-command.c -machdep x86_32 -cpp-frama-c-compliant -cpp-command "echo %%1 = \$(basename '%1') %%2 = '%2' %%args = '%args'" | python3 filter.py [kernel] Parsing cpp-command.c (with preprocessing) - %1 = cpp-command.c %2 = <TMPDIR/PP>.i %args = -I<TMP_MACHDEP> -I$FRAMAC_SHARE/libc -D__FRAMAC__ -dD -nostdinc + %1 = cpp-command.c %2 = <TMPDIR/PP>.i %args = -I<TMP_MACHDEP> -I$FRAMAC_SHARE/libc -U__STDC_IEC_559_COMPLEX__ -U__STDC_IEC_60559_COMPLEX__ -U__STDC_ISO_10646__ -U__STDC_UTF16__ -U__STDC_UTF32__ -D__FRAMAC__ -dD -nostdinc -undef $ frama-c -check -no-autoload-plugins cpp-command.c -machdep x86_32 -cpp-frama-c-compliant -cpp-command "printf \"%s\n\" \"using \\% has no effect : \$(basename \"\%input\")\"" [kernel] Parsing cpp-command.c (with preprocessing) @@ -19,7 +19,7 @@ $ frama-c -check -no-autoload-plugins cpp-command.c -machdep x86_32 -print-cpp-commands | python3 filter.py [kernel] Preprocessing command: - gcc -E -C -I<TMP_MACHDEP> -I$FRAMAC_SHARE/libc -D__FRAMAC__ -dD -nostdinc -Wno-builtin-macro-redefined -Wno-unknown-warning-option '$TESTCASE_ROOT/cpp-command.c' -o '<TMPDIR/PP>.i' + gcc -E -C -I<TMP_MACHDEP> -I$FRAMAC_SHARE/libc -U__STDC_IEC_559_COMPLEX__ -U__STDC_IEC_60559_COMPLEX__ -U__STDC_ISO_10646__ -U__STDC_UTF16__ -U__STDC_UTF32__ -D__FRAMAC__ -dD -nostdinc -undef -Wno-builtin-macro-redefined -Wno-unknown-warning-option '$TESTCASE_ROOT/cpp-command.c' -o '<TMPDIR/PP>.i' $ frama-c -check -no-autoload-plugins cpp-command.c -cpp-extra-args-per-file=cpp-command.c:"-DPF=\\\"cp%02d_%.3f\\\"" -cpp-extra-args="-DPF2=\\\"cp%02d_%.3f\\\"" -print | python3 filter.py [kernel] Parsing cpp-command.c (with preprocessing) @@ -46,9 +46,10 @@ $ frama-c -check -no-autoload-plugins cpp-command.c -cpp-extra-args-per-file=cpp-command.c:"file_extra" -cpp-extra-args="global_extra" -cpp-command "echo 'extra_args: %args'" -print | python3 filter.py [kernel] Warning: your preprocessor is not known to handle option `-nostdinc'. If preprocessing fails because of it, please add -no-cpp-frama-c-compliant option to Frama-C's command-line. If you do not want to see this warning again, explicitly use option -cpp-frama-c-compliant. + [kernel] Warning: your preprocessor is not known to handle option `-undef'. If preprocessing fails because of it, please add -no-cpp-frama-c-compliant option to Frama-C's command-line. If you do not want to see this warning again, explicitly use option -cpp-frama-c-compliant. [kernel] Warning: your preprocessor is not known to handle option `-dD'. If preprocessing fails because of it, please add -no-cpp-frama-c-compliant option to Frama-C's command-line. If you do not want to see this warning again, explicitly use option -cpp-frama-c-compliant. [kernel] Parsing cpp-command.c (with preprocessing) - extra_args: -I<TMP_MACHDEP> -I$FRAMAC_SHARE/libc -D__FRAMAC__ -dD -nostdinc file_extra global_extra + extra_args: -I<TMP_MACHDEP> -I$FRAMAC_SHARE/libc -U__STDC_IEC_559_COMPLEX__ -U__STDC_IEC_60559_COMPLEX__ -U__STDC_ISO_10646__ -U__STDC_UTF16__ -U__STDC_UTF32__ -D__FRAMAC__ -dD -nostdinc -undef file_extra global_extra [kernel] Warning: trying to preprocess annotation with an unknown preprocessor. /* Generated by Frama-C */ diff --git a/tests/syntax/dune b/tests/syntax/dune index 48d4f37d21492a8d3de0f511f008571fb9b943b7..8e231d9e2555eb4f19d2f0bda8f502475ae9038e 100644 --- a/tests/syntax/dune +++ b/tests/syntax/dune @@ -1,4 +1,5 @@ (cram (applies_to cpp-command) (enabled_if %{read:../../python-3.7-available}) + (deps ../../src/init/boot/empty_file.exe) ) diff --git a/tests/syntax/oracle/censored_macros.res.oracle b/tests/syntax/oracle/censored_macros.res.oracle new file mode 100644 index 0000000000000000000000000000000000000000..09d5b3c972888a72bea6fe9ba91138f50b9b68e4 --- /dev/null +++ b/tests/syntax/oracle/censored_macros.res.oracle @@ -0,0 +1,10 @@ +[kernel] Parsing censored_macros.c (with preprocessing) +/* Generated by Frama-C */ +int main(void) +{ + int __retres; + __retres = 0; + return __retres; +} + +