diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-10-01 18:06:59 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-10-01 18:06:59 +0200 |
| commit | e1b3b2291debb78797c724a9469001bc8cc10a15 (patch) | |
| tree | cd2b8e2f07faf9d1af6b6b0d54b1e0339ec0e634 /mppa_k1c/SelectLong.vp | |
| parent | 028a9a1a4ee8e79585a7123c72ffcc2bb6d94570 (diff) | |
| download | compcert-kvx-e1b3b2291debb78797c724a9469001bc8cc10a15.tar.gz compcert-kvx-e1b3b2291debb78797c724a9469001bc8cc10a15.zip | |
SelectLong.vp fix
Diffstat (limited to 'mppa_k1c/SelectLong.vp')
| -rw-r--r-- | mppa_k1c/SelectLong.vp | 12 |
1 files changed, 4 insertions, 8 deletions
diff --git a/mppa_k1c/SelectLong.vp b/mppa_k1c/SelectLong.vp index b3e07bf5..26735c99 100644 --- a/mppa_k1c/SelectLong.vp +++ b/mppa_k1c/SelectLong.vp @@ -292,14 +292,10 @@ Definition notl (e: expr) := (** ** Integer division and modulus *) -Definition divlu_base (e1: expr) (e2: expr) := - if Archi.splitlong then SplitLong.divlu_base e1 e2 else Eop Odivlu (e1:::e2:::Enil). -Definition modlu_base (e1: expr) (e2: expr) := - if Archi.splitlong then SplitLong.modlu_base e1 e2 else Eop Omodlu (e1:::e2:::Enil). -Definition divls_base (e1: expr) (e2: expr) := - if Archi.splitlong then SplitLong.divls_base e1 e2 else Eop Odivl (e1:::e2:::Enil). -Definition modls_base (e1: expr) (e2: expr) := - if Archi.splitlong then SplitLong.modls_base e1 e2 else Eop Omodl (e1:::e2:::Enil). +Definition divlu_base (e1: expr) (e2: expr) := SplitLong.divlu_base e1 e2. +Definition modlu_base (e1: expr) (e2: expr) := SplitLong.modlu_base e1 e2. +Definition divls_base (e1: expr) (e2: expr) := SplitLong.divls_base e1 e2. +Definition modls_base (e1: expr) (e2: expr) := SplitLong.modls_base e1 e2. Definition shrxlimm (e: expr) (n: int) := if Archi.splitlong then SplitLong.shrxlimm e n else |