diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-19 22:13:53 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-03-19 22:13:53 +0100 |
| commit | 4cc5324db73dd014bcd2c118f5769f88e52f8643 (patch) | |
| tree | 6f3df7b011f34f2cdaa8381342756708f7b02e49 /mppa_k1c/Machregs.v | |
| parent | f321f75979d18ab99f226b2c5d6bbb59bffb5cac (diff) | |
| parent | 2af07d6a328f73a32bc2c768e3108dd3db393ed1 (diff) | |
| download | compcert-kvx-4cc5324db73dd014bcd2c118f5769f88e52f8643.tar.gz compcert-kvx-4cc5324db73dd014bcd2c118f5769f88e52f8643.zip | |
Merge branch 'mppa-madd' into mppa_postpass
Diffstat (limited to 'mppa_k1c/Machregs.v')
| -rw-r--r-- | mppa_k1c/Machregs.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mppa_k1c/Machregs.v b/mppa_k1c/Machregs.v index 28154c7f..ef0f97a9 100644 --- a/mppa_k1c/Machregs.v +++ b/mppa_k1c/Machregs.v @@ -210,7 +210,7 @@ Global Opaque Definition two_address_op (op: operation) : bool := match op with - | Ocast32unsigned => true + | Ocast32unsigned | Omadd | Omaddimm _ => true | _ => false end. |