diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-10-22 08:32:14 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2006-10-22 08:32:14 +0000 |
| commit | ee41c6eae5af0703605780e0b3d8f5c3937f3276 (patch) | |
| tree | 253e7939da12ff14a942814e392826696310b181 | |
| parent | b6bdb4b4924b0934aed24335597a89e49f7cbd61 (diff) | |
| download | compcert-kvx-ee41c6eae5af0703605780e0b3d8f5c3937f3276.tar.gz compcert-kvx-ee41c6eae5af0703605780e0b3d8f5c3937f3276.zip | |
Meilleur traitement des fonctions forward declared. Ajout d'un warning sur le nombre d'arguments d'une fonction externe, qui est actuellement limite par le back-end
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@124 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
| -rw-r--r-- | caml/Cil2Csyntax.ml | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/caml/Cil2Csyntax.ml b/caml/Cil2Csyntax.ml index 1c796ea3..4012cd15 100644 --- a/caml/Cil2Csyntax.ml +++ b/caml/Cil2Csyntax.ml @@ -160,6 +160,17 @@ let globals_for_strings globs = (fun s id l -> CList.Coq_cons(global_for_string s id, l)) stringTable globs +(** Checking restrictions on external functions *) + +let acceptableExtFun targs = + let rec acceptable nint nfloat = function + | Tnil -> true + | Tcons(Tfloat _, rem) -> + nfloat > 0 && acceptable (nint - 2) (nfloat - 1) rem + | Tcons(_, rem) -> + nint > 0 && acceptable (nint - 1) nfloat rem + in acceptable 8 10 targs + (** ** Handling of stubs for variadic functions *) let stub_function_table = Hashtbl.create 47 @@ -174,6 +185,8 @@ let register_stub_function name tres targs = try (stub_name, Hashtbl.find stub_function_table stub_name) with Not_found -> + if not (acceptableExtFun targs) then + warning (name ^ ": too many parameters for a variadic function, will fail during Cminor -> PPC translation"); let rec types_of_types = function | Tnil -> Tnil | Tcons(Tfloat _, tl) -> Tcons(Tfloat F64, types_of_types tl) @@ -851,6 +864,8 @@ let convertExtFun v = updateLoc(v.vdecl); match convertTyp v.vtype with | Tfunction(args, res) -> + if not (acceptableExtFun args) then + warning (v.vname ^ ": too many parameters for an external function, will fail during Cminor -> PPC translation"); let id = intern_string v.vname in Datatypes.Coq_pair (id, External(id, args, res)) | _ -> @@ -912,6 +927,7 @@ let cleanupGlobals globs = List.fold_right (fun g def -> match g with GVar (v, init, loc) -> v.vname :: def + | GFun (fdec, loc) -> fdec.svar.vname :: def | _ -> def) globs [] in List.filter |