diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-12-08 11:03:48 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-12-08 11:03:48 +0100 |
| commit | 8350d5ab1823db94d04dd4e1aaa4b4b64c27371d (patch) | |
| tree | 2437d342ac2ab83b16fbd4aed579305518015574 /powerpc | |
| parent | cb93a301fd2ddae3071ae0838290b201496d90ef (diff) | |
| download | compcert-kvx-8350d5ab1823db94d04dd4e1aaa4b4b64c27371d.tar.gz compcert-kvx-8350d5ab1823db94d04dd4e1aaa4b4b64c27371d.zip | |
rm instructions now unused
Diffstat (limited to 'powerpc')
| -rw-r--r-- | powerpc/Op.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/powerpc/Op.v b/powerpc/Op.v index 3d84d95c..684b90bf 100644 --- a/powerpc/Op.v +++ b/powerpc/Op.v @@ -573,8 +573,7 @@ Definition is_trapping_op (op : operation) := match op with | Odiv | Odivl | Odivu | Odivlu | Oshrximm _ | Oshrxlimm _ - | Ointoffloat | Ointuoffloat - | Ofloatofint | Ofloatofintu + | Ointoffloat | Olongoffloat | Ofloatoflong => true | _ => false |