diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-07-23 18:25:00 +0200 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-07-23 18:25:00 +0200 |
| commit | b063fb03af84483671833d40491f4fa8d2c8b4c9 (patch) | |
| tree | 89033ebd4ec906091d31457b0b7f3c8539e11dc1 /scheduling/BTLtoRTLproof.v | |
| parent | 8de8dc6616c49018c6151887f76ea08c8f1ff04e (diff) | |
| download | compcert-kvx-b063fb03af84483671833d40491f4fa8d2c8b4c9.tar.gz compcert-kvx-b063fb03af84483671833d40491f4fa8d2c8b4c9.zip | |
non trapping loads
Diffstat (limited to 'scheduling/BTLtoRTLproof.v')
| -rw-r--r-- | scheduling/BTLtoRTLproof.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/scheduling/BTLtoRTLproof.v b/scheduling/BTLtoRTLproof.v index 9b8dabab..324f1d14 100644 --- a/scheduling/BTLtoRTLproof.v +++ b/scheduling/BTLtoRTLproof.v @@ -230,7 +230,8 @@ Proof. intros; rewrite symbols_preserved; trivial. - (* exec_load *) inv MIB. exists pc'; split; auto; constructor. - apply plus_one. eapply exec_Iload; eauto. + apply plus_one. inv LOAD. + eapply exec_Iload; eauto. all: erewrite <- eval_addressing_preserved; eauto; intros; rewrite symbols_preserved; trivial. - (* exec_store *) |