diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-11-28 14:24:01 +0100 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-11-28 14:24:01 +0100 |
| commit | 5568558f61a13754cc9f80d5e9641c6e9e9bc742 (patch) | |
| tree | e34df72baf8308857393b2b2b11e8ce2e8b2199e /mppa_k1c/Asmgen.v | |
| parent | 8d646d93ce0a6611cf55561450e39a82fa464fe6 (diff) | |
| download | compcert-kvx-5568558f61a13754cc9f80d5e9641c6e9e9bc742.tar.gz compcert-kvx-5568558f61a13754cc9f80d5e9641c6e9e9bc742.zip | |
mppa_k1c compiles
Diffstat (limited to 'mppa_k1c/Asmgen.v')
| -rw-r--r-- | mppa_k1c/Asmgen.v | 7 |
1 files changed, 1 insertions, 6 deletions
diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v index 9b9e6272..6f61747f 100644 --- a/mppa_k1c/Asmgen.v +++ b/mppa_k1c/Asmgen.v @@ -21,11 +21,6 @@ Require Import Errors. Local Open Scope error_monad_scope. -(** For OCaml code *) -Definition addptrofs (rd rs: ireg) (n: ptrofs) := basic_to_instruction (addptrofs rd rs n). -Definition storeind_ptr (src: ireg) (base: ireg) (ofs: ptrofs) := - basic_to_instruction (storeind_ptr src base ofs). - Definition transf_program (p: Mach.program) : res Asm.program := let mbp := Machblockgen.transf_program p in do abp <- Asmblockgen.transf_program mbp; @@ -40,4 +35,4 @@ Definition transl_code (f: Mach.function) (l: Mach.code) : res (list Asm.instruc let mbf := Machblockgen.transf_function f in let mbc := Machblockgen.trans_code l in do abc <- transl_blocks mbf mbc true; - OK (unfold abc).
\ No newline at end of file + OK (unfold abc). |