Adding a BTL record to help oracles

1 files changed, 11 insertions, 11 deletions

diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v
index b9a05a8a..94d299e7 100644
--- a/scheduling/BTL_SEtheory.v
+++ b/scheduling/BTL_SEtheory.v
@@ -557,21 +557,21 @@ Qed.
 Definition sexec_final_sfv (i: final) (sis: sistate): sfval := 
   match i with
   | Bgoto pc => Sgoto pc
-  | Bcall sig ros args res pc => 
+  | Bcall sig ros args res pc _ => 
     let svos := sum_left_map sis.(si_sreg) ros in
     let sargs := list_sval_inj (List.map sis.(si_sreg) args) in
     Scall sig svos sargs res pc
-  | Btailcall sig ros args =>
+  | Btailcall sig ros args _ =>
     let svos := sum_left_map sis.(si_sreg) ros in
     let sargs := list_sval_inj (List.map sis.(si_sreg) args) in
     Stailcall sig svos sargs
-  | Bbuiltin ef args res pc =>
+  | Bbuiltin ef args res pc _ =>
     let sargs := List.map (builtin_arg_map sis.(si_sreg)) args in
     Sbuiltin ef sargs res pc
-  | Breturn or => 
+  | Breturn or _ => 
     let sor := SOME r <- or IN Some (sis.(si_sreg) r) in
     Sreturn sor
-  | Bjumptable reg tbl =>
+  | Bjumptable reg tbl _ =>
     let sv := sis.(si_sreg) reg in
     Sjumptable sv tbl
   end.
@@ -772,15 +772,15 @@ Fixpoint sexec_rec ib sis (k: sistate -> sstate): sstate :=
   match ib with
   | BF fin => Sfinal sis (sexec_final_sfv fin sis)
   (* basic instructions *)
-  | Bnop => k sis
-  | Bop op args res => k (sexec_op op args res sis)
-  | Bload TRAP chunk addr args dst => k (sexec_load TRAP chunk addr args dst sis)
-  | Bload NOTRAP chunk addr args dst => Sabort (* TODO *)
-  | Bstore chunk addr args src => k (sexec_store chunk addr args src sis)
+  | Bnop _ => k sis
+  | Bop op args res _ => k (sexec_op op args res sis)
+  | Bload TRAP chunk addr args dst _ => k (sexec_load TRAP chunk addr args dst sis)
+  | Bload NOTRAP chunk addr args dst _ => Sabort (* TODO *)
+  | Bstore chunk addr args src _ => k (sexec_store chunk addr args src sis)
  (* composed instructions *)
   | Bseq ib1 ib2 =>
       sexec_rec ib1 sis (fun sis2 => sexec_rec ib2 sis2 k) 
-  | Bcond cond args ifso ifnot _ =>
+  | Bcond cond args ifso ifnot _ _ =>
       let args := list_sval_inj (List.map sis.(si_sreg) args) in
       let ifso := sexec_rec ifso sis k in
       let ifnot := sexec_rec ifnot sis k in