diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-20 13:32:18 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2015-10-20 13:32:18 +0200 |
| commit | 4d542bc7eafadb16b845cf05d1eb4988eb55ed0f (patch) | |
| tree | 1961b41815fc6e392cc0bd2beeb0fb504bc160ce /common/PrintAST.ml | |
| parent | 7a6bb90048db7a254e959b1e3c308bac5fe6c418 (diff) | |
| download | compcert-kvx-4d542bc7eafadb16b845cf05d1eb4988eb55ed0f.tar.gz compcert-kvx-4d542bc7eafadb16b845cf05d1eb4988eb55ed0f.zip | |
Updated PR by removing whitespaces. Bug 17450.
Diffstat (limited to 'common/PrintAST.ml')
| -rw-r--r-- | common/PrintAST.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/common/PrintAST.ml b/common/PrintAST.ml index 67b5eb9d..39481bfb 100644 --- a/common/PrintAST.ml +++ b/common/PrintAST.ml @@ -57,17 +57,17 @@ let rec print_builtin_arg px oc = function | BA_long n -> fprintf oc "long %Ld" (camlint64_of_coqint n) | BA_float n -> fprintf oc "float %F" (camlfloat_of_coqfloat n) | BA_single n -> fprintf oc "single %F" (camlfloat_of_coqfloat32 n) - | BA_loadstack(chunk, ofs) -> + | BA_loadstack(chunk, ofs) -> fprintf oc "%s[sp + %ld]" (name_of_chunk chunk) (camlint_of_coqint ofs) | BA_addrstack(ofs) -> fprintf oc "sp + %ld" (camlint_of_coqint ofs) - | BA_loadglobal(chunk, id, ofs) -> + | BA_loadglobal(chunk, id, ofs) -> fprintf oc "%s[&%s + %ld]" (name_of_chunk chunk) (extern_atom id) (camlint_of_coqint ofs) | BA_addrglobal(id, ofs) -> fprintf oc "&%s + %ld" (extern_atom id) (camlint_of_coqint ofs) | BA_splitlong(hi, lo) -> - fprintf oc "splitlong(%a, %a)" + fprintf oc "splitlong(%a, %a)" (print_builtin_arg px) hi (print_builtin_arg px) lo let rec print_builtin_args px oc = function @@ -80,6 +80,6 @@ let rec print_builtin_res px oc = function | BR x -> px oc x | BR_none -> fprintf oc "_" | BR_splitlong(hi, lo) -> - fprintf oc "splitlong(%a, %a)" + fprintf oc "splitlong(%a, %a)" (print_builtin_res px) hi (print_builtin_res px) lo |