diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-08 15:21:37 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-08 15:21:37 +0200 |
commit | 74699fa95d096dfc5b9ed7d60aaf1a1338bfc950 (patch) | |
tree | 1b0069a65ba56c5d6580520abfff8c19edc3aa18 /mppa_k1c/PostpassSchedulingOracle.ml | |
parent | a57ba1a8a0036853cac31d9401a6f71b877e70c1 (diff) | |
download | compcert-kvx-74699fa95d096dfc5b9ed7d60aaf1a1338bfc950.tar.gz compcert-kvx-74699fa95d096dfc5b9ed7d60aaf1a1338bfc950.zip |
notrap in mppa_k1c ML code
Diffstat (limited to 'mppa_k1c/PostpassSchedulingOracle.ml')
-rw-r--r-- | mppa_k1c/PostpassSchedulingOracle.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml index fa61d588..41dac766 100644 --- a/mppa_k1c/PostpassSchedulingOracle.ml +++ b/mppa_k1c/PostpassSchedulingOracle.ml @@ -302,7 +302,7 @@ let arith_rec i = | PArithR (i, rd) -> arith_r_rec i (IR rd) let load_rec i = match i with - | PLoadRRO (i, rs1, rs2, imm) -> + | PLoadRRO (trap, i, rs1, rs2, imm) -> { inst = load_real i; write_locs = [Reg (IR rs1)]; read_locs = [Mem; Reg (IR rs2)]; imm = (Some (Off imm)) ; is_control = false; read_at_id = []; read_at_e1 = [] } | PLoadQRRO(rs, ra, imm) -> @@ -313,7 +313,7 @@ let load_rec i = match i with let (((rs0, rs1), rs2), rs3) = gpreg_o_expand rs in { inst = loadorro_real; write_locs = [Reg (IR rs0); Reg (IR rs1); Reg (IR rs2); Reg (IR rs3)]; read_locs = [Mem; Reg (IR ra)]; imm = (Some (Off imm)) ; is_control = false; read_at_id = []; read_at_e1 = []} - | PLoadRRR (i, rs1, rs2, rs3) | PLoadRRRXS (i, rs1, rs2, rs3) -> + | PLoadRRR (trap, i, rs1, rs2, rs3) | PLoadRRRXS (trap, i, rs1, rs2, rs3) -> { inst = load_real i; write_locs = [Reg (IR rs1)]; read_locs = [Mem; Reg (IR rs2); Reg (IR rs3)]; imm = None ; is_control = false; read_at_id = []; read_at_e1 = [] } |