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/Renumberproof.v | |
| parent | f7d64b71170e0694c5c4fb38ab7d1a23a4bd4c2a (diff) | |
| download | compcert-kvx-eafbaf41e528cc9825a503c66739a66a92ca65a8.tar.gz compcert-kvx-eafbaf41e528cc9825a503c66739a66a92ca65a8.zip | |
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/Renumberproof.v')
| -rw-r--r-- | backend/Renumberproof.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/backend/Renumberproof.v b/backend/Renumberproof.v index 4488e49b..f18d3c2e 100644 --- a/backend/Renumberproof.v +++ b/backend/Renumberproof.v @@ -98,9 +98,9 @@ Qed. End RENUMBER. -Definition pnum (f: function) := postorder (successors f) f.(fn_entrypoint). +Definition pnum (f: function) := postorder (successors_map f) f.(fn_entrypoint). -Definition reach (f: function) (pc: node) := reachable (successors f) f.(fn_entrypoint) pc. +Definition reach (f: function) (pc: node) := reachable (successors_map f) f.(fn_entrypoint) pc. Lemma transf_function_at: forall f pc i, @@ -109,11 +109,11 @@ Lemma transf_function_at: (transf_function f).(fn_code)!(renum_pc (pnum f) pc) = Some(renum_instr (pnum f) i). Proof. intros. - destruct (postorder_correct (successors f) f.(fn_entrypoint)) as [A B]. + destruct (postorder_correct (successors_map f) f.(fn_entrypoint)) as [A B]. fold (pnum f) in *. unfold renum_pc. destruct (pnum f)! pc as [pc'|] eqn:?. simpl. eapply renum_cfg_nodes; eauto. - elim (B pc); auto. unfold successors. rewrite PTree.gmap1. rewrite H. simpl. congruence. + elim (B pc); auto. unfold successors_map. rewrite PTree.gmap1. rewrite H. simpl. congruence. Qed. Ltac TR_AT := @@ -128,7 +128,7 @@ Lemma reach_succ: reach f pc -> reach f s. Proof. unfold reach; intros. econstructor; eauto. - unfold successors. rewrite PTree.gmap1. rewrite H. auto. + unfold successors_map. rewrite PTree.gmap1. rewrite H. auto. Qed. Inductive match_frames: RTL.stackframe -> RTL.stackframe -> Prop := |