diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-03-15 11:05:33 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-03-15 11:05:33 +0100 |
| commit | fbe5ac2c9619441ad84dedf3c0cdabb315f9f974 (patch) | |
| tree | a31585dffee8046319d3b7fb7322803abcd6a702 /mppa_k1c/SelectLong.vp | |
| parent | 0dd01dbafe5125d69562640534fca6fe79fa9d82 (diff) | |
| download | compcert-kvx-fbe5ac2c9619441ad84dedf3c0cdabb315f9f974.tar.gz compcert-kvx-fbe5ac2c9619441ad84dedf3c0cdabb315f9f974.zip | |
Removing SelectLong.v from the git repo (compiled from SelectLong.vp)
Diffstat (limited to 'mppa_k1c/SelectLong.vp')
| -rw-r--r-- | mppa_k1c/SelectLong.vp | 18 |
1 files changed, 1 insertions, 17 deletions
diff --git a/mppa_k1c/SelectLong.vp b/mppa_k1c/SelectLong.vp index a3aefb15..5e94fbb5 100644 --- a/mppa_k1c/SelectLong.vp +++ b/mppa_k1c/SelectLong.vp @@ -341,29 +341,13 @@ Definition floatoflongu (e: expr) := if Archi.splitlong then SplitLong.floatoflongu e else Eop Ofloatoflongu (e:::Enil). -(* FIXME - normally we can have it natively, but in practice it requires proving that we can do Fwidenlwd + fixedd.rz.. To do later *) +(* SplitLong.longofsingle splits the operation into (longoffloat (floatofsingle e)) *) Definition longofsingle (e: expr) := SplitLong.longofsingle e. -(* - if Archi.splitlong then SplitLong.longofsingle e else - Eop Olongofsingle (e:::Enil). -*) Definition longuofsingle (e: expr) := SplitLong.longuofsingle e. -(* - if Archi.splitlong then SplitLong.longuofsingle e else - Eop Olonguofsingle (e:::Enil). -*) Definition singleoflong (e: expr) := SplitLong.singleoflong e. -(* - if Archi.splitlong then SplitLong.singleoflong e else - Eop Osingleoflong (e:::Enil). -*) Definition singleoflongu (e: expr) := SplitLong.singleoflongu e. -(* - if Archi.splitlong then SplitLong.singleoflongu e else - Eop Osingleoflongu (e:::Enil). -*) End SELECT. |