diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-11-05 17:00:20 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-11-05 17:00:20 +0100 |
| commit | f30de37bdb8ef770f238cc968c29d1158c8d8f3f (patch) | |
| tree | 5f80caecc579011ca4b90ae7e9b156cbe9abdd30 /mppa_k1c/Asmblockgen.v | |
| parent | 5397e5e8be051cf10934d59505666d335c018d90 (diff) | |
| download | compcert-kvx-f30de37bdb8ef770f238cc968c29d1158c8d8f3f.tar.gz compcert-kvx-f30de37bdb8ef770f238cc968c29d1158c8d8f3f.zip | |
MBreturn done
Diffstat (limited to 'mppa_k1c/Asmblockgen.v')
| -rw-r--r-- | mppa_k1c/Asmblockgen.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index 46b788fe..a43b0485 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -821,7 +821,7 @@ Definition transl_instr_control (f: Machblock.function) (oi: option Machblock.co (** Translation of a code sequence *) -Definition it1_is_parent (before: bool) (i: Machblock.basic_inst) : bool := +Definition fp_is_parent (before: bool) (i: Machblock.basic_inst) : bool := match i with | MBsetstack src ofs ty => before | MBgetparam ofs ty dst => negb (mreg_eq dst R10) @@ -836,7 +836,7 @@ Fixpoint transl_basic_code (f: Machblock.function) (il: list Machblock.basic_ins match il with | nil => OK nil | i1 :: il' => - do k <- transl_basic_code f il' (it1_is_parent it1p i1); + do k <- transl_basic_code f il' (fp_is_parent it1p i1); transl_instr_basic f i1 it1p k end. @@ -848,7 +848,7 @@ Fixpoint transl_basic_rec (f: Machblock.function) (il: list Machblock.basic_inst match il with | nil => k nil | i1 :: il' => - transl_basic_rec f il' (it1_is_parent it1p i1) + transl_basic_rec f il' (fp_is_parent it1p i1) (fun c1 => do c2 <- transl_instr_basic f i1 it1p c1; k c2) end. |