diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-08 21:29:21 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-08 21:29:21 +0200 |
| commit | d0c54b13ebe86cc6d21a534c6c5c3af6e8c6d350 (patch) | |
| tree | 7187904eff7695dc8eca237bb2af65b260a74bb5 /backend/Profiling.v | |
| parent | 3bdc0e7a5e6b4d8445001a05322086c84b11dd1e (diff) | |
| download | compcert-kvx-d0c54b13ebe86cc6d21a534c6c5c3af6e8c6d350.tar.gz compcert-kvx-d0c54b13ebe86cc6d21a534c6c5c3af6e8c6d350.zip | |
fix
Diffstat (limited to 'backend/Profiling.v')
| -rw-r--r-- | backend/Profiling.v | 6 |
1 files changed, 3 insertions, 3 deletions
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. |