diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-04-13 15:58:38 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-05-26 18:48:06 +0200 |
| commit | 58b59cce492f53ebd9aa960306f07f816c2e279d (patch) | |
| tree | 51e0430893119b307c21976c44ccffba0716d3cd /cfrontend/Cop.v | |
| parent | c36514ac4b05f78dd2e02fab3f8886cab8234925 (diff) | |
| download | compcert-58b59cce492f53ebd9aa960306f07f816c2e279d.tar.gz compcert-58b59cce492f53ebd9aa960306f07f816c2e279d.zip | |
Add a built-in function for "select" (strict conditional)
The built-in is called `EF_select` and has type `(int, T, T) -> T` for
a given Cminor type T.
During instruction selection, it is turned into an `Osel` operation if
available, otherwise into an if/then/else.
Diffstat (limited to 'cfrontend/Cop.v')
0 files changed, 0 insertions, 0 deletions