diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-04 12:34:11 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-04 12:34:11 +0200 |
| commit | b7ded97f34c5f0c670f43f2b15e77eb8874a764e (patch) | |
| tree | df8cda7c77a4ee98ba9178be184a9e82ca5bbe84 /mppa_k1c/Machregs.v | |
| parent | 3b70f4b0eb0d8efde0946ed883072e0f94d5766d (diff) | |
| download | compcert-kvx-b7ded97f34c5f0c670f43f2b15e77eb8874a764e.tar.gz compcert-kvx-b7ded97f34c5f0c670f43f2b15e77eb8874a764e.zip | |
progressing on select
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 f89f952f..daf724ea 100644 --- a/mppa_k1c/Machregs.v +++ b/mppa_k1c/Machregs.v @@ -209,7 +209,7 @@ Global Opaque Definition two_address_op (op: operation) : bool := match op with - | Ocast32unsigned | Omadd | Omaddimm _ | Omaddl | Omaddlimm _ | Oselect | Oselectl | Oselectf | Oselectfs => true + | Ocast32unsigned | Omadd | Omaddimm _ | Omaddl | Omaddlimm _ | Oselect _ | Oselectl | Oselectf | Oselectfs => true | _ => false end. |