From 2408dd1aecf8d8c3bfd3b24a65f7f57cf602cb10 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Thu, 20 May 2021 11:58:40 +0200 Subject: Changing to an opaq record in BTL info, this is a broken commit --- scheduling/BTL_SEtheory.v | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) (limited to 'scheduling/BTL_SEtheory.v') diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v index 94d299e7..cd69cd37 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. @@ -770,7 +770,7 @@ pour représenter l'ensemble des chemins. Fixpoint sexec_rec ib sis (k: sistate -> sstate): sstate := match ib with - | BF fin => Sfinal sis (sexec_final_sfv fin sis) + | 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) @@ -780,7 +780,7 @@ Fixpoint sexec_rec ib sis (k: sistate -> sstate): sstate := (* 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 -- cgit