diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-10-31 12:27:31 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-10-31 12:27:31 +0100 |
| commit | 908035f9c5b64390272bf9f270df9b3691c568c0 (patch) | |
| tree | c7fbdb160c8802dd0c077d0a704eba0d5dfb4c54 /mppa_k1c/Asmblockgen.v | |
| parent | 9b63f18830e480b95209751c7cd689eba952b19f (diff) | |
| download | compcert-kvx-908035f9c5b64390272bf9f270df9b3691c568c0.tar.gz compcert-kvx-908035f9c5b64390272bf9f270df9b3691c568c0.zip | |
Setting ep to false when the basicblock has a header. MBgoto done. MBgetparam needs fix
Diffstat (limited to 'mppa_k1c/Asmblockgen.v')
| -rw-r--r-- | mppa_k1c/Asmblockgen.v | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index ceee1810..46b788fe 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -903,14 +903,12 @@ Fixpoint transl_blocks (f: Machblock.function) (lmb: list Machblock.bblock) (ep: match lmb with | nil => OK nil | mb :: lmb => - do lb <- transl_block f mb ep; + do lb <- transl_block f mb (if Machblock.header mb then ep else false); do lb' <- transl_blocks f lmb false; OK (lb ++ lb') end . - - Definition transl_function (f: Machblock.function) := do lb <- transl_blocks f f.(Machblock.fn_code) true; OK (mkfunction f.(Machblock.fn_sig) |