diff options
author | Cyril SIX <cyril.six@kalray.eu> | 2018-09-05 15:15:48 +0200 |
---|---|---|
committer | Cyril SIX <cyril.six@kalray.eu> | 2018-09-06 15:59:07 +0200 |
commit | 672d9ea4489158f6a6b7175463c6514a91d1490d (patch) | |
tree | bd358992610110b8c7ebdefb5979ef30f601215a /mppa_k1c/Asmblockgen.v | |
parent | 5a78e28f0bd7e8f822d96c4ad24ab20cca8fedd1 (diff) | |
download | compcert-kvx-672d9ea4489158f6a6b7175463c6514a91d1490d.tar.gz compcert-kvx-672d9ea4489158f6a6b7175463c6514a91d1490d.zip |
Rajout d'un return_address_offset. Besoin de changer forward_simu de mach machblock
Diffstat (limited to 'mppa_k1c/Asmblockgen.v')
-rw-r--r-- | mppa_k1c/Asmblockgen.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index 4bb23e8e..79c28fe9 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -872,7 +872,7 @@ Fixpoint transl_blocks (f: Machblock.function) (lmb: list Machblock.bblock) := end . -Definition transl_function (f: Machblock.function) := +Definition transf_function (f: Machblock.function) := do lb <- transl_blocks f f.(Machblock.fn_code); OK (mkfunction f.(Machblock.fn_sig) (Pallocframe f.(fn_stacksize) f.(fn_link_ofs) ::b @@ -889,7 +889,7 @@ Definition transl_function (f: Machblock.function) := Definition transf_fundef (f: Machblock.fundef) : res Asmblock.fundef := - transf_partial_fundef transl_function f. + transf_partial_fundef transf_function f. Definition transf_program (p: Machblock.program) : res Asmblock.program := transform_partial_program transf_fundef p. |