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 /Makefile | |
| 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 'Makefile')
0 files changed, 0 insertions, 0 deletions