diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-07-20 15:21:29 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-07-20 15:21:29 +0200 |
| commit | a3319eb05543930844dedd9ac31ed1beaac3047e (patch) | |
| tree | a9745571f4ed7841f4c231505df9102f3e84ee65 /x86 | |
| parent | c3ce32da7d431069ef355296bef66b112a302b78 (diff) | |
| download | compcert-kvx-a3319eb05543930844dedd9ac31ed1beaac3047e.tar.gz compcert-kvx-a3319eb05543930844dedd9ac31ed1beaac3047e.zip | |
Fix compile on ARM/x86 backends
Diffstat (limited to 'x86')
| -rw-r--r-- | x86/PrepassSchedulingOracle.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/x86/PrepassSchedulingOracle.ml b/x86/PrepassSchedulingOracle.ml index 7b6a1b14..31b4ea5b 100644 --- a/x86/PrepassSchedulingOracle.ml +++ b/x86/PrepassSchedulingOracle.ml @@ -1,5 +1,3 @@ -open RTL -open Registers (* Do not do anything *) -let schedule_sequence (seqa : (instruction*Regset.t) array) = None +let schedule_sequence inst btl = None |