diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-03 22:36:22 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-03 22:36:22 +0200 |
commit | ca34ea47f863c074a9d0ca890097786c5829267c (patch) | |
tree | 52177af944305d25bcfea601f9abc57b1eef525a /cfrontend | |
parent | 524678ff9a521433ff0b5af2a3986c1e385e699e (diff) | |
download | compcert-kvx-ca34ea47f863c074a9d0ca890097786c5829267c.tar.gz compcert-kvx-ca34ea47f863c074a9d0ca890097786c5829267c.zip |
ternary ops for float/double
Diffstat (limited to 'cfrontend')
-rw-r--r-- | cfrontend/C2C.ml | 4 |
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", |