diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-03-01 17:25:48 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-03-01 17:25:48 +0100 |
| commit | 5f7252105c9c639078ca3cc313502c647779d2f8 (patch) | |
| tree | 502cbaf2c695bd7edeee512f6bc9ce8a46b34730 /mppa_k1c/Asmblockgen.v | |
| parent | d8fafb0add258e47287a2d57454194db8f1dd635 (diff) | |
| download | compcert-kvx-5f7252105c9c639078ca3cc313502c647779d2f8.tar.gz compcert-kvx-5f7252105c9c639078ca3cc313502c647779d2f8.zip | |
Ajouté la négation des comparateurs single
Diffstat (limited to 'mppa_k1c/Asmblockgen.v')
| -rw-r--r-- | mppa_k1c/Asmblockgen.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index fb6ba16e..73ecd67f 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -324,9 +324,9 @@ Definition transl_cond_op | Ccompfs c, a1 :: a2 :: nil => do r1 <- ireg_of a1; do r2 <- ireg_of a2; OK (transl_cond_float32 c rd r1 r2 k) -(* | Cnotcompfs c, a1 :: a2 :: nil => + | Cnotcompfs c, a1 :: a2 :: nil => do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (transl_cond_notfloat32 c rd r1 r2 k) *) (* FIXME - because of proofs, might have to use a xor instead *) + OK (transl_cond_notfloat32 c rd r1 r2 k) (* FIXME - because of proofs, might have to use a xor instead *) | Ccompf _, _ => Error(msg "Asmblockgen.transl_cond_op: Ccompf") | Cnotcompf _, _ => Error(msg "Asmblockgen.transl_cond_op: Cnotcompf") (*| Ccompf c, f1 :: f2 :: nil => |