diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-09-25 17:37:14 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2017-09-25 17:38:30 +0200 |
| commit | c0da0f3a550887c84982722c3b9596f03dc97e61 (patch) | |
| tree | f93ed7a3e19a45a03256e92093a4ecc268943d71 /driver | |
| parent | 8d5c6bb8f0cac1339dec7b730997ee30b1517073 (diff) | |
| download | compcert-c0da0f3a550887c84982722c3b9596f03dc97e61.tar.gz compcert-c0da0f3a550887c84982722c3b9596f03dc97e61.zip | |
Added dump-mnemonics option.
This option allows it to dump a list of all used mnemonics into
a file.
Bug 22239
Diffstat (limited to 'driver')
| -rw-r--r-- | driver/Driver.ml | 14 |
1 files changed, 12 insertions, 2 deletions
diff --git a/driver/Driver.ml b/driver/Driver.ml index a09aa95d..6996f537 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -311,6 +311,14 @@ let enforce_buildnr nr = Please use matching builds of QSK and CompCert.\n" build nr; exit 2 end +let dump_mnemonics destfile = + let oc = open_out_bin destfile in + let pp = Format.formatter_of_out_channel oc in + AsmToJSON.pp_mnemonics pp; + Format.pp_print_flush pp (); + close_out oc; + exit 0 + let language_support_options = [ option_fbitfields; option_flongdouble; option_fstruct_passing; option_fvararg_calls; option_funprototyped; @@ -338,10 +346,12 @@ let cmdline_actions = (* Getting version info *) Exact "-version", Unit print_version_and_exit; Exact "--version", Unit print_version_and_exit;] @ -(* Enforcing CompCert build numbers for QSKs *) +(* Enforcing CompCert build numbers for QSKs and mnemonics dump *) (if Version.buildnr <> "" then [ Exact "-qsk-enforce-build", Integer enforce_buildnr; - Exact "--qsk-enforce-build", Integer enforce_buildnr; ] + Exact "--qsk-enforce-build", Integer enforce_buildnr; + Exact "-dump-mnemonics", String dump_mnemonics; + ] else []) @ (* Processing options *) [ Exact "-c", Set option_c; |