diff options
| author | Pierre Nigron <pierre.nigron@free.fr> | 2020-09-22 12:32:59 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2022-09-19 16:23:17 +0200 |
| commit | b816d696733c96fdc62428e43c4a4a1f5a09b47b (patch) | |
| tree | 7a6ed23ab65addb874852d30b3a6ed8f1be11820 /backend/RTLgenspec.v | |
| parent | 88cccb19502dfec65f7e21d0f6772ba99b1fb99d (diff) | |
| download | compcert-b816d696733c96fdc62428e43c4a4a1f5a09b47b.tar.gz compcert-b816d696733c96fdc62428e43c4a4a1f5a09b47b.zip | |
RTLgen: use the state and error monad for reserve_labels (#371)
Diffstat (limited to 'backend/RTLgenspec.v')
| -rw-r--r-- | backend/RTLgenspec.v | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v index 25f9954c..f072b645 100644 --- a/backend/RTLgenspec.v +++ b/backend/RTLgenspec.v @@ -1339,14 +1339,12 @@ Lemma transl_function_charact: tr_function f tf. Proof. intros until tf. unfold transl_function. - caseEq (reserve_labels (fn_body f) (PTree.empty node, init_state)). - intros ngoto s0 RESERVE. - caseEq (transl_fun f ngoto s0). congruence. + caseEq (transl_fun f init_state). congruence. intros [nentry rparams] sfinal INCR TR E. inv E. monadInv TR. - exploit add_vars_valid. eexact EQ. apply init_mapping_valid. + exploit add_vars_valid. eexact EQ1. apply init_mapping_valid. intros [A B]. - exploit add_vars_valid. eexact EQ1. auto. + exploit add_vars_valid. eexact EQ0. auto. intros [C D]. eapply tr_function_intro; eauto with rtlg. eapply transl_stmt_charact; eauto with rtlg. |