diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-31 16:55:18 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-31 16:55:18 +0200 |
| commit | 271f87ba08f42340900378c0797511d4071fc1b8 (patch) | |
| tree | 8b861fa3221b179bb8e3ad339864cdb7c541d46a /scheduling/BTL_Scheduler.v | |
| parent | e6a1df51a2a3d29c58d72453355e50a979e86297 (diff) | |
| download | compcert-kvx-271f87ba08f42340900378c0797511d4071fc1b8.tar.gz compcert-kvx-271f87ba08f42340900378c0797511d4071fc1b8.zip | |
BTL Scheduler oracle and some drafts
Diffstat (limited to 'scheduling/BTL_Scheduler.v')
| -rw-r--r-- | scheduling/BTL_Scheduler.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/scheduling/BTL_Scheduler.v b/scheduling/BTL_Scheduler.v index 43d6dd5e..b479204c 100644 --- a/scheduling/BTL_Scheduler.v +++ b/scheduling/BTL_Scheduler.v @@ -7,6 +7,8 @@ Require Import Errors Linking BTL_SEtheory. (** External oracle *) Axiom scheduler: BTL.function -> BTL.code. +Extract Constant scheduler => "BTLScheduleraux.btl_scheduler". + (* a specification of the verification to do on each function *) Record match_function (f1 f2: BTL.function): Prop := { preserv_fnsig: fn_sig f1 = fn_sig f2; |