diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-12 08:30:14 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-12 08:30:14 +0200 |
| commit | 8bbb1bbaad236901afea1cbb7033dcc097e7b94e (patch) | |
| tree | 4fc77dbea8d13c81c977e07f277310232a0446a8 /x86 | |
| parent | 40cd35c9152ceba673e255ee1d6108e224a54c3f (diff) | |
| download | compcert-kvx-8bbb1bbaad236901afea1cbb7033dcc097e7b94e.tar.gz compcert-kvx-8bbb1bbaad236901afea1cbb7033dcc097e7b94e.zip | |
fix IA32 profiling bug
Diffstat (limited to 'x86')
| -rw-r--r-- | x86/TargetPrinter.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/x86/TargetPrinter.ml b/x86/TargetPrinter.ml index 3ffad3d0..b690c817 100644 --- a/x86/TargetPrinter.ml +++ b/x86/TargetPrinter.ml @@ -176,7 +176,8 @@ module ELF_System : SYSTEM = begin fprintf oc " pushl $%s\n" to_be_called; fprintf oc " call atexit\n"; - fprintf oc " addl $4, %%esp\n" + fprintf oc " addl $4, %%esp\n"; + fprintf oc " ret\n" end let x86_profiling_stub oc nr_items @@ -196,7 +197,8 @@ module ELF_System : SYSTEM = fprintf oc " pushl $%s\n" profiling_id_table_name; fprintf oc " pushl $%d\n" nr_items; fprintf oc " call %s\n" profiling_write_table_helper ; - fprintf oc " addl $12, %%esp\n" + fprintf oc " addl $12, %%esp\n"; + fprintf oc " ret\n" end;; let print_epilogue oc = |