diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-08 10:44:34 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-09-08 10:44:34 +0200 |
| commit | 2246044e99569fcf1c2172f0e710134123be8b49 (patch) | |
| tree | df56ebe23cb71259f346ee1f73fafe3f9a96e476 /powerpc/CBuiltins.ml | |
| parent | 73e20bd6e0586e38fbc7d87d8c306fad7b578418 (diff) | |
| download | compcert-kvx-2246044e99569fcf1c2172f0e710134123be8b49.tar.gz compcert-kvx-2246044e99569fcf1c2172f0e710134123be8b49.zip | |
Added builtin for isel.
The builtin_isel function takes a _Bool as first argument and returns
either the second or the third depending on the value of the _Bool.
Diffstat (limited to 'powerpc/CBuiltins.ml')
| -rw-r--r-- | powerpc/CBuiltins.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml index 6d7b2aff..e219a175 100644 --- a/powerpc/CBuiltins.ml +++ b/powerpc/CBuiltins.ml @@ -115,7 +115,10 @@ let builtins = { "__builtin_call_frame", (TPtr (TVoid [],[]),[],false); "__builtin_return_address", - (TPtr (TVoid [],[]),[],false) + (TPtr (TVoid [],[]),[],false); + (* isel *) + "__builtin_isel", + (TInt (IInt, []),[TInt(IInt, []);TInt(IInt, []);TInt(IInt, [])],false) ] } |