From eafbaf41e528cc9825a503c66739a66a92ca65a8 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 12 Aug 2013 13:09:20 +0000 Subject: 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 --- backend/Constpropproof.v | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'backend/Constpropproof.v') diff --git a/backend/Constpropproof.v b/backend/Constpropproof.v index 2d11d942..dcab6f62 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. -- cgit