diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-11 22:02:46 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-11 22:02:46 +0200 |
| commit | 7299996cac6c4747b6611b17f0af15fb08c6ee80 (patch) | |
| tree | 744b3f37834356ebb13c45097fc4740ffb4d16ea /backend/PrintAsmaux.ml | |
| parent | 7d15566ad116730c1452364bc0fe3d2dc714e5ed (diff) | |
| download | compcert-kvx-7299996cac6c4747b6611b17f0af15fb08c6ee80.tar.gz compcert-kvx-7299996cac6c4747b6611b17f0af15fb08c6ee80.zip | |
fix reverse printing problem for hashes
Diffstat (limited to 'backend/PrintAsmaux.ml')
| -rw-r--r-- | backend/PrintAsmaux.ml | 54 |
1 files changed, 28 insertions, 26 deletions
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index 25792df5..7a281684 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -363,33 +363,35 @@ let write_symbol_pointer oc sym = else fprintf oc " .4byte %s\n" sym;; let print_profiling_epilogue declare_function finalizer_call_method print_profiling_stub oc = - let nr_items = !next_profiling_position in - if nr_items > 0 + if !Clflags.option_profile_arcs then - begin - fprintf oc " .lcomm %s, %d\n" - profiling_counter_table_name (nr_items * 16); - fprintf oc " .section .rodata\n"; - fprintf oc "%s:\n" profiling_id_table_name; - Array.iter (print_profiling_id oc) (profiling_ids ()); - fprintf oc " .text\n"; - fprintf oc "%s:\n" profiling_write_table; - print_profiling_stub oc nr_items - profiling_id_table_name - profiling_counter_table_name; - declare_function oc profiling_write_table; - match finalizer_call_method with - | Dtors -> - fprintf oc " .section %s\n" dtor_section; - write_symbol_pointer oc profiling_write_table - | Init_atexit(atexit_call) -> - fprintf oc " .section %s\n" init_section; - write_symbol_pointer oc profiling_init; - fprintf oc " .text\n"; - fprintf oc "%s:\n" profiling_init; - atexit_call oc profiling_write_table; - declare_function oc profiling_init - end;; + let nr_items = !next_profiling_position in + if nr_items > 0 + then + begin + fprintf oc " .lcomm %s, %d\n" + profiling_counter_table_name (nr_items * 16); + fprintf oc " .section .rodata\n"; + fprintf oc "%s:\n" profiling_id_table_name; + Array.iter (print_profiling_id oc) (profiling_ids ()); + fprintf oc " .text\n"; + fprintf oc "%s:\n" profiling_write_table; + print_profiling_stub oc nr_items + profiling_id_table_name + profiling_counter_table_name; + declare_function oc profiling_write_table; + match finalizer_call_method with + | Dtors -> + fprintf oc " .section %s\n" dtor_section; + write_symbol_pointer oc profiling_write_table + | Init_atexit(atexit_call) -> + fprintf oc " .section %s\n" init_section; + write_symbol_pointer oc profiling_init; + fprintf oc " .text\n"; + fprintf oc "%s:\n" profiling_init; + atexit_call oc profiling_write_table; + declare_function oc profiling_init + end;; let profiling_offset id kind = ((profiling_position id)*2 + kind)*8;; |