diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-01-09 08:54:33 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-01-09 08:54:33 +0100 |
| commit | 2e613cd29123583fb3378d5727217c359e818611 (patch) | |
| tree | 895a2db1ac78e2da9c7221238c4f2b8193f582c5 /backend/ForwardMovesproof.v | |
| parent | a36948c2af873559e5df4a2d96fdbc5bbfcfaca8 (diff) | |
| download | compcert-kvx-2e613cd29123583fb3378d5727217c359e818611.tar.gz compcert-kvx-2e613cd29123583fb3378d5727217c359e818611.zip | |
more proofs
Diffstat (limited to 'backend/ForwardMovesproof.v')
| -rw-r--r-- | backend/ForwardMovesproof.v | 19 |
1 files changed, 18 insertions, 1 deletions
diff --git a/backend/ForwardMovesproof.v b/backend/ForwardMovesproof.v index aa516df4..6562fc7b 100644 --- a/backend/ForwardMovesproof.v +++ b/backend/ForwardMovesproof.v @@ -199,6 +199,16 @@ Proof. reflexivity. Qed. +Lemma top_ok : + forall rs, get_rb_sem (Some RELATION.top) rs. +Proof. + unfold get_rb_sem, RELATION.top. + intros. + unfold get_r. + rewrite PTree.gempty. + reflexivity. +Qed. + Ltac TR_AT := match goal with | [ A: (fn_code _)!_ = Some _ |- _ ] => @@ -447,7 +457,14 @@ Proof. eapply exec_function_internal; eauto. constructor; auto. - admit. + simpl in *. + unfold fmap_sem in *. + destruct (forward_map _) as [map |] eqn:MAP in *; trivial. + apply get_rb_sem_ge with (rb2 := Some RELATION.top). + { + eapply DS.fixpoint_entry with (code := fn_code f) (successors := successors_instr); try eassumption. + } + apply top_ok. (* external function *) - econstructor; split. |