aboutsummaryrefslogtreecommitdiffstats
path: root/x86
diff options
context:
space:
mode:
authorLéo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>2021-09-01 16:39:13 +0200
committerLéo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>2021-09-01 16:39:13 +0200
commita4c7a7240a93e874779027a6a3d41ccebc81b396 (patch)
tree2c0bd9a40ac0abee7260790ace9babb9d01ee815 /x86
parentc620afbf97a3f6b299bcf2cc14edafa0120a4bc2 (diff)
downloadcompcert-kvx-a4c7a7240a93e874779027a6a3d41ccebc81b396.tar.gz
compcert-kvx-a4c7a7240a93e874779027a6a3d41ccebc81b396.zip
fix stub for no-prepass archs...
Diffstat (limited to 'x86')
-rw-r--r--x86/PrepassSchedulingOracle.ml5
1 files changed, 3 insertions, 2 deletions
diff --git a/x86/PrepassSchedulingOracle.ml b/x86/PrepassSchedulingOracle.ml
index 31b4ea5b..a8ba6720 100644
--- a/x86/PrepassSchedulingOracle.ml
+++ b/x86/PrepassSchedulingOracle.ml
@@ -1,3 +1,4 @@
-
(* Do not do anything *)
-let schedule_sequence inst btl = None
+let schedule_sequence seqa btl (live_regs_entry : Registers.Regset.t)
+ (typing : RTLtyping.regenv) reference =
+ None