diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2019-04-12 17:35:18 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2019-05-20 18:00:46 +0200 |
| commit | 3830a91a4711c4570394e02e93e4e08db88eac6f (patch) | |
| tree | 4008888998c3c61a8a18adc4ca37e3b8e2e34000 /powerpc/Asm.v | |
| parent | e9cca9c8166fadb16c64df0fbb0b9ca640c0f594 (diff) | |
| download | compcert-kvx-3830a91a4711c4570394e02e93e4e08db88eac6f.tar.gz compcert-kvx-3830a91a4711c4570394e02e93e4e08db88eac6f.zip | |
Support a "select" operation between two values
`Val.select ob v1 v2 ty` is a conditional operation that chooses between
the values `v1` and `v2` depending on the comparison `ob : option bool`.
If `ob` is `None`, `Vundef` is returned.
If the selected value does not match type `ty`, `Vundef` is returned.
This operation will be used to model a "select" (or "conditional move")
operation at the CminorSel/RTL/LTL/Mach level.
Diffstat (limited to 'powerpc/Asm.v')
0 files changed, 0 insertions, 0 deletions