* <http://www.gnu.org/licenses/>.
  */
 
+#ifndef _CPUID_H_INCLUDED
+#define _CPUID_H_INCLUDED
+
 /* %eax */
 #define bit_AVX512BF16 (1 << 5)
 
   __cpuid_count (__leaf, __subleaf, *__eax, *__ebx, *__ecx, *__edx);
   return 1;
 }
+
+static __inline void
+__cpuidex (int __cpuid_info[4], int __leaf, int __subleaf)
+{
+  __cpuid_count (__leaf, __subleaf, __cpuid_info[0], __cpuid_info[1],
+                __cpuid_info[2], __cpuid_info[3]);
+}
+
+#endif /* _CPUID_H_INCLUDED */
 
--- /dev/null
+/* { dg-do run } */
+/* { dg-options "-O2 -Wall" } */
+
+#include <cpuid.h>
+#include <cpuid.h>
+
+int
+main ()
+{
+  unsigned int eax, ebx, ecx, edx;
+  int cpuid_info[4];
+
+  if (!__get_cpuid_count (7, 0, &eax, &ebx, &ecx, &edx))
+    return 0;
+
+  __cpuidex (cpuid_info, 7, 0);
+
+  if (cpuid_info[0] != eax
+      || cpuid_info[1] != ebx
+      || cpuid_info[2] != ecx
+      || cpuid_info[3] != edx)
+    __builtin_abort ();
+
+  return 0;
+}