diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-04 21:40:04 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-04 21:40:04 +0200 |
| commit | e08d244a18870131820814880685504f0ea467e6 (patch) | |
| tree | 58f95c1b0872bb7c6bc74a43b349f97171a37c51 /mppa_k1c/SelectOp.vp | |
| parent | 71c38724bee43fe1a2ce67ee51f09478cd167929 (diff) | |
| download | compcert-kvx-e08d244a18870131820814880685504f0ea467e6.tar.gz compcert-kvx-e08d244a18870131820814880685504f0ea467e6.zip | |
more on select
Diffstat (limited to 'mppa_k1c/SelectOp.vp')
| -rw-r--r-- | mppa_k1c/SelectOp.vp | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp index 31e81093..10c91bba 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -61,6 +61,11 @@ Section SELECT. Context {hf: helper_functions}. +(** Ternary operator *) +Definition select o0 o1 oselect := + Eop (Oselect (Ccomp0 Ceq)) + (o0:::o1:::oselect:::Enil). + (** ** Constants **) Definition addrsymbol (id: ident) (ofs: ptrofs) := |