Skip to content

Commit

Permalink
Add support for Arm-specific vector types
Browse files Browse the repository at this point in the history
GCC on Arm-only supports additional vector types that compile to
hardware-supported types.
  • Loading branch information
tautschnig committed Jan 20, 2025
1 parent e50c2d0 commit da974c7
Showing 1 changed file with 9 additions and 0 deletions.
9 changes: 9 additions & 0 deletions src/ansi-c/compiler_headers/gcc_builtin_headers_types.h
Original file line number Diff line number Diff line change
Expand Up @@ -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

0 comments on commit da974c7

Please sign in to comment.