Skip to content

Commit 84a343e

Browse files
committed
Add support for Arm-specific vector types
GCC on Arm-only supports additional vector types that compile to hardware-supported types.
1 parent 97c8624 commit 84a343e

File tree

1 file changed

+9
-0
lines changed

1 file changed

+9
-0
lines changed

src/ansi-c/compiler_headers/gcc_builtin_headers_types.h

+9
Original file line numberDiff line numberDiff line change
@@ -45,4 +45,13 @@ enum __gcc_atomic_memmodels {
4545
};
4646

4747
typedef unsigned char __tile __attribute__ ((__vector_size__ (1024)));
48+
49+
// GCC and Clang use the following on ARM:
50+
typedef float __Float32x4_t __attribute__ ((__vector_size__ (16)));
51+
typedef double __Float64x2_t __attribute__ ((__vector_size__ (16)));
52+
// The following ARM (scalable vector) extensions define vectors the size of
53+
// which is not known at compile time.
54+
typedef float *__SVFloat32_t;
55+
typedef double *__SVFloat64_t;
56+
typedef __CPROVER_bool *__SVBool_t;
4857
// clang-format on

0 commit comments

Comments
 (0)