diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-04 18:44:23 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-04 18:44:23 +0200 |
| commit | 55a90812e9f6f65b4abe7a124e933875f212238c (patch) | |
| tree | 3eb63f2584abbb3b77419e325eb60168af552b49 /backend/CSEproof.v | |
| parent | 44f4bea5d16273b834b1bcc8624c8f00aefaf018 (diff) | |
| download | compcert-kvx-55a90812e9f6f65b4abe7a124e933875f212238c.tar.gz compcert-kvx-55a90812e9f6f65b4abe7a124e933875f212238c.zip | |
ca avance
Diffstat (limited to 'backend/CSEproof.v')
| -rw-r--r-- | backend/CSEproof.v | 13 |
1 files changed, 11 insertions, 2 deletions
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: |