diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-03 09:25:48 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-05-03 09:25:48 +0200 |
| commit | 92b48e2aa6d24d1ad487c1d2a3644a57966c765e (patch) | |
| tree | 9ae13a1917a968992338a81a9a4a9fbb62df3222 /mppa_k1c/PostpassSchedulingOracle.ml | |
| parent | c56f9a47fe1837b7afb73c2c24aed9228bc0db08 (diff) | |
| download | compcert-kvx-92b48e2aa6d24d1ad487c1d2a3644a57966c765e.tar.gz compcert-kvx-92b48e2aa6d24d1ad487c1d2a3644a57966c765e.zip | |
rm Ofslow (résidu du Risc-V, inutilisé et complique les preuves)
Diffstat (limited to 'mppa_k1c/PostpassSchedulingOracle.ml')
| -rw-r--r-- | mppa_k1c/PostpassSchedulingOracle.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml index abc3dcb6..033cf943 100644 --- a/mppa_k1c/PostpassSchedulingOracle.ml +++ b/mppa_k1c/PostpassSchedulingOracle.ml @@ -544,9 +544,8 @@ exception InvalidEncoding let rec_to_usage r = let encoding = match r.imm with None -> None | Some (I32 i) | Some (I64 i) -> Some (encode_imm @@ Z.to_int64 i) - | Some (Off (Ofsimm ptr)) -> Some (encode_imm @@ camlint64_of_ptrofs ptr) - | Some (Off (Ofslow (_, _))) -> Some E27U27L10 (* FIXME *) - (* I do not know yet in which context Ofslow can be used by CompCert *) + | Some (Off ptr) -> Some (encode_imm @@ camlint64_of_ptrofs ptr) + and real_inst = ab_inst_to_real r.inst in match real_inst with | Addw | Andw | Nandw | Orw | Norw | Sbfw | Xorw |