From da974c7656955ff34ecbdcc37e1f9aca28fcb77f Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Mon, 20 Jan 2025 12:30:59 +0000 Subject: [PATCH] Add support for Arm-specific vector types GCC on Arm-only supports additional vector types that compile to hardware-supported types. --- src/ansi-c/compiler_headers/gcc_builtin_headers_types.h | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/ansi-c/compiler_headers/gcc_builtin_headers_types.h b/src/ansi-c/compiler_headers/gcc_builtin_headers_types.h index 8920a952f1d..348c245891c 100644 --- a/src/ansi-c/compiler_headers/gcc_builtin_headers_types.h +++ b/src/ansi-c/compiler_headers/gcc_builtin_headers_types.h @@ -45,4 +45,13 @@ enum __gcc_atomic_memmodels { }; typedef unsigned char __tile __attribute__ ((__vector_size__ (1024))); + +// GCC and Clang use the following on ARM: +typedef float __Float32x4_t __attribute__ ((__vector_size__ (16))); +typedef double __Float64x2_t __attribute__ ((__vector_size__ (16))); +// The following ARM (scalable vector) extensions define vectors the size of +// which is not known at compile time. +typedef float *__SVFloat32_t; +typedef double *__SVFloat64_t; +typedef __CPROVER_bool *__SVBool_t; // clang-format on