From 9f252d9055ad16f9433caaf41f6490e45424e88a Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Wed, 19 May 2021 15:53:02 +0200 Subject: Adding a BTL record to help oracles --- scheduling/BTLtoRTLproof.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'scheduling/BTLtoRTLproof.v') diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v index 08a77ae4..6c894b78 100644 --- a/scheduling/BTLtoRTLproof.v +++ b/scheduling/BTLtoRTLproof.v @@ -263,7 +263,7 @@ Proof. eapply plus_trans; eauto. - (* exec_cond *) inv MIB. - rename H10 into JOIN. (* is_join_opt opc1 opc2 opc *) + rename H11 into JOIN. (* is_join_opt opc1 opc2 opc *) destruct b; exploit IHIBIS; eauto. + (* taking ifso *) destruct ofin; simpl. @@ -305,14 +305,14 @@ Proof. erewrite <- preserv_fnstacksize; eauto. econstructor; eauto. - (* call *) - rename H7 into FIND. + rename H8 into FIND. exploit find_function_preserved; eauto. intros (fd' & FIND' & TRANSFU). eexists; split. eapply exec_Icall; eauto. apply function_sig_translated. assumption. repeat (econstructor; eauto). - (* tailcall *) - rename H2 into FIND. + rename H3 into FIND. exploit find_function_preserved; eauto. intros (fd' & FIND' & TRANSFU). eexists; split. eapply exec_Itailcall; eauto. -- cgit