diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-10 23:37:07 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-10 23:37:07 +0200 |
| commit | e2ea45f5ba656254fa11bf3f355da67292c11f06 (patch) | |
| tree | dc9bdd29f0e2dc34bfcd4fb984811a8afb86892d /mppa_k1c/Machregs.v | |
| parent | 95b43cbcc4390d9058034b769ffa757c42d2a74f (diff) | |
| download | compcert-kvx-e2ea45f5ba656254fa11bf3f355da67292c11f06.tar.gz compcert-kvx-e2ea45f5ba656254fa11bf3f355da67292c11f06.zip | |
more integer Op
Diffstat (limited to 'mppa_k1c/Machregs.v')
| -rw-r--r-- | mppa_k1c/Machregs.v | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/mppa_k1c/Machregs.v b/mppa_k1c/Machregs.v index cd8c6606..6e0efe28 100644 --- a/mppa_k1c/Machregs.v +++ b/mppa_k1c/Machregs.v @@ -213,7 +213,10 @@ Global Opaque Definition two_address_op (op: operation) : bool := match op with - | Omadd | Omaddimm _ | Omaddl | Omaddlimm _ + | Omadd | Omaddimm _ + | Omaddl | Omaddlimm _ + | Omsub | Omsubimm _ + | Omsubl | Omsublimm _ | Oselect _ | Oselectl _ | Oselectf _ | Oselectfs _ | Oinsf _ _ | Oinsfl _ _ => true | _ => false |