Merge branch 'fix/pp/really-censor-unsupported-macros' into 'master'

Undef unsupported macros

Closes #910

See merge request frama-c/frama-c!4891

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

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}).
 

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

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)

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"

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();

tests/spec/oracle/preprocess_string.res.oracle

 [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) ≡ '/'; */

tests/syntax/censored_macros.c

+#ifdef __SIZEOF_INT128__
+#error SHOULD BE BLACKLISTED
+#endif
+
+int main () { }

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 */
   

tests/syntax/dune

 (cram
   (applies_to cpp-command)
   (enabled_if %{read:../../python-3.7-available})
+  (deps ../../src/init/boot/empty_file.exe)
 )

tests/syntax/oracle/censored_macros.res.oracle

+[kernel] Parsing censored_macros.c (with preprocessing)
+/* Generated by Frama-C */
+int main(void)
+{
+  int __retres;
+  __retres = 0;
+  return __retres;
+}
+
+