aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/C2C.ml
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2019-04-03 22:36:22 +0200
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2019-04-03 22:36:22 +0200
commitca34ea47f863c074a9d0ca890097786c5829267c (patch)
tree52177af944305d25bcfea601f9abc57b1eef525a /cfrontend/C2C.ml
parent524678ff9a521433ff0b5af2a3986c1e385e699e (diff)
downloadcompcert-kvx-ca34ea47f863c074a9d0ca890097786c5829267c.tar.gz
compcert-kvx-ca34ea47f863c074a9d0ca890097786c5829267c.zip
ternary ops for float/double
Diffstat (limited to 'cfrontend/C2C.ml')
-rw-r--r--cfrontend/C2C.ml4
1 files changed, 4 insertions, 0 deletions
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index c17ce75a..0f2e3674 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -188,6 +188,10 @@ let builtins_generic = {
(* Ternary operator *)
builtin_ternary "uint" (TInt(IUInt, []));
builtin_ternary "ulong" (TInt(IULong, []));
+ builtin_ternary "int" (TInt(IInt, []));
+ builtin_ternary "long" (TInt(ILong, []));
+ builtin_ternary "double" (TFloat(FDouble, []));
+ builtin_ternary "float" (TFloat(FFloat, []));
(* Annotations *)
"__builtin_annot",