diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-04-19 07:17:03 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2008-04-19 07:17:03 +0000 |
commit | 9fdd9361e139fd36954f5ec9371d07461160b094 (patch) | |
tree | 7de467e88de1f0e026cb9da64add15e462bb9813 /caml | |
parent | 9e2f7e704ff490727bc9b83ffc2ca6ca95c73f3a (diff) | |
download | compcert-9fdd9361e139fd36954f5ec9371d07461160b094.tar.gz compcert-9fdd9361e139fd36954f5ec9371d07461160b094.zip |
Detecter __builtin_xxx
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@619 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'caml')
-rw-r--r-- | caml/Cil2Csyntax.ml | 13 |
1 files changed, 11 insertions, 2 deletions
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 |