diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-08 11:35:17 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-08 11:35:17 +0200 |
| commit | 1972df30827022dcb39110cddf9032eaa3dc61b9 (patch) | |
| tree | 37a7e62cbe08675ca56d2f734104bd2d164f74e0 /common/AST.v | |
| parent | 66f700d36891a90983bb97d245e04a2e97913c7d (diff) | |
| download | compcert-kvx-1972df30827022dcb39110cddf9032eaa3dc61b9.tar.gz compcert-kvx-1972df30827022dcb39110cddf9032eaa3dc61b9.zip | |
begin installing profiling
Diffstat (limited to 'common/AST.v')
| -rw-r--r-- | common/AST.v | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/common/AST.v b/common/AST.v index 595ace01..846678c2 100644 --- a/common/AST.v +++ b/common/AST.v @@ -466,6 +466,7 @@ Qed. (* Identifiers for profiling information *) Definition profiling_id := Z.t. +Definition profiling_kind := Z.t. (** For most languages, the functions composing the program are either internal functions, defined within the language, or external functions, @@ -521,8 +522,8 @@ Inductive external_function : Type := (** Transport debugging information from the front-end to the generated assembly. Takes zero, one or several arguments like [EF_annot]. Unlike [EF_annot], produces no observable event. *) - | EF_profiling (id: profiling_id). - (** Count one profiling event for this identifier. + | EF_profiling (id: profiling_id) (kind : profiling_kind). + (** Count one profiling event for this identifier and kind. Takes no argument. Produces no observable event. *) (** The type signature of an external function. *) @@ -541,7 +542,7 @@ Definition ef_sig (ef: external_function): signature := | EF_annot_val kind text targ => mksignature (targ :: nil) targ cc_default | EF_inline_asm text sg clob => sg | EF_debug kind text targs => mksignature targs Tvoid cc_default - | EF_profiling id => mksignature nil Tvoid cc_default + | EF_profiling id kind => mksignature nil Tvoid cc_default end. (** Whether an external function should be inlined by the compiler. *) @@ -560,7 +561,7 @@ Definition ef_inline (ef: external_function) : bool := | EF_annot_val kind Text rg => true | EF_inline_asm text sg clob => true | EF_debug kind text targs => true - | EF_profiling id => true + | EF_profiling id kind => true end. (** Whether an external function must reload its arguments. *) |