diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-06-04 07:26:55 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-06-04 07:26:55 +0200 |
| commit | 30f549e4e04567e35fb6a4eda269132f6cd22dd1 (patch) | |
| tree | bc89e3c3871c422460d5912dd58e2041a89f34d7 | |
| parent | 0daaa4c00119fe19872bab38aacf01c34d465c5f (diff) | |
| download | compcert-kvx-30f549e4e04567e35fb6a4eda269132f6cd22dd1.tar.gz compcert-kvx-30f549e4e04567e35fb6a4eda269132f6cd22dd1.zip | |
Osel is output = 1st input
| -rw-r--r-- | mppa_k1c/Machregs.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/mppa_k1c/Machregs.v b/mppa_k1c/Machregs.v index 4e8eedda..ee3a63c7 100644 --- a/mppa_k1c/Machregs.v +++ b/mppa_k1c/Machregs.v @@ -216,6 +216,7 @@ Definition two_address_op (op: operation) : bool := | Omadd | Omaddimm _ | Omaddl | Omaddlimm _ | Omsub | Omsubl + | Osel _ _ | Oinsf _ _ | Oinsfl _ _ => true | _ => false end. |