summaryrefslogtreecommitdiff
path: root/common
diff options
context:
space:
mode:
Diffstat (limited to 'common')
-rw-r--r--common/PrintAST.ml8
1 files changed, 4 insertions, 4 deletions
diff --git a/common/PrintAST.ml b/common/PrintAST.ml
index 6a66c30..53741d5 100644
--- a/common/PrintAST.ml
+++ b/common/PrintAST.ml
@@ -29,15 +29,15 @@ let name_of_chunk = function
| Mfloat64al32 -> "float64al32"
let name_of_external = function
- | EF_external(name, sg) -> extern_atom name
- | EF_builtin(name, sg) -> extern_atom name
+ | EF_external(name, sg) -> sprintf "extern %S" (extern_atom name)
+ | EF_builtin(name, sg) -> sprintf "builtin %S" (extern_atom name)
| EF_vload chunk -> sprintf "volatile load %s" (name_of_chunk chunk)
| EF_vstore chunk -> sprintf "volatile store %s" (name_of_chunk chunk)
| EF_vload_global(chunk, id, ofs) ->
- sprintf "volatile load %s global %s %ld"
+ sprintf "volatile load %s global %S %ld"
(name_of_chunk chunk) (extern_atom id) (camlint_of_coqint ofs)
| EF_vstore_global(chunk, id, ofs) ->
- sprintf "volatile store %s global %s %ld"
+ sprintf "volatile store %s global %S %ld"
(name_of_chunk chunk) (extern_atom id) (camlint_of_coqint ofs)
| EF_malloc -> "malloc"
| EF_free -> "free"