diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2021-01-10 12:51:29 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2021-01-10 12:51:29 +0100 |
| commit | ccdcb65f2d1c05ec31e6606fcdb676d93abe02dc (patch) | |
| tree | b52be3130245f212246b553e0a24cb11b4267ab2 | |
| parent | e4443dfc20fb76c49a168636d1252c93b89ea7fb (diff) | |
| download | compcert-kvx-ccdcb65f2d1c05ec31e6606fcdb676d93abe02dc.tar.gz compcert-kvx-ccdcb65f2d1c05ec31e6606fcdb676d93abe02dc.zip | |
one problem in this file (admitted)
| -rw-r--r-- | kvx/ValueAOpSSA.v | 2 | ||||
| -rw-r--r-- | midend/SCCPoptProp.v | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/kvx/ValueAOpSSA.v b/kvx/ValueAOpSSA.v index e94c0fc4..9e718621 100644 --- a/kvx/ValueAOpSSA.v +++ b/kvx/ValueAOpSSA.v @@ -317,7 +317,7 @@ Variable bc: block_classification. Variable ge: genv. Hypothesis GENV: genv_match bc ge. Variable sp: block. -Hypothesis STACK: bc sp <> BCinvalid. +Hypothesis STACK: bc sp = BCstack. Lemma minf_sound: forall v x w y, vmatch bc v x -> vmatch bc w y -> vmatch bc (ExtValues.minf v w) (minf x y). diff --git a/midend/SCCPoptProp.v b/midend/SCCPoptProp.v index 8bf5a52b..bdeec7b6 100644 --- a/midend/SCCPoptProp.v +++ b/midend/SCCPoptProp.v @@ -410,7 +410,7 @@ Proof. + intros. simpl. flatten. * split; congruence. * split; congruence. - - simpl. flatten. + - admit. (* simpl. flatten. *) - eapply G_list_val_list_match_approx; eauto. } eapply G_increasing; eauto. @@ -434,7 +434,7 @@ Proof. invh assigned_code_spec; try congruence. Unshelve. go. go. go. go. -Qed. +Admitted. Import Dom. Hint Resolve sdom_dom_pred fn_code_reached fn_entry_pred fn_phicode_inv |