diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-11 10:29:45 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-11 10:29:45 +0200 |
| commit | f50a1c1e1dc194c78b68ecdc7e3f6c0b0448f5f4 (patch) | |
| tree | 0996c636ec65dbf876652855b4013a8220623a42 /backend/PrintAsmaux.ml | |
| parent | 1f6cb381b91fc40d1e6b7c6ae1f022077f6091de (diff) | |
| download | compcert-kvx-f50a1c1e1dc194c78b68ecdc7e3f6c0b0448f5f4.tar.gz compcert-kvx-f50a1c1e1dc194c78b68ecdc7e3f6c0b0448f5f4.zip | |
seems like the ARM profiling perhaps works
Diffstat (limited to 'backend/PrintAsmaux.ml')
| -rw-r--r-- | backend/PrintAsmaux.ml | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml index c7161615..cc7b33c3 100644 --- a/backend/PrintAsmaux.ml +++ b/backend/PrintAsmaux.ml @@ -358,11 +358,7 @@ let write_symbol_pointer oc sym = then fprintf oc " .8byte %s\n" sym else fprintf oc " .4byte %s\n" sym;; -let declare_function oc name = - fprintf oc " .type %s, @function\n" name; - fprintf oc " .size %s, . - %s\n" name name;; - -let print_profiling_epilogue finalizer_call_method print_profiling_stub oc = +let print_profiling_epilogue declare_function finalizer_call_method print_profiling_stub oc = let nr_items = !next_profiling_position in if nr_items > 0 then |