From 3a0cc1a2fad8010a85239b029077750f6186dabb Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Thu, 25 Jan 2024 11:30:09 +0000
Subject: [PATCH] C front-end: GCC >= 12 support __builtin_shufflevector

This used to be Clang-only, but is now also supported by GCC.
---
 regression/cbmc/gcc_vector3/main.c | 15 +++++++++++++--
 src/ansi-c/c_typecheck_expr.cpp    |  4 +---
 2 files changed, 14 insertions(+), 5 deletions(-)

diff --git a/regression/cbmc/gcc_vector3/main.c b/regression/cbmc/gcc_vector3/main.c
index 85d45b3f724..b0469ad14a3 100644
--- a/regression/cbmc/gcc_vector3/main.c
+++ b/regression/cbmc/gcc_vector3/main.c
@@ -9,7 +9,7 @@ typedef union {
 } vector_u;
 #endif
 
-int main()
+void test_shuffle()
 {
 #if defined(__GNUC__) && !defined(__clang__)
   // https://gcc.gnu.org/onlinedocs/gcc/Vector-Extensions.html
@@ -31,7 +31,12 @@ int main()
   assert(res.members[1] == 5);
   assert(res.members[2] == 3);
   assert(res.members[3] == 6);
-#elif defined(__clang__)
+#endif
+}
+
+void test_shufflevector(void)
+{
+#if defined(__clang__) || (defined(__GNUC__) && __GNUC__ >= 12)
   v4si a = {1, 2, 3, 4};
   v4si b = {5, 6, 7, 8};
 
@@ -50,3 +55,9 @@ int main()
   assert(res.members[3] == 6);
 #endif
 }
+
+int main()
+{
+  test_shuffle();
+  test_shufflevector();
+}
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index df210afc6cf..5b95531fe1a 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -2133,9 +2133,7 @@ void c_typecheck_baset::typecheck_side_effect_function_call(
 
         return;
       }
-      else if(
-        identifier == "__builtin_shufflevector" &&
-        config.ansi_c.mode == configt::ansi_ct::flavourt::CLANG)
+      else if(identifier == "__builtin_shufflevector")
       {
         exprt result = typecheck_shuffle_vector(expr);
         expr.swap(result);