diff options
| author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2017-11-27 16:58:27 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2017-11-27 16:59:21 +0100 |
| commit | a674c56de3d0c0a9c92552a65602f026f397a886 (patch) | |
| tree | b5d37ee87278989abb57e100f7c22f9c8d7ed3db | |
| parent | 12f7b21e6e1bafe895680108e75311c678a22ac1 (diff) | |
| download | compcert-kvx-a674c56de3d0c0a9c92552a65602f026f397a886.tar.gz compcert-kvx-a674c56de3d0c0a9c92552a65602f026f397a886.zip | |
Remove temporary .o files after linking (#36)
When -c is not given, .o files are now generated in /tmp, but they are still not erased.
This commit uses an "at_exit" action to erase those temporary .o files before CompCert exits.
Using at_exit is easier to implement than explicit erasure (like we do for other temporary files), yet should not result in temporary files lingering in /tmp longer than strictly necessary, since the call to the linker is the last thing that CompCert does before exiting, hence temporary .o files are erased just after the linker returns.
| -rw-r--r-- | driver/Driver.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml index 4f27cb56..124bc587 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -61,8 +61,11 @@ let dump_jasm asm sourcename destfile = let object_filename sourcename suff = if nolink () then output_filename ~final: !option_c sourcename suff ".o" - else - Filename.temp_file "compcert" ".o" + else begin + let tmpfile = Filename.temp_file "compcert" ".o" in + at_exit (fun () -> safe_remove tmpfile); + tmpfile + end (* From CompCert C AST to asm *) |