aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authornicolas.nardino <nicolas.nardino@ens-lyon.fr>2021-06-17 17:03:53 +0200
committernicolas.nardino <nicolas.nardino@ens-lyon.fr>2021-06-17 17:03:53 +0200
commitfe557bf65ec738eaa078bc5e398ff690eb1f2b9e (patch)
tree94a3a535937d213ef9f9eb82a9887d1b3038c2ae
parentfae8d9b5c5f93d5eda36f800eb0ca1837b237cba (diff)
downloadcompcert-kvx-fe557bf65ec738eaa078bc5e398ff690eb1f2b9e.tar.gz
compcert-kvx-fe557bf65ec738eaa078bc5e398ff690eb1f2b9e.zip
changed type of schedule_seq in x86 for compatibility
-rw-r--r--x86/PrepassSchedulingOracle.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/x86/PrepassSchedulingOracle.ml b/x86/PrepassSchedulingOracle.ml
index 7b6a1b14..42a3da23 100644
--- a/x86/PrepassSchedulingOracle.ml
+++ b/x86/PrepassSchedulingOracle.ml
@@ -2,4 +2,5 @@ open RTL
open Registers
(* Do not do anything *)
-let schedule_sequence (seqa : (instruction*Regset.t) array) = None
+let schedule_sequence (seqa : (instruction*Regset.t) array)
+ live_regs_entry typing reference = None