diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-05 13:52:34 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-04-05 13:52:34 +0200 |
| commit | 799698875bd5b42b9ef5e57138f71128e68ed35e (patch) | |
| tree | 2c577959006a78fc7067560995899a96e44ec764 /backend/Selectionproof.v | |
| parent | e4bc9aa604977ee168c2f580d3fc3c3521f6c25c (diff) | |
| download | compcert-kvx-799698875bd5b42b9ef5e57138f71128e68ed35e.tar.gz compcert-kvx-799698875bd5b42b9ef5e57138f71128e68ed35e.zip | |
removed the unproved hack to get builtins, will be reinstated later
Diffstat (limited to 'backend/Selectionproof.v')
| -rw-r--r-- | backend/Selectionproof.v | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index d839f22a..50ff377a 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -854,8 +854,6 @@ Remark find_label_commut: | _, _ => False end. Proof. -Admitted. -(* induction s; intros until k'; simpl; intros MC SE; try (monadInv SE); simpl; auto. (* store *) unfold store. destruct (addressing m (sel_expr e)); simpl; auto. @@ -888,7 +886,6 @@ Admitted. (* label *) destruct (ident_eq lbl l). auto. apply IHs; auto. Qed. - *) Definition measure (s: Cminor.state) : nat := match s with @@ -903,8 +900,6 @@ Lemma sel_step_correct: (exists T2, step tge T1 t T2 /\ match_states S2 T2) \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 T1)%nat. Proof. -Admitted. -(* induction 1; intros T1 ME; inv ME; try (monadInv TS). - (* skip seq *) inv MC. left; econstructor; split. econstructor. econstructor; eauto. @@ -1072,7 +1067,6 @@ Admitted. right; split. simpl; omega. split. auto. econstructor; eauto. apply sel_builtin_res_correct; auto. Qed. - *) Lemma sel_initial_states: forall S, Cminor.initial_state prog S -> |