From 9fdd9361e139fd36954f5ec9371d07461160b094 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 19 Apr 2008 07:17:03 +0000 Subject: Detecter __builtin_xxx git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@619 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- caml/Cil2Csyntax.ml | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) (limited to 'caml/Cil2Csyntax.ml') diff --git a/caml/Cil2Csyntax.ml b/caml/Cil2Csyntax.ml index 17bcb262..f736fb0c 100644 --- a/caml/Cil2Csyntax.ml +++ b/caml/Cil2Csyntax.ml @@ -220,6 +220,14 @@ let make_temp typ = let v = Cil.makeTempVar f typ in intern_string v.vname +(** Detect and report GCC's __builtin_ functions *) + +let check_builtin s = + let b = "__builtin_" in + if String.length s >= String.length b + && String.sub s 0 (String.length b) = b + then unsupported ("GCC `" ^ s ^ "' built-in function") + (** ** Translation functions *) (** Convert a [Cil.ikind] into a pair [(intsize * signedness)] *) @@ -426,6 +434,7 @@ and convertLval lv = (* convert the lvalue *) match lv with | (Var v, ofs) -> + check_builtin v.vname; let id = intern_string v.vname in processOffset (Expr (Evar id, convertTyp v.vtype)) ofs | (Mem e, ofs) -> @@ -535,10 +544,10 @@ let convertExpFuncall e eList = let fun_name = match e with | Lval(Var v, NoOffset) -> - warning "working around a call to a variadic or non-prototyped function"; + warning "working around a call to a variadic function"; v.vname | _ -> - unsupported "call to variadic or non-prototyped function" in + unsupported "call to variadic function" in let rec typeOfExprList = function | Coq_nil -> Tnil | Coq_cons (Expr (_, ty), rem) -> Tcons (ty, typeOfExprList rem) in -- cgit