From d0c54b13ebe86cc6d21a534c6c5c3af6e8c6d350 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 8 Apr 2020 21:29:21 +0200 Subject: fix --- backend/Profiling.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'backend/Profiling.v') diff --git a/backend/Profiling.v b/backend/Profiling.v index 0dfc0a0b..4cba49ee 100644 --- a/backend/Profiling.v +++ b/backend/Profiling.v @@ -15,9 +15,9 @@ Section PER_FUNCTION_ID. 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 + (Ibuiltin (EF_profiling id 0%Z) nil BR_none ifnot) prog in let prog'':= PTree.set extra_pc' - (Ibuiltin (EF_profiling id 1%Z) nil BR_none ifnot) prog' in + (Ibuiltin (EF_profiling id 1%Z) nil BR_none ifso) prog' in (Pos.succ extra_pc', prog''). Definition inject_at (prog : code) (pc extra_pc : node) : node * code := @@ -25,7 +25,7 @@ Section PER_FUNCTION_ID. | Some (Icond cond args ifso ifnot expected) => inject_profiling_call (PTree.set pc - (Icond cond args extra_pc (Pos.succ extra_pc) expected) prog) + (Icond cond args (Pos.succ extra_pc) extra_pc expected) prog) pc extra_pc ifso ifnot | _ => inject_profiling_call prog pc extra_pc 1 1 (* does not happen *) end. -- cgit