From 0a89ade1e185b1f7eece609f1ee89e945ce7fc5d Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Fri, 21 Jan 2022 15:47:16 +0000
Subject: [PATCH] Enable rotate left/right tests on all platforms

We just need to provide the declarations on non-Clang builds. This is to
ensure test coverage irrespective of whether a test is run using Clang
or not.
---
 regression/cbmc/clang_builtins/rotate.c    | 18 ++++++++++++++----
 regression/cbmc/clang_builtins/rotate.desc |  4 +++-
 2 files changed, 17 insertions(+), 5 deletions(-)

diff --git a/regression/cbmc/clang_builtins/rotate.c b/regression/cbmc/clang_builtins/rotate.c
index 79bc30ac187..0f4df6cb213 100644
--- a/regression/cbmc/clang_builtins/rotate.c
+++ b/regression/cbmc/clang_builtins/rotate.c
@@ -8,7 +8,20 @@
 #define ror(type, x, d)                                                        \
   ((type)(((x) >> (d)) | ((x) << ((8 * sizeof(type)) - (d)))))
 
-#ifdef __clang__
+#ifndef __clang__
+unsigned char __builtin_rotateleft8(unsigned char, unsigned char);
+unsigned short __builtin_rotateleft16(unsigned short, unsigned short);
+unsigned int __builtin_rotateleft32(unsigned int, unsigned int);
+unsigned long long
+__builtin_rotateleft64(unsigned long long, unsigned long long);
+
+unsigned char __builtin_rotateright8(unsigned char, unsigned char);
+unsigned short __builtin_rotateright16(unsigned short, unsigned short);
+unsigned int __builtin_rotateright32(unsigned int, unsigned int);
+unsigned long long
+__builtin_rotateright64(unsigned long long, unsigned long long);
+#endif
+
 void check_left8(void)
 {
   uint8_t op;
@@ -80,11 +93,9 @@ void check_right64(void)
   assert(__builtin_rotateright64(op, 3) == ror(uint64_t, op, 3));
   assert(__builtin_rotateright64(op, 4) == ror(uint64_t, op, 4));
 }
-#endif
 
 int main(void)
 {
-#ifdef __clang__
   check_left8();
   check_left16();
   check_left32();
@@ -93,5 +104,4 @@ int main(void)
   check_right16();
   check_right32();
   check_right64();
-#endif
 }
diff --git a/regression/cbmc/clang_builtins/rotate.desc b/regression/cbmc/clang_builtins/rotate.desc
index 322d5232a1f..25a4d0c702a 100644
--- a/regression/cbmc/clang_builtins/rotate.desc
+++ b/regression/cbmc/clang_builtins/rotate.desc
@@ -1,6 +1,8 @@
-CORE gcc-only
+CORE
 rotate.c
 
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
+--
+^warning: ignoring