diff options
| author | Michael Schmidt <github@mschmidt.me> | 2015-10-14 15:07:48 +0200 |
|---|---|---|
| committer | Michael Schmidt <github@mschmidt.me> | 2015-10-14 15:07:48 +0200 |
| commit | 60ab550a952c3d9719b2a91ec90c9b58769f6717 (patch) | |
| tree | 523cf4eb5a35594b16a297b4bd7e29157f42b0fc /common | |
| parent | a479c280441b91007c379b0b63b907926d54f930 (diff) | |
| download | compcert-kvx-60ab550a952c3d9719b2a91ec90c9b58769f6717.tar.gz compcert-kvx-60ab550a952c3d9719b2a91ec90c9b58769f6717.zip | |
bug 17392: remove trailing whitespace in source files
Diffstat (limited to 'common')
| -rw-r--r-- | common/PrintAST.ml | 8 | ||||
| -rw-r--r-- | common/Sections.ml | 6 | ||||
| -rw-r--r-- | common/Switchaux.ml | 2 |
3 files changed, 8 insertions, 8 deletions
diff --git a/common/PrintAST.ml b/common/PrintAST.ml index aea8ff0f..d1825def 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 diff --git a/common/Sections.ml b/common/Sections.ml index 0910f2dc..93783155 100644 --- a/common/Sections.ml +++ b/common/Sections.ml @@ -58,7 +58,7 @@ let default_section_info = { let builtin_sections = [ "CODE", - {sec_name_init = Section_text; + {sec_name_init = Section_text; sec_name_uninit = Section_text; sec_writable = false; sec_executable = true; sec_access = Access_default}; @@ -119,7 +119,7 @@ let initialize () = (* Define or update a given section. *) let define_section name ?iname ?uname ?writable ?executable ?access () = - let si = + let si = try Hashtbl.find current_section_table name with Not_found -> default_section_info in let writable = @@ -218,7 +218,7 @@ let for_function env id ty_res = with Not_found -> assert false in [si_code.sec_name_init; si_literal.sec_name_init; si_jumptbl.sec_name_init] - + (* Determine section for a string literal *) let for_stringlit() = diff --git a/common/Switchaux.ml b/common/Switchaux.ml index 39b484c7..0d4901bf 100644 --- a/common/Switchaux.ml +++ b/common/Switchaux.ml @@ -50,7 +50,7 @@ let compile_switch_as_tree modulus default tbl = let (key1, act1) = sw.(lo) and (key2, act2) = sw.(lo+1) and (key3, act3) = sw.(lo+2) in - CTifeq(key1, act1, + CTifeq(key1, act1, CTifeq(key2, act2, if Z.sub maxval minval = Z.of_uint 2 then CTaction act3 |