From 55a90812e9f6f65b4abe7a124e933875f212238c Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 4 Sep 2019 18:44:23 +0200 Subject: ca avance --- backend/CSEproof.v | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) (limited to 'backend/CSEproof.v') diff --git a/backend/CSEproof.v b/backend/CSEproof.v index def8003c..108aef31 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -608,8 +608,17 @@ Proof. unfold aaddressing. apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto. erewrite <- regs_valnums_sound by eauto. eauto with va. auto. - -(* TODO *) +- eapply load_notrap1_eval_to; assumption. +- destruct (regs_valnums n vl) as [rl|] eqn:RV; try discriminate. + eapply load_notrap2_eval_to; eauto. rewrite <- H11. + destruct a; simpl in H10; try discriminate; simpl; trivial. + rewrite negb_false_iff in H8. + eapply Mem.load_storebytes_other. eauto. + rewrite H6. rewrite Z2Nat.id by omega. + eapply pdisjoint_sound. eauto. + unfold aaddressing. apply match_aptr_of_aval. eapply eval_static_addressing_sound; eauto. + erewrite <- regs_valnums_sound by eauto. eauto with va. + auto. Qed. Lemma load_memcpy: -- cgit