From 210352d90e5972aabfb253f7c8a38349f53917b3 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 22 Oct 2006 16:54:24 +0000 Subject: Lever la restriction sur les fonctions externes, restriction qui exigeait que tous les arguments resident en registres git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@125 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Conventions.v | 23 ----------------------- 1 file changed, 23 deletions(-) (limited to 'backend/Conventions.v') diff --git a/backend/Conventions.v b/backend/Conventions.v index 5b4222df..d621e7c0 100644 --- a/backend/Conventions.v +++ b/backend/Conventions.v @@ -676,29 +676,6 @@ Proof. intros; simpl. tauto. Qed. -(** ** Location of arguments to external functions *) - -Definition loc_external_arguments (s: signature) : list mreg := - List.map - (fun l => match l with R r => r | S _ => IT1 end) - (loc_arguments s). - -Definition sig_external_ok (s: signature) : Prop := - forall sl, ~In (S sl) (loc_arguments s). - -Lemma loc_external_arguments_loc_arguments: - forall s, - sig_external_ok s -> - loc_arguments s = List.map R (loc_external_arguments s). -Proof. - intros. unfold loc_external_arguments. - rewrite list_map_compose. - transitivity (List.map (fun x => x) (loc_arguments s)). - symmetry; apply list_map_identity. - apply list_map_exten; intros. - destruct x. auto. elim (H _ H0). -Qed. - (** ** Location of argument and result of dynamic allocation *) Definition loc_alloc_argument := R3. -- cgit