diff options
Diffstat (limited to 'mppa_k1c/Asmblockgen.v')
| -rw-r--r-- | mppa_k1c/Asmblockgen.v | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index ade84e7b..abb24327 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -1111,10 +1111,12 @@ Definition transl_instr_control (f: Machblock.function) (oi: option Machblock.co Definition fp_is_parent (before: bool) (i: Machblock.basic_inst) : bool := match i with + | MBgetstack ofs ty dst => before && negb (mreg_eq dst MFP) | MBsetstack src ofs ty => before | MBgetparam ofs ty dst => negb (mreg_eq dst MFP) | MBop op args res => before && negb (mreg_eq res MFP) - | _ => false + | MBload chunk addr args dst => before && negb (mreg_eq dst MFP) + | MBstore chunk addr args res => before end. (** This is the naive definition, which is not tail-recursive unlike the other backends *) @@ -1183,7 +1185,7 @@ Definition transl_block (f: Machblock.function) (fb: Machblock.bblock) (ep: bool Fixpoint transl_blocks (f: Machblock.function) (lmb: list Machblock.bblock) (ep: bool) := match lmb with | nil => OK nil - | mb :: lmb => + | mb :: lmb => do lb <- transl_block f mb (if Machblock.header mb then ep else false); do lb' <- transl_blocks f lmb false; OK (lb @@ lb') |