diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-08-12 13:09:20 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2013-08-12 13:09:20 +0000 |
| commit | eafbaf41e528cc9825a503c66739a66a92ca65a8 (patch) | |
| tree | 631be83d097b863cfce0482e143cf1d45f7263e8 /backend/Constpropproof.v | |
| parent | f7d64b71170e0694c5c4fb38ab7d1a23a4bd4c2a (diff) | |
Change interface of Kildall solvers to avoid precomputing the map pc -> list of successors.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2305 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'backend/Constpropproof.v')
| -rw-r--r-- | backend/Constpropproof.v | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index 2d11d94..dcab6f6 100644 --- a/backend/Constpropproof.v +++ b/backend/Constpropproof.v @@ -121,11 +121,10 @@ Lemma analyze_correct_1: Proof. unfold analyze; intros. set (lu := last_uses f) in *. - destruct (DS.fixpoint (successors f) (transfer' gapp f lu) + destruct (DS.fixpoint (fn_code f) successors_instr (transfer' gapp f lu) ((fn_entrypoint f, D.top) :: nil)) as [approxs|] eqn:FIX. apply regs_match_approx_increasing with (transfer' gapp f lu pc approxs!!pc). eapply DS.fixpoint_solution; eauto. - unfold successors_list, successors. rewrite PTree.gmap1. rewrite H. auto. unfold transfer'. destruct (lu!pc) as [regs|]. apply regs_match_approx_forget; auto. auto. @@ -138,7 +137,7 @@ Lemma analyze_correct_3: Proof. intros. unfold analyze. set (lu := last_uses f) in *. - destruct (DS.fixpoint (successors f) (transfer' gapp f lu) + destruct (DS.fixpoint (fn_code f) successors_instr (transfer' gapp f lu) ((fn_entrypoint f, D.top) :: nil)) as [approxs|] eqn:FIX. apply regs_match_approx_increasing with D.top. eapply DS.fixpoint_entry; eauto. auto with coqlib. |