From 42a4bac600c0eaa552b66659f2c67d2f8b44cdf6 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Thu, 5 Sep 2019 11:49:55 +0200 Subject: more proof --- backend/Debugvarproof.v | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) (limited to 'backend/Debugvarproof.v') 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. -- cgit