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/Asmgen.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/Asmgen.v')
| -rw-r--r-- | mppa_k1c/Asmgen.v | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v index 7b753506..15892818 100644 --- a/mppa_k1c/Asmgen.v +++ b/mppa_k1c/Asmgen.v @@ -23,4 +23,15 @@ Local Open Scope error_monad_scope. Definition transf_program (p: Mach.program) : res Asm.program := let mbp := Machblockgen.transf_program p in do abp <- Asmblockgen.transf_program mbp; - OK (Asm.transf_program abp).
\ No newline at end of file + OK (Asm.transf_program abp). + +Definition transf_function (f: Mach.function) : res function := + let mbf := Machblockgen.transf_function f in + do abf <- Asmblockgen.transf_function mbf; + OK (Asm.transf_function abf). + +Definition transl_code (f: Mach.function) (l: Mach.code) : res (list instruction) := + let mbf := Machblockgen.transf_function f in + let mbc := Machblockgen.trans_code l in + do abc <- transl_blocks mbf mbc; + OK (unfold abc).
\ No newline at end of file |