diff options
author | Bernhard Schommer <bschommer@users.noreply.github.com> | 2019-09-12 17:03:14 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-09-12 17:03:14 +0200 |
commit | a7c8e4f4ef4a5f0a15283cd3f0999f3fa24e581d (patch) | |
tree | a2960647cb46ecb19a6a63539f2a894df7fd1474 /backend/JsonAST.mli | |
parent | f3bdf0c70faa9e69359bd06b78570c60a569a7cb (diff) | |
download | compcert-kvx-a7c8e4f4ef4a5f0a15283cd3f0999f3fa24e581d.tar.gz compcert-kvx-a7c8e4f4ef4a5f0a15283cd3f0999f3fa24e581d.zip |
Reworked json export.
The json export prints formatted json, which takes a lot of
additional time, however the result is only consumed by other tools
and not meant for human reading.
This commit implements several small changes in order to speedup
the json export:
* Removal of usage of the Format Module
* Replacing `fprintf` calls by calls to function that print
directly, such as `output_string`, etc.
* Replacing list of all instruction names by a set of all
instructions
Diffstat (limited to 'backend/JsonAST.mli')
-rw-r--r-- | backend/JsonAST.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/backend/JsonAST.mli b/backend/JsonAST.mli index 7afdce51..c32439e4 100644 --- a/backend/JsonAST.mli +++ b/backend/JsonAST.mli @@ -13,4 +13,4 @@ val pp_mnemonics : Format.formatter -> string list -> unit -val pp_ast : Format.formatter -> (Format.formatter -> Asm.code -> unit) -> (Asm.coq_function AST.fundef, 'a) AST.program -> string -> unit +val pp_ast : out_channel -> (out_channel -> Asm.code -> unit) -> (Asm.coq_function AST.fundef, 'a) AST.program -> string -> unit |