diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-06-04 13:03:38 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-06-04 13:03:38 +0200 |
| commit | 7c054b47cad2f75efa661b298484dfbfdd976701 (patch) | |
| tree | daa0b1f8b8d023c648ed3b8dbd4c17162a6439fc /mppa_k1c/SelectOp.vp | |
| parent | 3f441224f1c33942cbfe0c41334ff66fcb8b4a72 (diff) | |
| download | compcert-kvx-7c054b47cad2f75efa661b298484dfbfdd976701.tar.gz compcert-kvx-7c054b47cad2f75efa661b298484dfbfdd976701.zip | |
little restructuring
Diffstat (limited to 'mppa_k1c/SelectOp.vp')
| -rw-r--r-- | mppa_k1c/SelectOp.vp | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/mppa_k1c/SelectOp.vp b/mppa_k1c/SelectOp.vp index ee614253..8101a9b0 100644 --- a/mppa_k1c/SelectOp.vp +++ b/mppa_k1c/SelectOp.vp @@ -66,10 +66,11 @@ Section SELECT. Context {hf: helper_functions}. (** Ternary operator *) -(** TODO *) +Definition select0 (ty : typ) (cond0 : condition0) (e1 e2 eC: expr) := + (Eop (Osel cond0 ty) (e1 ::: e2 ::: eC ::: Enil)). + Definition select (ty : typ) (cond : condition) (args : exprlist) (e1 e2: expr) : option expr := - Some (Eop (Osel (Ccomp0 Cne) ty) (e1 ::: e2 ::: - (Eop (Ocmp cond) args) ::: Enil)). + Some (select0 ty (Ccomp0 Cne) e1 e2 (Eop (Ocmp cond) args)). (** ** Constants **) |