diff options
| -rw-r--r-- | driver/Compiler.vexpand | 2 | ||||
| -rw-r--r-- | scheduling/BTL.v | 4 | ||||
| -rw-r--r-- | scheduling/BTL_SEtheory.v | 2 | ||||
| -rw-r--r-- | 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. |