diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-05-21 16:34:36 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-05-21 16:39:48 +0200 |
| commit | 479aacd0254605942a3f48c3b8053af4d07f0f6c (patch) | |
| tree | 7ddbddf078b86a30e693ae35721e08f54a0af11e /mppa_k1c/Machregs.v | |
| parent | b81dbb863781a5f450cad0b01f90f729fb1a2244 (diff) | |
| download | compcert-kvx-479aacd0254605942a3f48c3b8053af4d07f0f6c.tar.gz compcert-kvx-479aacd0254605942a3f48c3b8053af4d07f0f6c.zip | |
MPPA - Added modulo and division 64 bits. Non certified
32 bits version are not yet there.
Right now the code is directly from libgcc, compiled with k1-gcc because
of builtins.
Diffstat (limited to 'mppa_k1c/Machregs.v')
| -rw-r--r-- | mppa_k1c/Machregs.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/mppa_k1c/Machregs.v b/mppa_k1c/Machregs.v index ed582c98..bed3c040 100644 --- a/mppa_k1c/Machregs.v +++ b/mppa_k1c/Machregs.v @@ -208,11 +208,11 @@ Global Opaque integers as their 64-bit sign extension; and [Ocast32unsigned], because it builds on the same magic no-op. *) -Definition two_address_op (op: operation) : bool := false. - (* match op with - | Ocast32signed | Ocast32unsigned => true +Definition two_address_op (op: operation) : bool := + match op with + | Ocast32unsigned => true | _ => false - end. *) + end. (** Constraints on constant propagation for builtins *) |