From d3a8a8870050810a7bc3fb5e004059197ec364f8 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 8 Apr 2020 13:06:00 +0200 Subject: print hashes --- backend/Profiling.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'backend/Profiling.v') 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 -- cgit