diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-19 15:53:02 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-05-19 15:53:02 +0200 |
| commit | 9f252d9055ad16f9433caaf41f6490e45424e88a (patch) | |
| tree | ae2f3881062644dba56df68d669fcb3b0bd897d4 /scheduling/BTLtoRTLproof.v | |
| parent | ab520acd80f7d39aa14fdda6932accbb2a787ebf (diff) | |
| download | compcert-kvx-9f252d9055ad16f9433caaf41f6490e45424e88a.tar.gz compcert-kvx-9f252d9055ad16f9433caaf41f6490e45424e88a.zip | |
Adding a BTL record to help oracles
Diffstat (limited to 'scheduling/BTLtoRTLproof.v')
| -rw-r--r-- | scheduling/BTLtoRTLproof.v | 6 |
1 files changed, 3 insertions, 3 deletions
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. |