Add further GCC/Clang vector types

These are used in GCC/Clang built-ins.

Author: tautschnig

src/ansi-c/compiler_headers/gcc_builtin_headers_types.h

@@ -17,6 +17,9 @@ typedef short  __gcc_v4hi  __attribute__ ((__vector_size__ (8)));
 typedef short  __gcc_v8hi  __attribute__ ((__vector_size__ (16)));
 typedef short  __gcc_v16hi __attribute__ ((__vector_size__ (32)));
 typedef short  __gcc_v32hi __attribute__ ((__vector_size__ (64)));
+typedef __CPROVER_Float16  __gcc_v8hf  __attribute__ ((__vector_size__ (16)));
+typedef __CPROVER_Float16  __gcc_v16hf  __attribute__ ((__vector_size__ (32)));
+typedef __CPROVER_Float16  __gcc_v32hf  __attribute__ ((__vector_size__ (64)));
 typedef float  __gcc_v2sf  __attribute__ ((__vector_size__ (8)));
 typedef float  __gcc_v4sf  __attribute__ ((__vector_size__ (16)));
 typedef float  __gcc_v8sf  __attribute__ ((__vector_size__ (32)));
@@ -28,7 +31,10 @@ typedef long long __gcc_v1di __attribute__ ((__vector_size__ (8)));
 typedef long long __gcc_v2di __attribute__ ((__vector_size__ (16)));
 typedef long long __gcc_v4di __attribute__ ((__vector_size__ (32)));
 typedef long long __gcc_v8di __attribute__ ((__vector_size__ (64)));
+typedef unsigned short __gcc_v32uhi __attribute__ ((__vector_size__ (64)));
+typedef unsigned int __gcc_v16usi  __attribute__ ((__vector_size__ (64)));
 typedef unsigned long long __gcc_di;
+typedef unsigned long long __gcc_v8udi __attribute__ ((__vector_size__ (64)));
 
 enum __gcc_atomic_memmodels {
   __ATOMIC_RELAXED, __ATOMIC_CONSUME, __ATOMIC_ACQUIRE, __ATOMIC_RELEASE, __ATOMIC_ACQ_REL, __ATOMIC_SEQ_CST

src/ansi-c/scanner.l

@@ -540,6 +540,10 @@ enable_or_disable ("enable"|"disable")
                     return make_identifier();
                 }
 
+{CPROVER_PREFIX}"Float16" {
+                  loc(); return TOK_GCC_FLOAT16;
+                }
+
 "__bf16"        { if(PARSER.bf16_type)
                   { loc(); return TOK_GCC_FLOAT16; }
                   else

src/cpp/parse.cpp

@@ -772,11 +772,12 @@ bool Parser::isTypeSpecifier()
          || t == TOK_SIGNED || t == TOK_UNSIGNED || t == TOK_FLOAT ||
          t == TOK_DOUBLE || t == TOK_INT8 || t == TOK_INT16 || t == TOK_INT32 ||
          t == TOK_INT64 || t == TOK_GCC_INT128 || t == TOK_PTR32 ||
-         t == TOK_PTR64 || t == TOK_GCC_FLOAT80 || t == TOK_GCC_FLOAT128 ||
-         t == TOK_VOID || t == TOK_BOOL || t == TOK_CPROVER_BOOL ||
-         t == TOK_CLASS || t == TOK_STRUCT || t == TOK_UNION || t == TOK_ENUM ||
-         t == TOK_INTERFACE || t == TOK_TYPENAME || t == TOK_TYPEOF ||
-         t == TOK_DECLTYPE || t == TOK_UNDERLYING_TYPE;
+         t == TOK_PTR64 || t == TOK_GCC_FLOAT16 || t == TOK_GCC_FLOAT80 ||
+         t == TOK_GCC_FLOAT128 || t == TOK_VOID || t == TOK_BOOL ||
+         t == TOK_CPROVER_BOOL || t == TOK_CLASS || t == TOK_STRUCT ||
+         t == TOK_UNION || t == TOK_ENUM || t == TOK_INTERFACE ||
+         t == TOK_TYPENAME || t == TOK_TYPEOF || t == TOK_DECLTYPE ||
+         t == TOK_UNDERLYING_TYPE;
 }
 
 /*
@@ -2510,6 +2511,9 @@ bool Parser::optIntegralTypeOrClassSpec(typet &p)
     case TOK_INT32: type_id=ID_int32; break;
     case TOK_INT64: type_id=ID_int64; break;
     case TOK_GCC_INT128: type_id=ID_gcc_int128; break;
+    case TOK_GCC_FLOAT16:
+      type_id = ID_gcc_float16;
+      break;
     case TOK_GCC_FLOAT80: type_id=ID_gcc_float80; break;
     case TOK_GCC_FLOAT128: type_id=ID_gcc_float128; break;
     case TOK_BOOL: