diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-12-08 13:57:08 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-12-08 13:57:08 +0100 |
| commit | 05853d6e87d2f4da7132e6c354037effb8f7a7d3 (patch) | |
| tree | 91a2f75903f8cb3a40c00ce1530e5e0d58d0a016 /powerpc | |
| parent | 766968b709e5248a6aac6fdb92f6228be05fc70c (diff) | |
| parent | dc1e8157540655cd303df5c36e41c50a3dcc678e (diff) | |
| download | compcert-kvx-05853d6e87d2f4da7132e6c354037effb8f7a7d3.tar.gz compcert-kvx-05853d6e87d2f4da7132e6c354037effb8f7a7d3.zip | |
Merge remote-tracking branch 'origin/kvx-work' into kvx-better2-cse3
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 7ddbcc34..505b7545 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 |