diff options
Diffstat (limited to 'backend/Inlining.v')
| -rw-r--r-- | backend/Inlining.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/backend/Inlining.v b/backend/Inlining.v index f7ee4166..9cf535b9 100644 --- a/backend/Inlining.v +++ b/backend/Inlining.v @@ -364,9 +364,9 @@ Definition expand_instr (ctx: context) (pc: node) (i: instruction): mon unit := | Iop op args res s => set_instr (spc ctx pc) (Iop (sop ctx op) (sregs ctx args) (sreg ctx res) (spc ctx s)) - | Iload chunk addr args dst s => + | Iload trap chunk addr args dst s => set_instr (spc ctx pc) - (Iload chunk (saddr ctx addr) (sregs ctx args) (sreg ctx dst) (spc ctx s)) + (Iload trap chunk (saddr ctx addr) (sregs ctx args) (sreg ctx dst) (spc ctx s)) | Istore chunk addr args src s => set_instr (spc ctx pc) (Istore chunk (saddr ctx addr) (sregs ctx args) (sreg ctx src) (spc ctx s)) |