diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2018-05-30 17:41:25 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2018-05-30 17:41:25 +0200 |
| commit | 616f796999a47aa12aa60b0dc39274dd4fe7a2ca (patch) | |
| tree | 0e2271997dd8f5c265e4559475676256531182b6 /mppa_k1c/Asmexpand.ml | |
| parent | 8acbfc64cd77d911076aec57e8e0a558b36e448f (diff) | |
| download | compcert-kvx-616f796999a47aa12aa60b0dc39274dd4fe7a2ca.tar.gz compcert-kvx-616f796999a47aa12aa60b0dc39274dd4fe7a2ca.zip | |
WIP - Trying to add builtins support. They are not detected for now :(
Diffstat (limited to 'mppa_k1c/Asmexpand.ml')
| -rw-r--r-- | mppa_k1c/Asmexpand.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/mppa_k1c/Asmexpand.ml b/mppa_k1c/Asmexpand.ml index f0a9404c..282fa476 100644 --- a/mppa_k1c/Asmexpand.ml +++ b/mppa_k1c/Asmexpand.ml @@ -565,11 +565,11 @@ let expand_instruction instr = | Pj_s(symb, sg) -> fixup_call sg; emit instr - | Pbuiltin (ef,args,res) -> +*)| PExpand Pbuiltin (ef,args,res) -> begin match ef with | EF_builtin (name,sg) -> expand_builtin_inline (camlstring_of_coqstring name) args res - | EF_vload chunk -> + (*| EF_vload chunk -> expand_builtin_vload chunk args res | EF_vstore chunk -> expand_builtin_vstore chunk args @@ -579,10 +579,10 @@ let expand_instruction instr = expand_builtin_memcpy (Z.to_int sz) (Z.to_int al) args | EF_annot _ | EF_debug _ | EF_inline_asm _ -> emit instr - | _ -> + *)| _ -> assert false end -*)| _ -> + | _ -> emit instr (* NOTE: Dwarf register maps for RV32G are not yet specified |