diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-05 11:49:55 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-05 11:49:55 +0200 |
| commit | 42a4bac600c0eaa552b66659f2c67d2f8b44cdf6 (patch) | |
| tree | 915ede9317b4898864cf711e251fa28b7c99e70c /backend/Debugvarproof.v | |
| parent | fb09457f928fd4f19cd89a1fe22246444e3a5f4a (diff) | |
| download | compcert-kvx-42a4bac600c0eaa552b66659f2c67d2f8b44cdf6.tar.gz compcert-kvx-42a4bac600c0eaa552b66659f2c67d2f8b44cdf6.zip | |
more proof
Diffstat (limited to 'backend/Debugvarproof.v')
| -rw-r--r-- | backend/Debugvarproof.v | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/backend/Debugvarproof.v b/backend/Debugvarproof.v index d31c63ec..95020637 100644 --- a/backend/Debugvarproof.v +++ b/backend/Debugvarproof.v @@ -449,6 +449,22 @@ Proof. eauto. eauto. apply eval_add_delta_ranges. traceEq. constructor; auto. +- (* load notrap1 *) + econstructor; split. + eapply plus_left. + eapply exec_Lload_notrap1. + rewrite <- H; apply eval_addressing_preserved; exact symbols_preserved. + eauto. eauto. + apply eval_add_delta_ranges. traceEq. + constructor; auto. +- (* load notrap2 *) + econstructor; split. + eapply plus_left. + eapply exec_Lload_notrap2. + rewrite <- H; apply eval_addressing_preserved; exact symbols_preserved. + eauto. eauto. + apply eval_add_delta_ranges. traceEq. + constructor; auto. - (* store *) econstructor; split. eapply plus_left. |