diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-08 13:06:00 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-08 13:06:00 +0200 |
| commit | d3a8a8870050810a7bc3fb5e004059197ec364f8 (patch) | |
| tree | 8368172ddd21e31aea993c80a9740e8b1a2d9706 /backend/Profiling.v | |
| parent | cce39d8408cfa33ae4cc7c586e35546a5b731dbf (diff) | |
| download | compcert-kvx-d3a8a8870050810a7bc3fb5e004059197ec364f8.tar.gz compcert-kvx-d3a8a8870050810a7bc3fb5e004059197ec364f8.zip | |
print hashes
Diffstat (limited to 'backend/Profiling.v')
| -rw-r--r-- | backend/Profiling.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/backend/Profiling.v b/backend/Profiling.v index 1840af6e..0dfc0a0b 100644 --- a/backend/Profiling.v +++ b/backend/Profiling.v @@ -4,15 +4,15 @@ Require Import Memory Registers Op RTL. Local Open Scope positive. -Parameter function_id : function -> Z. -Parameter branch_id : Z -> node -> Z. +Parameter function_id : function -> AST.profiling_id. +Parameter branch_id : AST.profiling_id -> node -> AST.profiling_id. Section PER_FUNCTION_ID. - Variable function_id : Z. + Variable f_id : AST.profiling_id. Definition inject_profiling_call (prog : code) (pc extra_pc ifso ifnot : node) : node * code := - let id := branch_id function_id pc in + let id := branch_id f_id pc in let extra_pc' := Pos.succ extra_pc in let prog' := PTree.set extra_pc (Ibuiltin (EF_profiling id 0%Z) nil BR_none ifso) prog in |