diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-04-19 14:01:18 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-04-19 14:01:18 +0000 |
| commit | c8ff7e933d81716dc8ac0cd380389f4269427549 (patch) | |
| tree | c042c5ecc9e8b084ce603b75b9f0554bd0f5e9ec /arm | |
| parent | fb6683f13b501844d64a8e9dad0a95cacd0f145c (diff) | |
Typos
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1640 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'arm')
| -rw-r--r-- | arm/PrintAsm.ml | 13 |
1 files changed, 5 insertions, 8 deletions
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index 44e02b9..66ee772 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -109,12 +109,10 @@ let condition_name = function let name_of_section_ELF = function | Section_text -> ".text" - | Section_data i -> if i then ".data" else ".bss" - | Section_small_data i -> if i then ".sdata" else ".sbss" - | Section_const -> ".rodata" - | Section_small_const -> ".sdata2" - | Section_string -> ".rodata" - | Section_literal -> ".section .rodata.cst8,\"aM\",%progbits,8" + | Section_data i | Section_small_data i -> if i then ".data" else ".bss" + | Section_const | Section_small_const -> ".section .rodata" + | Section_string -> ".section .rodata" + | Section_literal -> ".text" | Section_jumptable -> ".text" | Section_user(s, wr, ex) -> sprintf ".section %s,\"a%s%s\",%%progbits" @@ -663,10 +661,9 @@ let print_var oc (Coq_pair(name, v)) = fprintf oc " .align %d\n" align; if not (C2C.atom_is_static name) then fprintf oc " .global %a\n" print_symb name; - fprintf oc " .type %a, %%object\n" print_symb name; fprintf oc "%a:\n" print_symb name; print_init_data oc name v.gvar_init; - fprintf oc " .type %a, @object\n" print_symb name; + fprintf oc " .type %a, %%object\n" print_symb name; fprintf oc " .size %a, . - %a\n" print_symb name print_symb name let print_program oc p = |