diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-07 12:27:43 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-07 12:27:43 +0200 |
| commit | 35febfa5b231a71234a1b32c128169352e96eaca (patch) | |
| tree | 5401681c76c8e45e9c1e6128d313851582e6fc9f /backend/CSEproof.v | |
| parent | 046c24d29796a3bb130c94fe464e54e8a7aa2eb3 (diff) | |
| download | compcert-kvx-35febfa5b231a71234a1b32c128169352e96eaca.tar.gz compcert-kvx-35febfa5b231a71234a1b32c128169352e96eaca.zip | |
fixes for ARM
Diffstat (limited to 'backend/CSEproof.v')
| -rw-r--r-- | backend/CSEproof.v | 12 |
1 files changed, 3 insertions, 9 deletions
diff --git a/backend/CSEproof.v b/backend/CSEproof.v index 684729d4..209fa40f 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -1151,9 +1151,7 @@ Proof. econstructor. split. eapply exec_Iload; eauto. - rewrite eval_addressing_preserved with (ge1 := ge). - exact Ha'1. - exact symbols_preserved. + try (rewrite eval_addressing_preserved with (ge1 := ge) by assumption). econstructor; eauto. eapply analysis_correct_1; eauto. simpl; eauto. @@ -1204,9 +1202,7 @@ Proof. { econstructor. split. eapply exec_Iload; eauto. - rewrite eval_addressing_preserved with (ge1 := ge). - exact Ha'1. - exact symbols_preserved. + try (rewrite eval_addressing_preserved with (ge1 := ge) by assumption). econstructor; eauto. eapply analysis_correct_1; eauto. simpl; eauto. @@ -1220,9 +1216,7 @@ Proof. { econstructor. split. eapply exec_Iload_notrap2; eauto. - rewrite eval_addressing_preserved with (ge1 := ge). - exact Ha'1. - exact symbols_preserved. + try (rewrite eval_addressing_preserved with (ge1 := ge) by assumption). econstructor; eauto. eapply analysis_correct_1; eauto. simpl; eauto. |