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/Stackingproof.v | |
| parent | 046c24d29796a3bb130c94fe464e54e8a7aa2eb3 (diff) | |
| download | compcert-kvx-35febfa5b231a71234a1b32c128169352e96eaca.tar.gz compcert-kvx-35febfa5b231a71234a1b32c128169352e96eaca.zip | |
fixes for ARM
Diffstat (limited to 'backend/Stackingproof.v')
| -rw-r--r-- | backend/Stackingproof.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index 1d4a93e7..19a40e0f 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -1943,7 +1943,7 @@ Proof. { econstructor; split. apply plus_one. apply exec_Mload with (a:=a') (v:=v'); eauto. - rewrite <- A. apply eval_addressing_preserved. exact symbols_preserved. + try (rewrite <- A; apply eval_addressing_preserved; assumption). econstructor; eauto with coqlib. apply agree_regs_set_reg. rewrite transl_destroyed_by_load. apply agree_regs_undef_regs; auto. auto. apply agree_locs_set_reg. apply agree_locs_undef_locs. auto. apply destroyed_by_load_caller_save. auto. @@ -1951,7 +1951,8 @@ Proof. { econstructor; split. apply plus_one. apply exec_Mload_notrap2 with (a:=a'); eauto. - rewrite <- A. apply eval_addressing_preserved. exact symbols_preserved. + try (rewrite <- A; apply eval_addressing_preserved; assumption). + econstructor; eauto with coqlib. apply agree_regs_set_reg. rewrite transl_destroyed_by_load. apply agree_regs_undef_regs; auto. auto. apply agree_locs_set_reg. apply agree_locs_undef_locs. auto. apply destroyed_by_load_caller_save. auto. |