diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index a2670ae693..f44eb63812 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -421,6 +421,9 @@ let convertIkind k a : coq_type =
let convertFkind k a : coq_type =
match k with
+ | C.FFloat16 ->
+ unsupported "'_Float16' type";
+ Tfloat (F32, a)
| C.FFloat -> Tfloat (F32, a)
| C.FDouble -> Tfloat (F64, a)
| C.FLongDouble ->
@@ -695,6 +698,9 @@ let convertFloat f kind =
match mant with
| Z.Z0 ->
begin match kind with
+ | FFloat16 ->
+ unsupported "'_Float16' type";
+ Ctyping.econst_single (Float.to_single Float.zero)
| FFloat ->
Ctyping.econst_single (Float.to_single Float.zero)
| FDouble | FLongDouble ->
@@ -712,6 +718,9 @@ let convertFloat f kind =
let base = P.of_int (if f.C.hex then 2 else 10) in
begin match kind with
+ | FFloat16 ->
+ unsupported "'_Float16' type";
+ Ctyping.econst_single (Float.to_single Float.zero)
| FFloat ->
let f = Float32.from_parsed base mant exp in
checkFloatOverflow f "float";
diff --git a/cparser/C.mli b/cparser/C.mli
index 1388fab949..24f0e6f94a 100644
--- a/cparser/C.mli
+++ b/cparser/C.mli
@@ -46,11 +46,11 @@ type ikind =
(** Kinds of floating-point numbers*)
type fkind =
- FFloat (** [float] *)
+ | FFloat16 (** [_Float16] *)
+ | FFloat (** [float] *)
| FDouble (** [double] *)
| FLongDouble (** [long double] *)
-
(** Constants *)
type float_cst = {
diff --git a/cparser/Cabs.v b/cparser/Cabs.v
index 59cd30abbc..f27640114c 100644
--- a/cparser/Cabs.v
+++ b/cparser/Cabs.v
@@ -48,6 +48,7 @@ Inductive typeSpecifier := (* Merge all specifiers into one type *)
| Tint
| Tlong
| Tfloat
+ | Tfloat16
| Tdouble
| Tsigned
| Tunsigned
diff --git a/cparser/Cprint.ml b/cparser/Cprint.ml
index 054487841e..8155cf0943 100644
--- a/cparser/Cprint.ml
+++ b/cparser/Cprint.ml
@@ -56,6 +56,7 @@ let const pp = function
else
fprintf pp "%s.%sE%s" v.intPart v.fracPart v.exp;
begin match fk with
+ | FFloat16 -> () (* no syntax for FP16 literals; should not happen *)
| FFloat -> fprintf pp "F"
| FLongDouble -> fprintf pp "L"
| FDouble -> ()
@@ -123,6 +124,7 @@ let name_of_ikind = function
| IULongLong -> "unsigned long long"
let name_of_fkind = function
+ | FFloat16 -> "_Float16"
| FFloat -> "float"
| FDouble -> "double"
| FLongDouble -> "long double"
diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml
index 5b099d7fa6..0ef96ddd13 100644
--- a/cparser/Cutil.ml
+++ b/cparser/Cutil.ml
@@ -461,6 +461,7 @@ let alignof_ikind = function
| ILongLong | IULongLong -> !config.alignof_longlong
let alignof_fkind = function
+ | FFloat16 -> 2
| FFloat -> !config.alignof_float
| FDouble -> !config.alignof_double
| FLongDouble -> !config.alignof_longdouble
@@ -515,6 +516,7 @@ let sizeof_ikind = function
| ILongLong | IULongLong -> !config.sizeof_longlong
let sizeof_fkind = function
+ | FFloat16 -> 2
| FFloat -> !config.sizeof_float
| FDouble -> !config.sizeof_double
| FLongDouble -> !config.sizeof_longdouble
@@ -865,6 +867,7 @@ let integer_rank = function
(* Ranking of float kinds *)
let float_rank = function
+ | FFloat16 -> 0
| FFloat -> 1
| FDouble -> 2
| FLongDouble -> 3
@@ -922,7 +925,9 @@ let binary_conversion env t1 t2 =
| TFloat(FDouble, _), (TInt _ | TFloat _) -> t1
| (TInt _ | TFloat _), TFloat(FDouble, _) -> t2
| TFloat(FFloat, _), (TInt _ | TFloat _) -> t1
- | (TInt _), TFloat(FFloat, _) -> t2
+ | (TInt _ | TFloat _), TFloat(FFloat, _) -> t2
+ | TFloat(FFloat16, _), (TInt _ | TFloat _) -> t1
+ | (TInt _), TFloat(FFloat16, _) -> t2
| TInt(k1, _), TInt(k2, _) ->
if k1 = k2 then t1 else begin
match is_signed_ikind k1, is_signed_ikind k2 with
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index b4c0a20727..3060568b23 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -815,6 +815,7 @@ let rec elab_specifier ?(only = false) loc env specifier =
| [Cabs.Tunsigned; Cabs.Tlong; Cabs.Tlong; Cabs.Tint] -> simple (TInt(IULongLong, []))
| [Cabs.Tfloat] -> simple (TFloat(FFloat, []))
+ | [Cabs.Tfloat16] -> simple (TFloat(FFloat16, []))
| [Cabs.Tdouble] -> simple (TFloat(FDouble, []))
| [Cabs.Tlong; Cabs.Tdouble] -> simple (TFloat(FLongDouble, []))
diff --git a/cparser/Lexer.mll b/cparser/Lexer.mll
index 95374afe90..5d377053df 100644
--- a/cparser/Lexer.mll
+++ b/cparser/Lexer.mll
@@ -37,6 +37,7 @@ let () =
("_Bool", fun loc -> UNDERSCORE_BOOL loc);
("_Generic", fun loc -> GENERIC loc);
("_Complex", fun loc -> reserved_keyword loc "_Complex");
+ ("_Float16", fun loc -> FLOAT16 loc);
("_Imaginary", fun loc -> reserved_keyword loc "_Imaginary");
("_Static_assert", fun loc -> STATIC_ASSERT loc);
("__alignof", fun loc -> ALIGNOF loc);
@@ -638,6 +639,7 @@ and singleline_comment = parse
| Pre_parser.EQEQ loc -> loop (Parser.EQEQ loc)
| Pre_parser.EXTERN loc -> loop (Parser.EXTERN loc)
| Pre_parser.FLOAT loc -> loop (Parser.FLOAT loc)
+ | Pre_parser.FLOAT16 loc -> loop (Parser.FLOAT16 loc)
| Pre_parser.FOR loc -> loop (Parser.FOR loc)
| Pre_parser.GENERIC loc -> loop (Parser.GENERIC loc)
| Pre_parser.GEQ loc -> loop (Parser.GEQ loc)
diff --git a/cparser/Parser.vy b/cparser/Parser.vy
index cb1873b886..b69979675a 100644
--- a/cparser/Parser.vy
+++ b/cparser/Parser.vy
@@ -35,7 +35,8 @@ Require Cabs.
%token<Cabs.loc> LPAREN RPAREN LBRACK RBRACK LBRACE RBRACE DOT COMMA
SEMICOLON ELLIPSIS TYPEDEF EXTERN STATIC RESTRICT AUTO REGISTER INLINE
- NORETURN CHAR SHORT INT LONG SIGNED UNSIGNED FLOAT DOUBLE CONST VOLATILE VOID
+ NORETURN CHAR SHORT INT LONG SIGNED UNSIGNED FLOAT FLOAT16 DOUBLE
+ CONST VOLATILE VOID
STRUCT UNION ENUM UNDERSCORE_BOOL PACKED ALIGNAS ATTRIBUTE ASM
%token<Cabs.loc> CASE DEFAULT IF_ ELSE SWITCH WHILE DO FOR GOTO CONTINUE BREAK
@@ -441,6 +442,8 @@ type_specifier:
{ (Cabs.Tlong, loc) }
| loc = FLOAT
{ (Cabs.Tfloat, loc) }
+| loc = FLOAT16
+ { (Cabs.Tfloat16, loc) }
| loc = DOUBLE
{ (Cabs.Tdouble, loc) }
| loc = SIGNED
diff --git a/cparser/pre_parser.mly b/cparser/pre_parser.mly
index 00ca0ade7e..fd1559f74b 100644
--- a/cparser/pre_parser.mly
+++ b/cparser/pre_parser.mly
@@ -55,7 +55,8 @@
COLON AND MUL_ASSIGN DIV_ASSIGN MOD_ASSIGN ADD_ASSIGN SUB_ASSIGN LEFT_ASSIGN
RIGHT_ASSIGN AND_ASSIGN XOR_ASSIGN OR_ASSIGN LPAREN RPAREN LBRACK RBRACK
LBRACE RBRACE DOT COMMA SEMICOLON ELLIPSIS TYPEDEF EXTERN STATIC RESTRICT
- AUTO REGISTER INLINE NORETURN CHAR SHORT INT LONG SIGNED UNSIGNED FLOAT DOUBLE
+ AUTO REGISTER INLINE NORETURN CHAR SHORT INT LONG SIGNED UNSIGNED
+ FLOAT FLOAT16 DOUBLE
UNDERSCORE_BOOL CONST VOLATILE VOID STRUCT UNION ENUM CASE DEFAULT IF ELSE
SWITCH WHILE DO FOR GOTO CONTINUE BREAK RETURN BUILTIN_VA_ARG ALIGNOF
ATTRIBUTE ALIGNAS PACKED ASM BUILTIN_OFFSETOF STATIC_ASSERT GENERIC
@@ -510,6 +511,7 @@ type_specifier_no_typedef_name:
| INT
| LONG
| FLOAT
+| FLOAT16
| DOUBLE
| SIGNED
| UNSIGNED