diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2019-12-19 23:36:01 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2019-12-21 10:34:53 +0100 |
| commit | 4b042d572b943c8cb3b86b61e3282bba58f488ab (patch) | |
| tree | ae34d15572708ca62101f92b4e3acc1f480a092e /cparser/Elab.ml | |
| parent | 4dfcd7d4be18e8bc437ca170782212aa06635a95 (diff) | |
| download | compcert-kvx-4b042d572b943c8cb3b86b61e3282bba58f488ab.tar.gz compcert-kvx-4b042d572b943c8cb3b86b61e3282bba58f488ab.zip | |
Added error for unknown builtin functions. (#208)
Previously, using an unknown builtin function was treated like any
other call to an undeclared function: a warning was emitted, and
an error occurred at link-time.
With this commit, using an unknown builtin function is an error,
like in Clang.
Diffstat (limited to 'cparser/Elab.ml')
| -rw-r--r-- | cparser/Elab.ml | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 2b04340e..3dbb9d45 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -1853,7 +1853,12 @@ let elab_expr ctx loc env a = having declared it *) match a1 with | VARIABLE n when not (Env.ident_is_bound env n) -> - warning Implicit_function_declaration "implicit declaration of function '%s' is invalid in C99" n; + let is_builtin = String.length n > 10 + && String.sub n 0 10 = "__builtin_" in + if is_builtin then + error "use of unknown builtin '%s'" n + else + warning Implicit_function_declaration "implicit declaration of function '%s' is invalid in C99" n; let ty = TFun(TInt(IInt, []), None, false, []) in (* Check against other definitions and enter in env *) let (id, sto, env, ty, linkage) = |