Add gcc to the NIX shell on macOS to support CBMC.

Leaves CC set as "clang" for compilation and testing
on macOS.

Always use gcc for pre-processing with goto-cc to get
consistent C header files on all platforms, including
macOS/Darwin.

Ported from mlkem-native (pq-code-package/mlkem-native#1780,
commit b828ccdb28db111695837efdbb3a85338b5ef112).

Signed-off-by: Rod Chapman <rodchap@amazon.com>
Signed-off-by: Hanno Becker <beckphan@amazon.co.uk>

Author: rod-chapman

nix/util.nix

@@ -49,6 +49,15 @@ rec {
       # - On some machines, `native-gcc` needed to be evaluated lastly (placed as the last element of the toolchain list), or else would result in environment variables (CC, AR, ...) overriding issue.
     pkgs.lib.optionals cross [ pkgs.qemu pkgs.gcc-arm-embedded x86_64-gcc aarch64-gcc riscv64-gcc riscv32-gcc ppc64le-gcc ]
     ++ pkgs.lib.optionals (cross && pkgs.stdenv.isLinux && pkgs.stdenv.isx86_64) [ aarch64_be-gcc ]
+    # On Darwin, install GCC in addition to Clang. We reuse the exact same
+    # `pkgs.gcc` attribute that the Linux native toolchain wraps (`native-gcc`
+    # = `wrap-gcc pkgs`, whose compiler is `pkgs.gcc.cc`). Because both sides
+    # reference the same package from the flake-locked nixpkgs, the Darwin GCC
+    # version is always identical to the Linux one (do NOT pin a hardcoded
+    # `gccNN` here, or the two platforms could drift apart on a nixpkgs bump).
+    # Note that on Darwin, $CC remains set to "clang" for compilation and testing purposes,
+    # while gcc is used for pre-processing sources for CBMC only.
+    ++ pkgs.lib.optionals pkgs.stdenv.isDarwin [ pkgs.gcc ]
     ++ pkgs.lib.optionals cross [ native-gcc ]
     # git is not available in the nix shell on Darwin. As a workaround we add git as a dependency here.
     # Initially, we expected this to be fixed by https://github.com/NixOS/nixpkgs/pull/353893, but that does not seem to be the case.

proofs/cbmc/Makefile.common

@@ -330,7 +330,12 @@ CHECKFLAGS += $(CBMC_FLAG_UNSIGNED_OVERFLOW_CHECK)
 NONDET_STATIC ?=
 
 # Flags to pass to goto-cc for compilation and linking
-COMPILE_FLAGS ?= -Wall -Werror --native-compiler $(CC)
+#
+# Note that we always use gcc for pre-processing with goto-cc
+# in order to get consistent header files on all platforms,
+# rather than using $(CC) (which might be preferred for compilation
+# on some platforms such as macOS/Darwin)
+COMPILE_FLAGS ?= -Wall -Werror --native-compiler gcc
 LINK_FLAGS ?= -Wall -Werror
 EXPORT_FILE_LOCAL_SYMBOLS ?= --export-file-local-symbols