diff options
| author | Léo Gourdin <leo.gourdin@lilo.org> | 2021-11-02 11:17:10 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@lilo.org> | 2021-11-02 11:17:10 +0100 |
| commit | 98ec44d9d96e7e94896eea9ac054a0188be7b6dd (patch) | |
| tree | 9a749c8920ee020dd9c127398fdc516382b23eee /backend | |
| parent | 5530915001c3e8b395d731480e5a6618a08af7af (diff) | |
| download | compcert-kvx-98ec44d9d96e7e94896eea9ac054a0188be7b6dd.tar.gz compcert-kvx-98ec44d9d96e7e94896eea9ac054a0188be7b6dd.zip | |
bugfix
Diffstat (limited to 'backend')
| -rw-r--r-- | backend/Deadcodeproof.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/backend/Deadcodeproof.v b/backend/Deadcodeproof.v index be64a1a7..52332a82 100644 --- a/backend/Deadcodeproof.v +++ b/backend/Deadcodeproof.v @@ -823,7 +823,7 @@ Ltac UseTransfer := intros (tv & P & Q). econstructor; split. try (eapply exec_Iload; eauto; eapply has_loaded_normal; eauto; - [ rewrite <- U; apply eval_addressing_preserved; exact symbols_preserved | eauto]). + try (rewrite <- U; apply eval_addressing_preserved; exact symbols_preserved; fail); eauto). eapply match_succ_states; eauto. simpl; auto. apply eagree_update; eauto 2 with na. eapply magree_monotone; eauto. intros. apply incl_nmem_add; auto. @@ -851,7 +851,7 @@ Ltac UseTransfer := { econstructor; split. try (eapply exec_Iload; eauto; eapply has_loaded_normal; eauto; - erewrite eval_addressing_preserved with (ge1 := ge); [ assumption | exact symbols_preserved]). + try (rewrite <- U; apply eval_addressing_preserved; exact symbols_preserved; fail); eauto). eapply match_succ_states; eauto. simpl; auto. apply eagree_update; eauto 2 with na. eapply magree_monotone; eauto. intros. apply incl_nmem_add; auto. |