From 271f87ba08f42340900378c0797511d4071fc1b8 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Mon, 31 May 2021 16:55:18 +0200 Subject: BTL Scheduler oracle and some drafts --- scheduling/BTL_Scheduler.v | 2 ++ 1 file changed, 2 insertions(+) (limited to 'scheduling/BTL_Scheduler.v') 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; -- cgit