diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2015-10-11 09:58:17 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2015-10-11 09:58:17 +0200 |
| commit | 659b735ed2dbefcbe8bcb2ec2123b66019ddaf14 (patch) | |
| tree | 916aa2c5fc22e97b040b540a4edcc76e2dd5062d /exportclight/ExportClight.ml | |
| parent | f8bc6863f72948b8041289e200ff1d8b1f63a342 (diff) | |
| download | compcert-kvx-659b735ed2dbefcbe8bcb2ec2123b66019ddaf14.tar.gz compcert-kvx-659b735ed2dbefcbe8bcb2ec2123b66019ddaf14.zip | |
Upgrade to reflect changes in type external_function.
Diffstat (limited to 'exportclight/ExportClight.ml')
| -rw-r--r-- | exportclight/ExportClight.ml | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml index 9563d551..82066cc9 100644 --- a/exportclight/ExportClight.ml +++ b/exportclight/ExportClight.ml @@ -250,10 +250,6 @@ let external_function p = function fprintf p "(EF_vload %s)" (name_of_chunk chunk) | EF_vstore chunk -> fprintf p "(EF_vstore %s)" (name_of_chunk chunk) - | EF_vload_global(chunk, id, ofs) -> - fprintf p "(EF_vload_global %s %a %a)" (name_of_chunk chunk) ident id coqint ofs - | EF_vstore_global(chunk, id, ofs) -> - fprintf p "(EF_vstore_global %s %a %a)" (name_of_chunk chunk) ident id coqint ofs | EF_malloc -> fprintf p "EF_malloc" | EF_free -> fprintf p "EF_free" | EF_memcpy(sz, al) -> @@ -264,6 +260,8 @@ let external_function p = function | EF_annot_val(text, targ) -> assertions := (text, [targ]) :: !assertions; fprintf p "(EF_annot_val %ld%%positive %a)" (P.to_int32 text) asttype targ + | EF_debug(kind, text, targs) -> + fprintf p "(EF_debug %ld%%positive %ld%%positive %a)" (P.to_int32 kind) (P.to_int32 text) (print_list asttype) targs | EF_inline_asm(text, sg, clob) -> fprintf p "@[<hov 2>(EF_inline_asm %ld%%positive@ %a@ %a)@]" (P.to_int32 text) |