diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2014-11-27 15:37:32 +0100 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2014-11-27 15:37:32 +0100 |
| commit | 56690956f52349c3398b3de6f8ec3987501e9034 (patch) | |
| tree | 5fc98e863bb41018084b2110f0ae950189a7b7d6 /backend/Inliningproof.v | |
| parent | 853a40b117495ebf883593633f680cd5c92f5951 (diff) | |
| parent | c3b615f875ed2cf8418453c79c4621d2dc61b0a0 (diff) | |
| download | compcert-56690956f52349c3398b3de6f8ec3987501e9034.tar.gz compcert-56690956f52349c3398b3de6f8ec3987501e9034.zip | |
Merge branch 'master' into dwarf
Diffstat (limited to 'backend/Inliningproof.v')
| -rw-r--r-- | backend/Inliningproof.v | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v index 2564a736..9b1aec4c 100644 --- a/backend/Inliningproof.v +++ b/backend/Inliningproof.v @@ -43,6 +43,12 @@ Proof. intros. apply Genv.find_symbol_transf_partial with (transf_fundef fenv); auto. Qed. +Lemma public_preserved: + forall (s: ident), Genv.public_symbol tge s = Genv.public_symbol ge s. +Proof. + intros. apply Genv.public_symbol_transf_partial with (transf_fundef fenv); auto. +Qed. + Lemma varinfo_preserved: forall b, Genv.find_var_info tge b = Genv.find_var_info ge b. Proof. @@ -1008,7 +1014,7 @@ Proof. left; econstructor; split. eapply plus_one. eapply exec_Ibuiltin; eauto. eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. econstructor. eapply match_stacks_inside_set_reg. eapply match_stacks_inside_extcall with (F1 := F) (F2 := F1) (m1 := m) (m1' := m'0); eauto. @@ -1161,7 +1167,7 @@ Proof. left; econstructor; split. eapply plus_one. eapply exec_function_external; eauto. eapply external_call_symbols_preserved; eauto. - exact symbols_preserved. exact varinfo_preserved. + exact symbols_preserved. exact public_preserved. exact varinfo_preserved. econstructor. eapply match_stacks_bound with (Mem.nextblock m'0). eapply match_stacks_extcall with (F1 := F) (F2 := F1) (m1 := m) (m1' := m'0); eauto. @@ -1250,7 +1256,7 @@ Theorem transf_program_correct: forward_simulation (semantics prog) (semantics tprog). Proof. eapply forward_simulation_star. - eexact symbols_preserved. + eexact public_preserved. eexact transf_initial_states. eexact transf_final_states. eexact step_simulation. |