diff options
author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-04-13 19:19:22 +0200 |
---|---|---|
committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2019-05-26 18:48:06 +0200 |
commit | bc67de2b1275ba5e6f9e2259f559808533a8649f (patch) | |
tree | efc1e867889dea064ce08ddd10d2411ebc7799fe /driver/Compopts.v | |
parent | 58b59cce492f53ebd9aa960306f07f816c2e279d (diff) | |
download | compcert-bc67de2b1275ba5e6f9e2259f559808533a8649f.tar.gz compcert-bc67de2b1275ba5e6f9e2259f559808533a8649f.zip |
Add selection to CompCert C as a derived form
`Eselection r1 r2 r3 ty` is like `Econdition r1 r2 r3 ty`, except
that both `r2` and `r3` are always evaluated, thus the expression
can be compiled down to a conditional move.
Internally, `Eselection` is expressed as a call to the built-in
`EF_select`. We prove admissible evaluation rules, showing that
the encoding gives the expected semantics.
Diffstat (limited to 'driver/Compopts.v')
0 files changed, 0 insertions, 0 deletions