From 8752cea89f862d92d49183fe10d1918588143ab1 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Fri, 28 May 2021 12:38:05 +0200 Subject: fix some merge errors --- driver/Compiler.vexpand | 2 +- scheduling/BTL.v | 4 ++-- scheduling/BTL_SEtheory.v | 2 +- scheduling/RTLtoBTLproof.v | 1 + 4 files changed, 5 insertions(+), 4 deletions(-) diff --git a/driver/Compiler.vexpand b/driver/Compiler.vexpand index 40ea0d68..85f265db 100644 --- a/driver/Compiler.vexpand +++ b/driver/Compiler.vexpand @@ -300,7 +300,7 @@ EXPAND_RTL_FORWARD_SIMULATIONS eapply compose_forward_simulations. eapply RTLtoBTLproof.transf_program_correct; eassumption. eapply compose_forward_simulations. - eapply BTLtoRTLproof.transf_program_correct; eassumption. + eapply BTLtoRTLproof.transf_program_correct_cfg; eassumption. eapply compose_forward_simulations. eapply Allocationproof.transf_program_correct; eassumption. eapply compose_forward_simulations. diff --git a/scheduling/BTL.v b/scheduling/BTL.v index 2be4fcac..2c1dda5b 100644 --- a/scheduling/BTL.v +++ b/scheduling/BTL.v @@ -94,7 +94,7 @@ Coercion BF: final >-> Funclass. Record iblock_info := { entry: iblock; - input_regs: Regset.t (* extra liveness information for BTL functional semantics *) + input_regs: Regset.t; (* extra liveness information for BTL functional semantics *) binfo: block_info (* Ghost field used in oracles *) }. @@ -1285,4 +1285,4 @@ Definition is_goto (ib: iblock): bool := match ib with | BF (Bgoto _) _ => true | _ => false - end. \ No newline at end of file + end. diff --git a/scheduling/BTL_SEtheory.v b/scheduling/BTL_SEtheory.v index cea69f55..5b15fe9b 100644 --- a/scheduling/BTL_SEtheory.v +++ b/scheduling/BTL_SEtheory.v @@ -731,7 +731,7 @@ pour représenter l'ensemble des chemins. Fixpoint sexec_rec f ib sis (k: sistate -> sstate): sstate := match ib with - | BF fin => Sfinal (tr_sis f fin sis) (sexec_final_sfv fin sis) + | BF fin _ => Sfinal (tr_sis f fin sis) (sexec_final_sfv fin sis) (* basic instructions *) | Bnop _ => k sis | Bop op args res _ => k (sexec_op op args res sis) diff --git a/scheduling/RTLtoBTLproof.v b/scheduling/RTLtoBTLproof.v index 7d83931b..f2f99ef5 100644 --- a/scheduling/RTLtoBTLproof.v +++ b/scheduling/RTLtoBTLproof.v @@ -554,6 +554,7 @@ Proof. eexists; left; eexists; split; eauto. repeat econstructor; eauto. apply iblock_istep_run_equiv in BTL_RUN; eauto. + econstructor. - (* Others *) exists (Some ib2); right; split. simpl; auto. -- cgit