aboutsummaryrefslogtreecommitdiffstats
path: root/kvx
diff options
context:
space:
mode:
authorDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-07-10 22:42:27 +0200
committerDavid Monniaux <david.monniaux@univ-grenoble-alpes.fr>2020-07-10 22:42:27 +0200
commitba39e941a47a87ecc67795f955cc24e5c1266428 (patch)
treec206188c2a8fdd867ca269f26f062b9cadde1c11 /kvx
parent7abe728fea66e04db905df7fc1899904690560af (diff)
downloadcompcert-kvx-ba39e941a47a87ecc67795f955cc24e5c1266428.tar.gz
compcert-kvx-ba39e941a47a87ecc67795f955cc24e5c1266428.zip
fix the last instruction detection code
Diffstat (limited to 'kvx')
-rw-r--r--kvx/lib/RTLpathScheduleraux.ml7
1 files changed, 5 insertions, 2 deletions
diff --git a/kvx/lib/RTLpathScheduleraux.ml b/kvx/lib/RTLpathScheduleraux.ml
index 12637a9d..1b8ea20a 100644
--- a/kvx/lib/RTLpathScheduleraux.ml
+++ b/kvx/lib/RTLpathScheduleraux.ml
@@ -112,8 +112,11 @@ let schedule_superblock sb code =
let nr_instr = Array.length sb.instructions in
let trailer_length =
match PTree.get (sb.instructions.(nr_instr-1)) code with
- | Some (Ireturn _ | Itailcall _ | Ijumptable _ | Icall _) -> 1
- | _ -> 0 in
+ | None -> 0
+ | Some ii ->
+ match predicted_successor ii with
+ | Some _ -> 0
+ | None -> 1 in
match PrepassSchedulingOracle.schedule_sequence
(Array.map (fun i ->
(match PTree.get i code with