diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-08 12:39:07 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-08 12:39:07 +0200 |
| commit | cce39d8408cfa33ae4cc7c586e35546a5b731dbf (patch) | |
| tree | 60c727602b4c68934209ee9407303634ec4d4c6f | |
| parent | 3c30567c452f030267d0fb09465adf8d7b44a90d (diff) | |
| download | compcert-kvx-cce39d8408cfa33ae4cc7c586e35546a5b731dbf.tar.gz compcert-kvx-cce39d8408cfa33ae4cc7c586e35546a5b731dbf.zip | |
so that it gets printed
| -rw-r--r-- | mppa_k1c/TargetPrinter.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index 930b1c51..491d2c14 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -328,6 +328,9 @@ module Target (*: TARGET*) = fprintf oc "%s begin inline assembly\n\t" comment; print_inline_asm preg_asm oc (camlstring_of_coqstring txt) sg args res; fprintf oc "%s end inline assembly\n" comment + | EF_profiling(id, kind) -> + fprintf oc "%s profiling %LX %d\n" comment + (Z.to_int64 id) (Z.to_int kind) | _ -> assert false end |