diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-01-15 09:45:17 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-01-15 09:45:17 +0100 |
| commit | b77b57ea6da032e0931a80c6e826ae9acc3e748e (patch) | |
| tree | b9c2dada7c0f0862acc191c966e6d80bb3ac9eb9 /cparser | |
| parent | 320d0841ee99fa33c0cd85e0fab203ee9b861748 (diff) | |
| parent | 4393640af54ee3139e5c399e6fa1685faf483707 (diff) | |
| download | compcert-kvx-b77b57ea6da032e0931a80c6e826ae9acc3e748e.tar.gz compcert-kvx-b77b57ea6da032e0931a80c6e826ae9acc3e748e.zip | |
Merge branch 'dm-div2' of https://github.com/monniaux/CompCert into mppa-work
Diffstat (limited to 'cparser')
| -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) = |