diff options
| author | Cyril SIX <cyril.six@kalray.eu> | 2019-09-18 14:26:17 +0200 |
|---|---|---|
| committer | Cyril SIX <cyril.six@kalray.eu> | 2019-09-18 14:26:17 +0200 |
| commit | 7f1025fa2da08e68b839b7b6ea89771822dcfe83 (patch) | |
| tree | 30cf2e840c19e7ba91a9f647ed29e8c7b083f360 /mppa_k1c/PostpassSchedulingOracle.ml | |
| parent | a42baf15372e64f398685aaef079a82ea0db834e (diff) | |
| download | compcert-kvx-7f1025fa2da08e68b839b7b6ea89771822dcfe83.tar.gz compcert-kvx-7f1025fa2da08e68b839b7b6ea89771822dcfe83.zip | |
Detailing oracle/vérificateur in the timings
Diffstat (limited to 'mppa_k1c/PostpassSchedulingOracle.ml')
| -rw-r--r-- | mppa_k1c/PostpassSchedulingOracle.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml index fa61d588..327901f3 100644 --- a/mppa_k1c/PostpassSchedulingOracle.ml +++ b/mppa_k1c/PostpassSchedulingOracle.ml @@ -991,4 +991,5 @@ let rec bundles_to_coq_schedule = function (** Called schedule function from Coq *) -let schedule bb = let toto = bundles_to_coq_schedule @@ bblock_to_bundles bb in toto +let schedule_notime bb = let toto = bundles_to_coq_schedule @@ bblock_to_bundles bb in toto +let schedule bb = Timing.time_coq ('P'::('o'::('s'::('t'::('p'::('a'::('s'::('s'::('S'::('c'::('h'::('e'::('d'::('u'::('l'::('i'::('n'::('g'::(' '::('o'::('r'::('a'::('c'::('l'::('e'::([])))))))))))))))))))))))))) schedule_notime bb |